(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013-2022 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Groups 5› theory Group_ZF_5 imports Group_ZF_4 Ring_ZF Semigroup_ZF begin text‹In this theory we study group homomorphisms.› subsection‹Homomorphisms› text‹A homomorphism is a function between groups that preserves the group operations.› text‹Suppose we have two groups $G$ and $H$ with corresponding binary operations $P:G\times G \rightarrow G$ and $F:H\times H \rightarrow H$. Then $f$ is a homomorphism if for all $g_1,g_2\in G$ we have $f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle$. › definition Homomor where "IsAgroup(G,P) ⟹ IsAgroup(H,F) ⟹ Homomor(f,G,P,H,F) ≡ ∀g⇩_{1}∈G. ∀g⇩_{2}∈G. f`(P`⟨g⇩_{1},g⇩_{2}⟩)=F`⟨f`(g⇩_{1}),f`(g⇩_{2})⟩" text‹Now a lemma about the definition:› lemma homomor_eq: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "g⇩_{1}∈G" "g⇩_{2}∈G" shows "f`(P`⟨g⇩_{1},g⇩_{2}⟩)=F`⟨f`(g⇩_{1}),f`(g⇩_{2})⟩" using assms Homomor_def by auto text‹An endomorphism is a homomorphism from a group to the same group. In case the group is abelian, it has a nice structure.› definition "End(G,P) ≡ {f∈G→G. Homomor(f,G,P,G,P)}" text‹The defining property of an endomorphism written in notation used in ‹group0› context:› lemma (in group0) endomor_eq: assumes "f ∈ End(G,P)" "g⇩_{1}∈G" "g⇩_{2}∈G" shows "f`(g⇩_{1}⋅g⇩_{2}) = f`(g⇩_{1})⋅f`(g⇩_{2})" using groupAssum assms homomor_eq unfolding End_def by simp text‹A function that maps a group $G$ into itself and satisfies $f(g_1\cdot g2) = f(g_1)\cdot f(g_2)$ is an endomorphism.› lemma (in group0) eq_endomor: assumes "f:G→G" and "∀g⇩_{1}∈G. ∀g⇩_{2}∈G. f`(g⇩_{1}⋅g⇩_{2})=f`(g⇩_{1})⋅f`(g⇩_{2})" shows "f ∈ End(G,P)" using groupAssum assms Homomor_def unfolding End_def by auto text‹The set of endomorphisms forms a submonoid of the monoid of function from a set to that set under composition.› lemma (in group0) end_composition: assumes "f⇩_{1}∈End(G,P)" "f⇩_{2}∈End(G,P)" shows "Composition(G)`⟨f⇩_{1},f⇩_{2}⟩ ∈ End(G,P)" proof- from assms have fun: "f⇩_{1}:G→G" "f⇩_{2}:G→G" unfolding End_def by auto then have "f⇩_{1}O f⇩_{2}:G→G" using comp_fun by auto from assms fun(2) have "∀g⇩_{1}∈G. ∀g⇩_{2}∈G. (f⇩_{1}O f⇩_{2})`(g⇩_{1}⋅g⇩_{2}) = ((f⇩_{1}O f⇩_{2})`(g⇩_{1}))⋅((f⇩_{1}O f⇩_{2})`(g⇩_{2}))" using group_op_closed comp_fun_apply endomor_eq apply_type by simp with fun ‹f⇩_{1}O f⇩_{2}:G→G› show ?thesis using eq_endomor func_ZF_5_L2 by simp qed text‹We will use some binary operations that are naturally defined on the function space $G\rightarrow G$, but we consider them restricted to the endomorphisms of $G$. To shorten the notation in such case we define an abbreviation ‹InEnd(F,G,P)› which restricts a binary operation $F$ to the set of endomorphisms of $G$. › abbreviation InEnd("_ {in End} [_,_]") where "InEnd(F,G,P) ≡ restrict(F,End(G,P)×End(G,P))" text‹Endomoprhisms of a group form a monoid with composition as the binary operation, with the identity map as the neutral element.› theorem (in group0) end_comp_monoid: shows "IsAmonoid(End(G,P),InEnd(Composition(G),G,P))" and "TheNeutralElement(End(G,P),InEnd(Composition(G),G,P))=id(G)" proof - let ?C⇩_{0}= "InEnd(Composition(G),G,P)" have fun: "id(G):G→G" unfolding id_def by auto { fix g h assume "g∈G""h∈G" then have "id(G)`(g⋅h)=(id(G)`g)⋅(id(G)`h)" using group_op_closed by simp } with groupAssum fun have "id(G) ∈ End(G,P)" using eq_endomor by simp moreover have A0: "id(G)=TheNeutralElement(G → G, Composition(G))" using Group_ZF_2_5_L2(2) by auto ultimately have A1: "TheNeutralElement(G → G, Composition(G)) ∈ End(G,P)" by auto moreover have A2: "End(G,P) ⊆ G→G" unfolding End_def by blast moreover have A3: "End(G,P) {is closed under} Composition(G)" using end_composition unfolding IsOpClosed_def by blast ultimately show "IsAmonoid(End(G,P),?C⇩_{0})" using monoid0.group0_1_T1 Group_ZF_2_5_L2(1) unfolding monoid0_def by blast have "IsAmonoid(G→G,Composition(G))" using Group_ZF_2_5_L2(1) by auto with A0 A1 A2 A3 show "TheNeutralElement(End(G,P),?C⇩_{0}) = id(G)" using group0_1_L6 by auto qed text‹The set of endomorphisms is closed under pointwise addition (derived from the group operation). This is so because the group is abelian.› theorem (in abelian_group) end_pointwise_addition: assumes "f∈End(G,P)" "g∈End(G,P)" "F = P {lifted to function space over} G" shows "F`⟨f,g⟩ ∈ End(G,P)" proof- from assms(1,2) have fun: "f:G→G" "g∈G→G" unfolding End_def by simp_all with assms(3) have fun2: "F`⟨f,g⟩:G→G" using monoid0.Group_ZF_2_1_L0 group0_2_L1 by simp { fix g⇩_{1}g⇩_{2}assume "g⇩_{1}∈G" "g⇩_{2}∈G" with isAbelian assms fun have "(F`⟨f,g⟩)`(g⇩_{1}⋅g⇩_{2}) = (F`⟨f,g⟩)`(g⇩_{1})⋅(F`⟨f,g⟩)`(g⇩_{2})" using Group_ZF_2_1_L3 group_op_closed endomor_eq apply_type group0_4_L8(3) Group_ZF_2_1_L3 by simp } with fun2 show ?thesis using eq_endomor by simp qed text‹The inverse of an abelian group is an endomorphism.› lemma (in abelian_group) end_inverse_group: shows "GroupInv(G,P) ∈ End(G,P)" using inverse_in_group group_inv_of_two isAbelian IsCommutative_def group0_2_T2 groupAssum Homomor_def unfolding End_def by simp text‹The set of homomorphisms of an abelian group is an abelian subgroup of the group of functions from a set to a group, under pointwise multiplication.› theorem (in abelian_group) end_addition_group: assumes "F = P {lifted to function space over} G" shows "IsAgroup(End(G,P),InEnd(F,G,P))" and "InEnd(F,G,P) {is commutative on} End(G,P)" proof- have "End(G,P)≠0" using end_comp_monoid(1) monoid0.group0_1_L3A unfolding monoid0_def by auto moreover have "End(G,P) ⊆ G→G" unfolding End_def by auto moreover from isAbelian assms(1) have "End(G,P){is closed under}F" unfolding IsOpClosed_def using end_pointwise_addition by auto moreover from groupAssum assms(1) have "∀f∈End(G,P). GroupInv(G→G,F)`(f) ∈ End(G,P)" using monoid0.group0_1_L1 end_composition(1) end_inverse_group func_ZF_5_L2 group0_2_T2 Group_ZF_2_1_L6 unfolding monoid0_def End_def by force ultimately show "IsAgroup(End(G,P),InEnd(F,G,P))" using assms(1) group0.group0_3_T3 Group_ZF_2_1_T2 unfolding IsAsubgroup_def group0_def by blast from assms(1) isAbelian show "InEnd(F,G,P) {is commutative on} End(G,P)" using Group_ZF_2_1_L7 unfolding End_def IsCommutative_def by auto qed text‹For the endomorphisms of a group $G$ the group operation lifted to the function space over $G$ is distributive with respect to the composition operation. › lemma (in abelian_group) distributive_comp_pointwise: assumes "F = P {lifted to function space over} G" shows "IsDistributive(End(G,P),InEnd(F,G,P),InEnd(Composition(G),G,P))" proof - let ?C⇩_{G}= "Composition(G)" let ?C⇩_{E}= "InEnd(?C⇩_{G},G,P)" let ?F⇩_{E}= "InEnd(F,G,P)" { fix b c d assume AS: "b∈End(G,P)" "c∈End(G,P)" "d∈End(G,P)" with assms(1) have ig1: "?C⇩_{G}`⟨b, F ` ⟨c, d⟩⟩ = b O (F`⟨c,d⟩)" using monoid.Group_ZF_2_1_L0 func_ZF_5_L2 unfolding End_def by auto with AS have ig2: "F`⟨?C⇩_{G}`⟨b,c⟩,?C⇩_{G}`⟨b,d⟩⟩ = F`⟨b O c,b O d⟩" unfolding End_def using func_ZF_5_L2 by auto from assms(1) AS have comp1fun: "(b O (F`⟨c,d⟩)):G→G" using monoid.Group_ZF_2_1_L0 comp_fun unfolding End_def by force from assms(1) AS have comp2fun: "(F `⟨b O c,b O d⟩) : G→G" using monoid.Group_ZF_2_1_L0 comp_fun unfolding End_def by force { fix g assume "g∈G" with assms(1) AS(2,3) have "(b O (F`⟨c,d⟩))`(g) = b`((F`⟨c,d⟩)`(g))" using comp_fun_apply monoid.Group_ZF_2_1_L0 unfolding End_def by force with groupAssum assms(1) AS ‹g∈G› have "(b O (F`⟨c,d⟩))`(g) = (F`⟨b O c,b O d⟩)`(g)" using Group_ZF_2_1_L3 apply_type homomor_eq comp_fun unfolding End_def by auto } hence "∀g∈G. (b O (F`⟨c,d⟩))`(g) = (F`⟨b O c,b O d⟩)`(g)" by simp with comp1fun comp2fun ig1 ig2 have "?C⇩_{G}`⟨b,F`⟨c, d⟩⟩ = F`⟨?C⇩_{G}`⟨b , c⟩,?C⇩_{G}`⟨b,d⟩⟩" using func_eq by simp moreover from AS(2,3) have "F`⟨c, d⟩ = ?F⇩_{E}`⟨c, d⟩" using restrict by simp moreover from AS have "?C⇩_{G}`⟨b,c⟩ = ?C⇩_{E}`⟨b,c⟩" and "?C⇩_{G}`⟨b,d⟩ = ?C⇩_{E}`⟨b,d⟩" using restrict by auto moreover from assms AS have "?C⇩_{G}`⟨b,F `⟨c,d⟩⟩ = ?C⇩_{E}`⟨b, F`⟨c, d⟩⟩" using end_pointwise_addition by simp moreover from AS have "F`⟨?C⇩_{G}`⟨b,c⟩,?C⇩_{G}`⟨b,d⟩⟩ = ?F⇩_{E}`⟨?C⇩_{G}`⟨b,c⟩,?C⇩_{G}`⟨b,d⟩⟩" using end_composition by simp ultimately have eq1: "?C⇩_{E}`⟨b, ?F⇩_{E}`⟨c,d⟩⟩ = ?F⇩_{E}`⟨?C⇩_{E}`⟨b,c⟩,?C⇩_{E}`⟨b,d⟩⟩" by simp from assms(1) AS have compfun: "(F`⟨c,d⟩) O b : G→G" "F`⟨c O b,d O b⟩ : G→G" using monoid.Group_ZF_2_1_L0 comp_fun unfolding End_def by auto { fix g assume "g∈G" with AS(1) have bg: "b`(g) ∈ G" unfolding End_def using apply_type by auto from ‹g∈G› AS(1) have "((F`⟨c,d⟩) O b)`g = (F`⟨c,d⟩)`(b`(g))" using comp_fun_apply unfolding End_def by force also from assms(1) AS(2,3) bg have "… = (c`(b`(g)))⋅(d`(b`(g)))" using Group_ZF_2_1_L3 unfolding End_def by auto also from ‹g∈G› AS have "… = ((c O b)`(g))⋅((d O b)`(g))" using comp_fun_apply unfolding End_def by auto also from assms(1) ‹g∈G› AS have "… = (F`⟨c O b,d O b⟩)`g" using comp_fun Group_ZF_2_1_L3 unfolding End_def by auto finally have "((F`⟨c,d⟩) O b)`(g) = (F`⟨c O b,d O b⟩)`(g)" by simp } hence "∀g∈G. ((F`⟨c,d⟩) O b)`(g) = (F`⟨c O b,d O b⟩)`(g)" by simp with compfun have "(F`⟨c,d⟩) O b = F`⟨c O b,d O b⟩" using func_eq by blast with assms(1) AS have "?C⇩_{G}`⟨F`⟨c,d⟩,b⟩ = F`⟨?C⇩_{G}`⟨c,b⟩,?C⇩_{G}`⟨d , b⟩⟩" using monoid.Group_ZF_2_1_L0 func_ZF_5_L2 unfolding End_def by simp moreover from AS(2,3) have "F`⟨c, d⟩ = ?F⇩_{E}`⟨c, d⟩" using restrict by simp moreover from AS have "?C⇩_{G}`⟨c,b⟩ = ?C⇩_{E}`⟨c , b⟩" "?C⇩_{G}`⟨d,b⟩ = ?C⇩_{E}`⟨d,b⟩" using restrict by auto moreover from assms AS have "?C⇩_{G}`⟨F`⟨c,d⟩,b⟩ = ?C⇩_{E}`⟨F`⟨c,d⟩,b⟩" using end_pointwise_addition by auto moreover from AS have "F`⟨?C⇩_{G}`⟨c,b⟩,?C⇩_{G}`⟨d,b⟩⟩ = ?F⇩_{E}`⟨?C⇩_{G}`⟨c,b⟩,?C⇩_{G}`⟨d,b⟩⟩" using end_composition by auto ultimately have "?C⇩_{E}`⟨?F⇩_{E}`⟨c,d⟩,b⟩ = ?F⇩_{E}`⟨?C⇩_{E}`⟨c,b⟩,?C⇩_{E}`⟨d,b⟩⟩" by auto with eq1 have "(?C⇩_{E}`⟨b, ?F⇩_{E}`⟨c, d⟩⟩ = ?F⇩_{E}`⟨?C⇩_{E}`⟨b,c⟩,?C⇩_{E}`⟨b,d⟩⟩) ∧ (?C⇩_{E}`⟨?F⇩_{E}`⟨c,d⟩,b⟩ = ?F⇩_{E}`⟨?C⇩_{E}`⟨c,b⟩,?C⇩_{E}`⟨d,b⟩⟩)" by auto } then show ?thesis unfolding IsDistributive_def by auto qed text‹The endomorphisms of an abelian group is in fact a ring with the previous operations.› theorem (in abelian_group) end_is_ring: assumes "F = P {lifted to function space over} G" shows "IsAring(End(G,P),InEnd(F,G,P),InEnd(Composition(G),G,P))" using assms end_addition_group end_comp_monoid(1) distributive_comp_pointwise unfolding IsAring_def by auto text‹The theorems proven in the ‹ring0› context are valid in the ‹abelian_group› context as applied to the endomorphisms of $G$. › sublocale abelian_group < endo_ring: ring0 "End(G,P)" "InEnd(P {lifted to function space over} G,G,P)" "InEnd(Composition(G),G,P)" "λx b. InEnd(P {lifted to function space over} G,G,P)`⟨x,b⟩" "λx. GroupInv(End(G, P), InEnd(P {lifted to function space over} G,G,P))`(x)" "λx b. InEnd(P {lifted to function space over} G,G,P)`⟨x, GroupInv(End(G, P), InEnd(P {lifted to function space over} G,G,P))`(b)⟩" "λx b. InEnd(Composition(G),G,P)`⟨x, b⟩" "TheNeutralElement(End(G, P),InEnd(P {lifted to function space over} G,G,P))" "TheNeutralElement(End(G, P),InEnd(Composition(G),G,P))" "InEnd(P {lifted to function space over} G,G,P)` ⟨TheNeutralElement (End(G, P), InEnd(Composition(G),G,P)), TheNeutralElement (End(G, P), InEnd(Composition(G),G,P))⟩" "λx. InEnd(Composition(G),G,P)`⟨x, x⟩" using end_is_ring unfolding ring0_def by blast subsection‹First isomorphism theorem› text‹Now we will prove that any homomorphism $f:G\to H$ defines a bijective homomorphism between $G/H$ and $f(G)$.› text‹A group homomorphism sends the neutral element to the neutral element.› lemma image_neutral: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" shows "f`(TheNeutralElement(G,P)) = TheNeutralElement(H,F)" proof - let ?e⇩_{G}= "TheNeutralElement(G,P)" let ?e⇩_{H}= "TheNeutralElement(H,F)" have g: "?e⇩_{G}= P`⟨?e⇩_{G},?e⇩_{G}⟩" "?e⇩_{G}∈ G" using assms(1) group0.group0_2_L2 unfolding group0_def by simp_all with assms have "f`(?e⇩_{G}) = F`⟨f`(?e⇩_{G}),f`(?e⇩_{G})⟩" using Homomor_def by force moreover from assms(4) g(2) have h: "f`(?e⇩_{G}) ∈ H" using apply_type by simp with assms(2) have "f`(?e⇩_{G}) = F`⟨f`(?e⇩_{G}),?e⇩_{H}⟩" using group0.group0_2_L2 unfolding group0_def by simp ultimately have "F`⟨f`(?e⇩_{G}),?e⇩_{H}⟩ = F`⟨f`(?e⇩_{G}),f`(?e⇩_{G})⟩" by simp with assms(2) h have "LeftTranslation(H,F,f`(?e⇩_{G}))`(?e⇩_{H}) = LeftTranslation(H,F,f`(?e⇩_{G}))`(f`(?e⇩_{G}))" using group0.group0_5_L2(2) group0.group0_2_L2 unfolding group0_def by simp moreover from assms(2) h have "LeftTranslation(H,F,f`(?e⇩_{G}))∈inj(H,H)" using group0.trans_bij(2) unfolding group0_def bij_def by simp ultimately show ?thesis using h assms(2) group0.group0_2_L2 unfolding inj_def group0_def by force qed text‹If $f:G\rightarrow H$ is a homomorphism, then it commutes with the inverse › lemma image_inv: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" "g∈G" shows "f`(GroupInv(G,P)`(g)) = GroupInv(H,F)`(f`(g))" proof- from assms(4,5) have im: "f`(g)∈H" using apply_type by simp from assms(1,5) have inv: "GroupInv(G,P)`(g)∈G" using group0.inverse_in_group unfolding group0_def by simp with assms(4) have inv2: "f`(GroupInv(G,P)`g)∈H" using apply_type by simp from assms(1,5) have "f`(TheNeutralElement(G,P)) = f`(P`⟨g,GroupInv(G,P)`(g)⟩)" using group0.group0_2_L6 unfolding group0_def by simp also from assms(1,2,3,5) inv have "… = F`⟨f`(g),f`(GroupInv(G,P)`(g))⟩" using Homomor_def by simp finally have "f`(TheNeutralElement(G,P)) = F`⟨f`(g),f`(GroupInv(G,P)`(g))⟩" by simp with assms(1-4) im inv2 show ?thesis using group0.group0_2_L9 image_neutral unfolding group0_def by simp qed text‹The preimage of a subgroup is a subgroup› theorem preimage_sub: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" "IsAsubgroup(K,F)" shows "IsAsubgroup(f-``(K),P)" proof - from assms(2) have Hgr: "group0(H,F)" unfolding group0_def by simp from assms(1) have Ggr: "group0(G,P)" unfolding group0_def by simp moreover from assms Ggr Hgr have "TheNeutralElement(G,P) ∈ f-``(K)" using image_neutral group0.group0_3_L5 func1_1_L15 group0.group0_2_L2 by simp hence "f-``(K)≠0" by blast moreover from assms(4) have "f-``(K) ⊆ G" using func1_1_L3 by simp moreover from assms Ggr Hgr have "f-``(K) {is closed under} P" using func1_1_L15 group0.group0_3_L6 Homomor_def group0.group_op_closed func1_1_L15 unfolding IsOpClosed_def by simp moreover from assms Ggr Hgr have "∀x∈f-``(K). GroupInv(G, P)`(x) ∈ f-``(K)" using group0.group0_3_T3A image_inv func1_1_L15 group0.inverse_in_group by simp ultimately show ?thesis by (rule group0.group0_3_T3) qed text‹The preimage of a normal subgroup is normal› theorem preimage_normal_subgroup: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" "IsAnormalSubgroup(H,F,K)" shows "IsAnormalSubgroup(G,P,f-``(K))" proof - from assms(2) have Hgr: "group0(H,F)" unfolding group0_def by simp with assms(5) have "K⊆H" using group0.group0_3_L2 unfolding IsAnormalSubgroup_def by simp from assms(1) have Ggr: "group0(G,P)" unfolding group0_def by simp moreover from assms have "IsAsubgroup(f-``(K),P)" using preimage_sub unfolding IsAnormalSubgroup_def by simp moreover { fix g assume gG: "g∈G" { fix h assume "h ∈ {P`⟨g,P`⟨h, GroupInv(G, P)`(g)⟩⟩. h ∈ f-``(K)}" then obtain k where k: "h = P`⟨g,P`⟨k,GroupInv(G, P)`(g)⟩⟩" "k ∈ f-``(K)" by auto from k(1) have "f`(h) = f`(P`⟨g,P`⟨k, GroupInv(G, P)`(g)⟩⟩)" by simp moreover from assms(4) k(2) have "k∈G" using vimage_iff unfolding Pi_def by blast ultimately have f: "f`(h) = F`⟨f`(g),F`⟨f`(k),GroupInv(H,F)`(f`(g))⟩⟩" using assms(1-4) Ggr gG group0.group_op_closed group0.inverse_in_group image_inv homomor_eq by simp from assms(1,4) Ggr ‹g∈G› k have "h∈G" using group0.group_op_closed group0.inverse_in_group func1_1_L15 by simp from assms(4,5) k(2) ‹g∈G› have "f`(k)∈K" "f`(g)∈H" and "F`⟨F`⟨f`(g),f`(k)⟩,GroupInv(H,F)`(f`(g))⟩ ∈ K" using func1_1_L15 apply_type unfolding IsAnormalSubgroup_def by auto moreover from ‹f`(k)∈K› ‹K⊆H› Hgr f ‹f`(g)∈H› have "f`(h) = F`⟨F`⟨f`(g),f`(k)⟩,GroupInv(H,F)`(f`(g))⟩" using group0.group_oper_assoc group0.inverse_in_group by auto ultimately have "f`(h) ∈ K" by simp with assms(4) ‹h∈G› have "h ∈ f-``(K)" using func1_1_L15 by simp } hence "{P`⟨g,P`⟨h,GroupInv(G,P)`(g)⟩⟩. h∈f-``(K)} ⊆ f-``(K)" by blast } hence "∀g∈G. {P`⟨g, P`⟨h, GroupInv(G, P)`(g)⟩⟩. h∈f-``(K)} ⊆ f-``(K)" by simp ultimately show ?thesis using group0.cont_conj_is_normal by simp qed text‹The kernel of an homomorphism is a normal subgroup.› corollary kernel_normal_sub: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" shows "IsAnormalSubgroup(G,P,f-``{TheNeutralElement(H,F)})" using assms preimage_normal_subgroup group0.trivial_normal_subgroup unfolding group0_def by auto text‹The image of a subgroup is a subgroup› theorem image_subgroup: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" "IsAsubgroup(K,P)" shows "IsAsubgroup(f``K,F)" proof - from assms(1,5) have sub: "K⊆G" using group0.group0_3_L2 unfolding group0_def by simp from assms(2) have "group0(H,F)" unfolding group0_def by simp moreover from assms(4) have "f``(K) ⊆ H" using func_imagedef sub apply_type by auto moreover from assms(1,4,5) sub have "f`(TheNeutralElement(G,P)) ∈ f``(K)" using group0.group0_3_L5 func_imagedef unfolding group0_def by auto hence "f``(K) ≠ 0" by blast moreover { fix x assume "x∈f``(K)" with assms(4) sub obtain q where q: "q∈K" "x=f`(q)" using func_imagedef by auto with assms(1-4) sub have "GroupInv(H,F)`(x) = f`(GroupInv(G,P)`q)" using image_inv by auto with assms(1,4,5) q(1) sub have "GroupInv(H,F)`(x) ∈ f``(K)" using group0.group0_3_T3A func_imagedef unfolding group0_def by auto } hence "∀x∈f``(K). GroupInv(H, F)`(x) ∈ f``(K)" by auto moreover { fix x y assume "x∈f``(K)" "y∈f``(K)" with assms(4) sub obtain q⇩_{x}q⇩_{y}where q: "q⇩_{x}∈K" "x=f`(q⇩_{x})" "q⇩_{y}∈K" "y=f`(q⇩_{y})" using func_imagedef by auto with assms(1-3) sub have "F`⟨x,y⟩ = f`(P`⟨q⇩_{x},q⇩_{y}⟩)" using homomor_eq by force moreover from assms(1,5) q(1,3) have "P`⟨q⇩_{x},q⇩_{y}⟩ ∈ K" using group0.group0_3_L6 unfolding group0_def by simp ultimately have "F`⟨x,y⟩ ∈ f``(K)" using assms(4) sub func_imagedef by auto } then have "f``(K) {is closed under} F" unfolding IsOpClosed_def by simp ultimately show ?thesis using group0.group0_3_T3 by simp qed text‹The image of a group under a homomorphism is a subgroup of the target group.› corollary image_group: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" shows "IsAsubgroup(f``(G),F)" proof - from assms(1) have "restrict(P,G×G) = P" using group0.group_oper_fun restrict_domain unfolding group0_def by blast with assms show ?thesis using image_subgroup unfolding IsAsubgroup_def by simp qed text‹Now we are able to prove the first isomorphism theorem. This theorem states that any group homomorphism $f:G\to H$ gives an isomorphism between a quotient group of $G$ and a subgroup of $H$.› theorem isomorphism_first_theorem: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" defines "r ≡ QuotientGroupRel(G,P,f-``{TheNeutralElement(H,F)})" and "𝒫 ≡ QuotientGroupOp(G,P,f-``{TheNeutralElement(H,F)})" shows "∃𝔣. Homomor(𝔣,G//r,𝒫,f``(G),restrict(F,(f``(G))×(f``(G)))) ∧ 𝔣∈bij(G//r,f``(G))" proof- let ?𝔣 = "{⟨r``{g},f`(g)⟩. g∈G}" from assms(1-5) have "equiv(G,r)" using group0.Group_ZF_2_4_L3 kernel_normal_sub unfolding group0_def IsAnormalSubgroup_def by simp from assms(4,5) have "?𝔣 ∈ Pow((G//r)×f``G)" unfolding quotient_def using func_imagedef by auto moreover have "(G//r) ⊆ domain(?𝔣)" unfolding domain_def quotient_def by auto moreover { fix x y t assume A: "⟨x,y⟩ ∈ ?𝔣" "⟨x,t⟩ ∈ ?𝔣" then obtain g⇩_{y}g⇩_{r}where "⟨x, y⟩=⟨r``{g⇩_{y}},f`(g⇩_{y})⟩" "⟨x, t⟩=⟨r``{g⇩_{r}},f`(g⇩_{r})⟩" and "g⇩_{r}∈G" "g⇩_{y}∈G" by auto hence B: "r``{g⇩_{y}}=r``{g⇩_{r}}" "y=f`(g⇩_{y})" "t=f`(g⇩_{r})" by auto from assms(4) ‹g⇩_{y}∈G› ‹g⇩_{r}∈G› B(2,3) have "y∈H" "t∈H" using apply_type by simp_all with ‹equiv(G,r)› ‹g⇩_{r}∈G› ‹r``{g⇩_{y}}=r``{g⇩_{r}}› have "⟨g⇩_{y},g⇩_{r}⟩∈r" using same_image_equiv by simp with assms(4,5) have "f`(P`⟨g⇩_{y},GroupInv(G,P)`(g⇩_{r})⟩) = TheNeutralElement(H,F)" unfolding QuotientGroupRel_def using func1_1_L15 by simp with assms(1-4) B(2,3) ‹g⇩_{y}∈G› ‹g⇩_{r}∈G› ‹y∈H› ‹t∈H› have "y=t" using image_inv Homomor_def group0.inverse_in_group group0.group0_2_L11A unfolding group0_def by auto } hence "∀x y. ⟨x,y⟩ ∈ ?𝔣 ⟶ (∀z. ⟨x,z⟩∈?𝔣 ⟶ y=z)" by auto ultimately have ff_fun: "?𝔣:G//r→f``(G)" unfolding Pi_def function_def by auto { fix a⇩_{1}a⇩_{2}assume AS: "a⇩_{1}∈G//r" "a⇩_{2}∈G//r" then obtain g⇩_{1}g⇩_{2}where "g⇩_{1}∈G" "g⇩_{2}∈G" and a: "a⇩_{1}=r``{g⇩_{1}}" "a⇩_{2}=r``{g⇩_{2}}" unfolding quotient_def by auto with assms ‹equiv(G,r)› have "⟨𝒫`⟨a⇩_{1},a⇩_{2}⟩,f`(P`⟨g⇩_{1},g⇩_{2}⟩)⟩ ∈ ?𝔣" using Group_ZF_2_4_L5A kernel_normal_sub group0.Group_ZF_2_2_L2 group0.group_op_closed unfolding QuotientGroupOp_def group0_def by auto with ff_fun have eq: "?𝔣`(𝒫`⟨a⇩_{1},a⇩_{2}⟩) = f`(P`⟨g⇩_{1},g⇩_{2}⟩)" using apply_equality by simp from ‹g⇩_{1}∈G› ‹g⇩_{2}∈G› a have "⟨a⇩_{1},f`(g⇩_{1})⟩ ∈ ?𝔣" and "⟨a⇩_{2},f`(g⇩_{2})⟩ ∈ ?𝔣" by auto with assms(1,2,3) ff_fun ‹g⇩_{1}∈G› ‹g⇩_{2}∈G› eq have "F`⟨?𝔣`(a⇩_{1}),?𝔣`(a⇩_{2})⟩ = ?𝔣`(𝒫`⟨a⇩_{1},a⇩_{2}⟩)" using apply_equality Homomor_def by simp moreover from AS ff_fun have "?𝔣`(a⇩_{1}) ∈ f``(G)" "?𝔣`(a⇩_{2}) ∈ f``(G)" using apply_type by auto ultimately have "restrict(F,f``(G)×f``(G))`⟨?𝔣`(a⇩_{1}),?𝔣`(a⇩_{2})⟩ = ?𝔣`(𝒫`⟨a⇩_{1},a⇩_{2}⟩)" by simp } hence r: "∀a⇩_{1}∈G//r. ∀a⇩_{2}∈G//r. restrict(F,f``G×f``G)`⟨?𝔣`a⇩_{1},?𝔣`a⇩_{2}⟩ = ?𝔣`(𝒫`⟨a⇩_{1},a⇩_{2}⟩)" by simp moreover from assms have G: "IsAgroup(G//r,𝒫)" using Group_ZF_2_4_T1 kernel_normal_sub by simp moreover from assms(1-4) have H: "IsAgroup(f``(G), restrict(F,f``(G)×f``(G)))" using image_group unfolding IsAsubgroup_def by simp ultimately have HOM: "Homomor(?𝔣,G//r,𝒫,f``(G),restrict(F,(f``(G))×(f``(G))))" using Homomor_def by simp { fix b⇩_{1}b⇩_{2}assume AS: "?𝔣`(b⇩_{1}) = ?𝔣`(b⇩_{2})" "b⇩_{1}∈G//r" "b⇩_{2}∈G//r" from G AS(3) have invb2: "GroupInv(G//r,𝒫)`(b⇩_{2})∈G//r" using group0.inverse_in_group unfolding group0_def by simp with G AS(2) have I: "𝒫`⟨b⇩_{1},GroupInv(G//r,𝒫)`(b⇩_{2})⟩∈G//r" using group0.group_op_closed unfolding group0_def by auto then obtain g where "g∈G" and gg: "𝒫`⟨b⇩_{1},GroupInv(G//r,𝒫)`(b⇩_{2})⟩=r``{g}" unfolding quotient_def by auto from ‹g∈G› have "⟨r``{g},f`(g)⟩ ∈ ?𝔣" by blast with ff_fun gg have E: "?𝔣`(𝒫`⟨b⇩_{1},GroupInv(G//r,𝒫)`(b⇩_{2})⟩) = f`(g)" using apply_equality by simp from ff_fun invb2 have pp: "?𝔣`(GroupInv(G//r,𝒫)`(b⇩_{2}))∈f``(G)" using apply_type by simp from ff_fun AS(2,3) have fff: "?𝔣`(b⇩_{1}) ∈ f``(G)" "?𝔣`(b⇩_{2}) ∈ f``(G)" using apply_type by simp_all from fff(1) pp have EE: "F`⟨?𝔣`(b⇩_{1}),?𝔣`(GroupInv(G//r,𝒫)`(b⇩_{2}))⟩= restrict(F,f``(G)×f``(G))`⟨?𝔣`(b⇩_{1}),?𝔣`(GroupInv(G//r,𝒫)`(b⇩_{2}))⟩" by auto from assms(4) have "f``(G) ⊆ H" using func1_1_L6(2) by simp with fff have "?𝔣`(b⇩_{1})∈H" "?𝔣`(b⇩_{2})∈H" by auto with assms(1-4) G H HOM ff_fun AS(1,3) fff(2) EE have "TheNeutralElement(H,F) = restrict(F,f``(G)×f``(G))`⟨?𝔣`(b⇩_{1}),?𝔣`(GroupInv(G//r,𝒫)`(b⇩_{2}))⟩" using group0.group0_2_L6(1) restrict image_inv group0.group0_3_T1 image_group unfolding group0_def by simp also from G H HOM AS(2,3) E have "… = f`(g)" using Homomor_def group0.inverse_in_group unfolding group0_def by simp finally have "TheNeutralElement(H,F) = f`(g)" by simp with assms(4) ‹g∈G› have "g∈f-``{TheNeutralElement(H,F)}" using func1_1_L15 by simp with assms ‹g∈G› gg have "𝒫`⟨b⇩_{1},GroupInv(G//r,𝒫)`(b⇩_{2})⟩ = TheNeutralElement(G//r,𝒫)" using group0.Group_ZF_2_4_L5E kernel_normal_sub unfolding group0_def by simp with AS(2,3) G have "b⇩_{1}=b⇩_{2}" using group0.group0_2_L11A unfolding group0_def by auto } with ff_fun have "?𝔣 ∈ inj(G//r,f``(G))" unfolding inj_def by blast moreover { fix m assume "m ∈ f``(G)" with assms(4) obtain g where "g∈G" "m=f`(g)" using func_imagedef by auto hence "⟨r``{g},m⟩ ∈ ?𝔣" by blast with ff_fun have "?𝔣`(r``{g})=m" using apply_equality by auto with ‹g∈G› have "∃A∈G//r. ?𝔣`(A) = m" unfolding quotient_def by auto } ultimately have "?𝔣 ∈ bij(G//r,f``G)" unfolding bij_def surj_def using ff_fun by blast with HOM show ?thesis by blast qed text‹The inverse of a bijective homomorphism is an homomorphism. Meaning that in the previous result, the homomorphism we found is an isomorphism.› theorem bij_homomor: assumes "f∈bij(G,H)" "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" shows "Homomor(converse(f),H,F,G,P)" proof- { fix h⇩_{1}h⇩_{2}assume "h⇩_{1}∈H" "h⇩_{2}∈H" with assms(1) obtain g⇩_{1}g⇩_{2}where g1: "g⇩_{1}∈G" "f`(g⇩_{1})=h⇩_{1}" and g2: "g⇩_{2}∈G" "f`(g⇩_{2})=h⇩_{2}" unfolding bij_def surj_def by blast with assms(2,3,4) have "converse(f)`(f`(P`⟨g⇩_{1},g⇩_{2}⟩)) = converse(f)`(F`⟨h⇩_{1},h⇩_{2}⟩)" using homomor_eq by simp with assms(1,2) g1 g2 have "P`⟨converse(f)`(h⇩_{1}),converse(f)`(h⇩_{2})⟩ = converse(f)`(F`⟨h⇩_{1},h⇩_{2}⟩)" using left_inverse group0.group_op_closed unfolding group0_def bij_def by auto } with assms(2,3) show ?thesis using Homomor_def by simp qed text‹A very important homomorphism is given by taking every element to its class in a group quotient. Recall that $\lambda x\in X. p(x)$ is an alternative notation for function defined as a set of pairs, see lemma ‹lambda_fun_alt› in theory ‹func1.thy›.› lemma (in group0) quotient_map: assumes "IsAnormalSubgroup(G,P,H)" defines "r ≡ QuotientGroupRel(G,P,H)" and "q ≡ λx∈G. QuotientGroupRel(G,P,H)``{x}" shows "Homomor(q,G,P,G//r,QuotientGroupOp(G,P,H))" using groupAssum assms group_op_closed lam_funtype lamE EquivClass_1_L10 Group_ZF_2_4_L3 Group_ZF_2_4_L5A Homomor_def Group_ZF_2_4_T1 unfolding IsAnormalSubgroup_def QuotientGroupOp_def by simp text‹In the context of ‹group0›, we may use all results of ‹semigr0›.› sublocale group0 < semigroup:semigr0 G P groper "λx. Fold1(P,x)" Append Concat unfolding semigr0_def using groupAssum IsAgroup_def IsAmonoid_def by auto end