Theory Groups_On_With
theory Groups_On_With
imports
"HOL-Types_To_Sets.Group_On_With"
Complex_Main
begin
section ‹Locales for non-abelian groups›
text ‹Extends the approach used for smooth manifolds in \<^session>‹HOL-Types_To_Sets›
(under Examples) to also include non-commutative groups.
We can use the \<^locale>‹semigroup_add_on_with› as it is defined in the theory above.
Notice "add" is merely a name for the group operation, we will want to apply this to groups under
(matrix) multiplication too.›
subsection ‹Locale definitions leading to non-abelian groups›
locale monoid_on_with = semigroup_add_on_with +
fixes z
assumes add_zero: "a ∈ S ⟹ pls z a = a ∧ pls a z = a"
assumes zero_mem: "z ∈ S"
begin
lemma carrier_ne: "S ≠ {}" using zero_mem by auto
lemma
assumes "a ∈ S"
shows add_zeroL: "pls z a = a"
and add_zeroR: "pls a z = a"
by (simp_all add: add_zero assms)
end
locale group_on_with = monoid_on_with +
fixes mns um
assumes left_minus: "a ∈ S ⟹ pls (um a) a = z"
and diff_conv_add_uminus: "a ∈ S ⟹ b ∈ S ⟹ mns a b = pls a (um b)"
and uminus_mem: "a ∈ S ⟹ um a ∈ S"
begin
text ‹Axiom @{thm diff_conv_add_uminus} ensures division/subtraction agrees with inverse/unary-minus,
while leaving the flexibility to provide any fitting implementation of the operations
(since they are constrained only on the carrier set).›
lemma right_minus: "a ∈ S ⟹ pls a (um a) = z"
by (metis (full_types) add_assoc add_zero add_zeroR local.left_minus uminus_mem)
lemma add_uminus: "a ∈ S ⟹ pls a (um a) = z ∧ pls (um a) a = z"
by (simp add: left_minus right_minus)
text ‹A group's identity is unique: we show this both inside and outside \<^locale>‹group_on_with›.
The in-locale version is mildly more powerful, requiring invariance only on one side.
The non-locale lemma is used later to prove there is a canonical instantiation of the group
inverse and division, and to provide the sublocale ‹grp_on› of \<^locale>‹group_on_with›,
which requires fewer parameters.›
lemma id_is_unique:
assumes "⋀x. x∈S ⟹ pls x other_id = x ∨ pls other_id x = x" "other_id∈S"
shows "other_id = z"
using assms zero_mem add_zero add_zeroR
by metis
lemma uminus_uminus: "x∈S ⟹ um (um x) = x"
by (metis (full_types) add_assoc add_zeroL add_zeroR local.right_minus uminus_mem)
end
lemma id_is_unique:
fixes G::"'a set" and mult::"'a⇒'a⇒'a" and e::'a
defines "is_id ≡ λe. e∈G ∧ (∀a∈G. mult e a = a ∧ mult a e = a)"
assumes ident: "is_id e"
shows "e = (THE e. is_id e)" "is_id e' ⟶ e'=e"
using the_equality apply (metis assms) by (metis assms)
text ‹Inverses are unique too, and we show this in several lemmas both inside and outside the locale
‹group_on_with›, as above.›
lemma inv_is_uniqueL:
fixes G::"'a set" and mult::"'a⇒'a⇒'a" and e::'a
defines "is_id ≡ λe. e∈G ∧ (∀a∈G. mult e a = a)"
assumes assoc: "∀a∈G. ∀b∈G. ∀c∈G. mult (mult a b) c = mult a (mult b c)"
and ident: "is_id e"
and inver: "∀x∈G. ∃y∈G. mult x y = e"
and "x∈G" "y∈G" "z∈G" "mult x y = e" "mult x z = e"
shows "y=z"
by (metis assms)
lemma inv_is_uniqueR:
fixes G::"'a set" and mult::"'a⇒'a⇒'a" and e::'a
defines "is_id ≡ λe. e∈G ∧ (∀a∈G. mult a e = a)"
assumes assoc: "∀a∈G. ∀b∈G. ∀c∈G. mult (mult a b) c = mult a (mult b c)"
and ident: "is_id e"
and inver: "∀x∈G. ∃y∈G. mult x y = e"
and "x∈G" "y∈G" "z∈G" "mult y x = e" "mult z x = e"
shows "y=z"
by (metis assms)
lemma inv_is_unique:
fixes G::"'a set" and mult::"'a⇒'a⇒'a" and e::'a
defines "is_id ≡ λe. e∈G ∧ (∀a∈G. mult e a = a ∧ mult a e = a)"
assumes assoc: "∀a∈G. ∀b∈G. ∀c∈G. mult (mult a b) c = mult a (mult b c)"
and ident: "is_id e"
and "x∈G" "y∈G" "z∈G" "mult y x = e" "mult x z = e"
shows "y=z"
by (metis assms)
lemma (in group_on_with) inv_is_unique:
fixes other_inv
assumes "∀x∈S. pls x (other_inv x) = z ∨ pls (other_inv x) x = z"
and "∀x∈S. other_inv x ∈ S"
shows "∀x∈S. other_inv x = um x"
proof
fix x assume "x∈S"
consider "pls x (other_inv x) = z" | "pls (other_inv x) x = z" using assms ‹x ∈ S› by auto
thus "other_inv x = um x"
proof (cases)
case 1
hence "um x = pls (um x) (pls x (other_inv x))" by (simp add: ‹x∈S› add_zeroR uminus_mem)
also have "… = pls (pls (um x) x) (other_inv x)" by (simp add: ‹x∈S› add_assoc assms(2) uminus_mem)
finally show "other_inv x = um x" by (simp add: ‹x∈S› add_zero assms(2) left_minus)
next
case 2
hence "um x = pls (pls (other_inv x) x) (um x)" using add_zero[OF uminus_mem[OF ‹x∈S›]] by simp
also have "… = pls (other_inv x) (pls x (um x))" by (simp add: ‹x∈S› add_assoc assms(2) uminus_mem)
finally show "other_inv x = um x" by (simp add: ‹x∈S› add_zeroR assms(2) right_minus)
qed
qed
lemma group_on_with_alt_intro:
fixes G::"'a set" and mult::"'a⇒'a⇒'a" and e::'a
and is_id is_inv
defines "is_id ≡ λe. e∈G ∧ (∀a∈G. mult e a = a ∧ mult a e = a)"
and "is_inv ≡ λx y. y∈G ∧ mult x y = e ∧ mult y x = e"
assumes closed: "∀a∈G. ∀b∈G. mult a b ∈ G"
and assoc: "∀a∈G. ∀b∈G. ∀c∈G. mult (mult a b) c = mult a (mult b c)"
and ident: "is_id e"
and inver: "∀x∈G. ∃y. is_inv x y"
shows "group_on_with G mult e (λx z. mult x (THE y. is_inv z y)) (λx. THE y. is_inv x y)"
(is "group_on_with G mult e ?div ?inv")
proof (unfold_locales)
show "e∈G"
using ident is_id_def by auto
have inv: "∀x∈G. mult x (?inv x) = e" "∀x∈G. ?inv x ∈ G" "∀x∈G. mult (?inv x) x = e"
proof (safe)
fix x assume "x∈G"
have 1: "e∈G ∧ (∀a∈G. mult e a = a)" "∀x∈G. ∃y∈G. mult x y = e"
using ident is_id_def inver is_inv_def by auto
obtain y where y: "is_inv x y"
using inver ‹x∈G› by blast
have y_Uniq: "y = ?inv x"
using y inv_is_uniqueL[OF assoc 1 ‹x∈G›] unfolding is_inv_def by (simp add: the_equality)
thus 2: "mult x (?inv x) = e"
using is_inv_def y by blast
show "?inv x ∈ G"
using y y_Uniq is_inv_def by simp
show "mult (?inv x) x = e"
using 2 is_id_def by (metis is_inv_def y y_Uniq)
qed
fix x assume "x ∈ G"
show "mult e x = x ∧ mult x e = x"
using ‹x ∈ G› ident is_id_def by auto
show "mult (?inv x) x = e"
using inv(3) by (simp add: ‹x ∈ G›)
show "?inv x ∈ G"
by (simp add: ‹x ∈ G› inv(2))
qed (simp add: assoc closed)+
locale grp_on = monoid_on_with +
assumes inv_ex: "∀x∈S. ∃y∈S. pls x y = z ∧ pls y x = z"
begin
definition "is_invs x y ≡ y∈S ∧ pls x y = z ∧ pls y x = z"
definition "invs ≡ (λx. THE y. is_invs x y)"
definition "mns ≡ (λx y. pls x (invs y))"
lemma is_group_on_with:
shows "group_on_with S pls z mns invs"
apply (unfold mns_def invs_def is_invs_def, intro group_on_with_alt_intro)
using inv_ex by (auto simp: add_mem add_assoc add_zero zero_mem)
lemma grp_on_cong:
assumes "⋀x y. x∈S ⟹ y∈S ⟹ pls x y = pls' x y"
shows "grp_on S pls' z"
using assms add_assoc add_mem add_zeroR inv_ex zero_mem by (unfold_locales, auto)
sublocale group_on_with S pls z mns invs
using is_group_on_with by simp
end
lemma (in group_on_with) is_grp_on:
shows "grp_on S pls z"
using add_uminus uminus_mem by (unfold_locales, blast)
subsection ‹(Homo)morphism of groups›
locale group_on_with_pair =
G1: group_on_with G1 pls1 z1 mns1 um1 +
G2: group_on_with G2 pls2 z2 mns2 um2
for G1 G2 pls1 pls2 z1 z2 mns1 mns2 um1 um2
locale group_hom_betw =
group_on_with_pair +
fixes f
assumes group_hom: "x∈G1 ⟹ y∈G1 ⟹ f (pls1 x y) = pls2 (f x) (f y)"
and closure: "x ∈ G1 ⟹ f x ∈ G2"
begin
lemma maps_id: "f z1 = z2"
using G2.id_is_unique closure group_hom
by (metis (full_types) G1.add_zeroR G1.zero_mem G2.add_assoc G2.add_zeroR G2.right_minus G2.uminus_mem)
lemma maps_inv: "f (um1 x) = um2 (f x)" if "x∈G1" for x
using G2.inv_is_unique G1.uminus_mem closure group_hom that maps_id
by (smt (z3) G1.left_minus G2.add_assoc G2.add_zeroL G2.add_zeroR G2.right_minus G2.uminus_mem)
end
end