(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013 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 4› theory Group_ZF_4 imports Group_ZF_1 Group_ZF_2 Finite_ZF Ring_ZF Cardinal_ZF Semigroup_ZF begin text{*This theory file deals with normal subgroup test and some finite group theory. Then we define group homomorphisms and prove that the set of endomorphisms forms a ring with unity and we also prove the first isomorphism theorem.*} subsection{*Conjugation of subgroups*} text{*The conjugate of a subgroup is a subgroup.*} theorem(in group0) semigr0: shows "semigr0(G,P)" unfolding semigr0_def using groupAssum IsAgroup_def IsAmonoid_def by auto theorem (in group0) conj_group_is_group: assumes "IsAsubgroup(H,P)" "g∈G" shows "IsAsubgroup({g⋅(h⋅g¯). h∈H},P)" proof- have sub:"H⊆G" using assms(1) group0_3_L2 by auto from assms(2) have "g¯∈G" using inverse_in_group by auto { fix r assume "r∈{g⋅(h⋅g¯). h∈H}" then obtain h where h:"h∈H" "r=g⋅(h⋅(g¯))" by auto from h(1) have "h¯∈H" using group0_3_T3A assms(1) by auto from h(1) sub have "h∈G" by auto then have "h¯∈G" using inverse_in_group by auto with `g¯∈G` have "((h¯)⋅(g)¯)∈G" using group_op_closed by auto from h(2) have "r¯=(g⋅(h⋅(g¯)))¯" by auto moreover from `h∈G` `g¯∈G` have s:"h⋅(g¯)∈G" using group_op_closed by blast ultimately have "r¯=(h⋅(g¯))¯⋅(g)¯" using group_inv_of_two[OF assms(2)] by auto moreover from s assms(2) h(2) have r:"r∈G" using group_op_closed by auto have "(h⋅(g¯))¯=(g¯)¯⋅h¯" using group_inv_of_two[OF `h∈G``g¯∈G`] by auto moreover have "(g¯)¯=g" using group_inv_of_inv[OF assms(2)] by auto ultimately have "r¯=(g⋅(h¯))⋅(g)¯" by auto then have "r¯=g⋅((h¯)⋅(g)¯)" using group_oper_assoc[OF assms(2) `h¯∈G``g¯∈G`] by auto with `h¯∈H` r have "r¯∈{g⋅(h⋅g¯). h∈H}" "r∈G" by auto } then have "∀r∈{g⋅(h⋅g¯). h∈H}. r¯∈{g⋅(h⋅g¯). h∈H}" and "{g⋅(h⋅g¯). h∈H}⊆G" by auto moreover { fix s t assume s:"s∈{g⋅(h⋅g¯). h∈H}" and t:"t∈{g⋅(h⋅g¯). h∈H}" then obtain hs ht where hs:"hs∈H" "s=g⋅(hs⋅(g¯))" and ht:"ht∈H" "t=g⋅(ht⋅(g¯))" by auto from hs(1) have "hs∈G" using sub by auto then have "g⋅hs∈G" using group_op_closed assms(2) by auto then have "(g⋅hs)¯∈G" using inverse_in_group by auto from ht(1) have "ht∈G" using sub by auto with `g¯:G` have "ht⋅(g¯)∈G" using group_op_closed by auto from hs(2) ht(2) have "s⋅t=(g⋅(hs⋅(g¯)))⋅(g⋅(ht⋅(g¯)))" by auto moreover have "g⋅(hs⋅(g¯))=g⋅hs⋅(g¯)" using group_oper_assoc[OF assms(2) `hs∈G` `g¯∈G`] by auto then have "(g⋅(hs⋅(g¯)))⋅(g⋅(ht⋅(g¯)))=(g⋅hs⋅(g¯))⋅(g⋅(ht⋅(g¯)))" by auto then have "(g⋅(hs⋅(g¯)))⋅(g⋅(ht⋅(g¯)))=(g⋅hs⋅(g¯))⋅(g¯¯⋅(ht⋅(g¯)))" using group_inv_of_inv[OF assms(2)] by auto also have "…=g⋅hs⋅(ht⋅(g¯))" using group0_2_L14A(2)[OF `(g⋅hs)¯∈G` `g¯∈G``ht⋅(g¯)∈G`] group_inv_of_inv[OF `(g⋅hs)∈G`] by auto ultimately have "s⋅t=g⋅hs⋅(ht⋅(g¯))" by auto moreover have "hs⋅(ht⋅(g¯))=(hs⋅ht)⋅(g¯)" using group_oper_assoc[OF `hs∈G``ht∈G``g¯∈G`] by auto moreover have "g⋅hs⋅(ht⋅(g¯))=g⋅(hs⋅(ht⋅(g¯)))" using group_oper_assoc[OF `g∈G``hs∈G``(ht⋅g¯)∈G`] by auto ultimately have "s⋅t=g⋅((hs⋅ht)⋅(g¯))" by auto moreover from hs(1) ht(1) have "hs⋅ht∈H" using assms(1) group0_3_L6 by auto ultimately have "s⋅t∈{g⋅(h⋅g¯). h∈H}" by auto } then have "{g⋅(h⋅g¯). h∈H} {is closed under}P" unfolding IsOpClosed_def by auto moreover from assms(1) have "𝟭∈H" using group0_3_L5 by auto then have "g⋅(𝟭⋅g¯)∈{g⋅(h⋅g¯). h∈H}" by auto then have "{g⋅(h⋅g¯). h∈H}≠0" by auto ultimately show ?thesis using group0_3_T3 by auto qed text{*Every set is equipollent with its conjugates.*} theorem (in group0) conj_set_is_eqpoll: assumes "H⊆G" "g∈G" shows "H≈{g⋅(h⋅g¯). h∈H}" proof- have fun:"{⟨h,g⋅(h⋅g¯)⟩. h∈H}:H→{g⋅(h⋅g¯). h∈H}" unfolding Pi_def function_def domain_def by auto { fix h1 h2 assume "h1∈H""h2∈H""{⟨h,g⋅(h⋅g¯)⟩. h∈H}`h1={⟨h,g⋅(h⋅g¯)⟩. h∈H}`h2" with fun have "g⋅(h1⋅g¯)=g⋅(h2⋅g¯)""h1⋅g¯∈G""h2⋅g¯∈G""h1∈G""h2∈G" using apply_equality assms(1) group_op_closed[OF _ inverse_in_group[OF assms(2)]] by auto then have "h1⋅g¯=h2⋅g¯" using group0_2_L19(2)[OF `h1⋅g¯∈G` `h2⋅g¯∈G` assms(2)] by auto then have "h1=h2" using group0_2_L19(1)[OF `h1∈G``h2∈G` inverse_in_group[OF assms(2)]] by auto } then have "∀h1∈H. ∀h2∈H. {⟨h,g⋅(h⋅g¯)⟩. h∈H}`h1={⟨h,g⋅(h⋅g¯)⟩. h∈H}`h2 ⟶ h1=h2" by auto with fun have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}∈inj(H,{g⋅(h⋅g¯). h∈H})" unfolding inj_def by auto moreover { fix ghg assume "ghg∈{g⋅(h⋅g¯). h∈H}" then obtain h where "h∈H" "ghg=g⋅(h⋅g¯)" by auto then have "⟨h,ghg⟩∈{⟨h,g⋅(h⋅g¯)⟩. h∈H}" by auto then have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}`h=ghg" using apply_equality fun by auto with `h∈H` have "∃h∈H. {⟨h,g⋅(h⋅g¯)⟩. h∈H}`h=ghg" by auto } with fun have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}∈surj(H,{g⋅(h⋅g¯). h∈H})" unfolding surj_def by auto ultimately have "{⟨h,g⋅(h⋅g¯)⟩. h∈H}∈bij(H,{g⋅(h⋅g¯). h∈H})" unfolding bij_def by auto then show ?thesis unfolding eqpoll_def by auto qed text{*Every normal subgroup contains its conjugate subgroups.*} theorem (in group0) norm_group_cont_conj: assumes "IsAnormalSubgroup(G,P,H)" "g∈G" shows "{g⋅(h⋅g¯). h∈H}⊆H" proof- { fix r assume "r∈{g⋅(h⋅g¯). h∈H}" then obtain h where "r=g⋅(h⋅g¯)" "h∈H" by auto moreover then have "h∈G" using group0_3_L2 assms(1) unfolding IsAnormalSubgroup_def by auto moreover from assms(2) have "g¯∈G" using inverse_in_group by auto ultimately have "r=g⋅h⋅g¯" "h∈H" using group_oper_assoc assms(2) by auto then have "r∈H" using assms unfolding IsAnormalSubgroup_def by auto } then show "{g⋅(h⋅g¯). h∈H}⊆H" by auto qed text{*If a subgroup contains all its conjugate subgroups, then it is normal.*} theorem (in group0) cont_conj_is_normal: assumes "IsAsubgroup(H,P)" "∀g∈G. {g⋅(h⋅g¯). h∈H}⊆H" shows "IsAnormalSubgroup(G,P,H)" proof- { fix h g assume "h∈H" "g∈G" with assms(2) have "g⋅(h⋅g¯)∈H" by auto moreover have "h∈G""g¯∈G" using group0_3_L2 assms(1) `g∈G``h∈H` inverse_in_group by auto ultimately have "g⋅h⋅g¯∈H" using group_oper_assoc `g∈G` by auto } then show ?thesis using assms(1) unfolding IsAnormalSubgroup_def by auto qed text{*If a group has only one subgroup of a given order, then this subgroup is normal.*} corollary(in group0) only_one_equipoll_sub: assumes "IsAsubgroup(H,P)" "∀M. IsAsubgroup(M,P)∧ H≈M ⟶ M=H" shows "IsAnormalSubgroup(G,P,H)" proof- { fix g assume g:"g∈G" with assms(1) have "IsAsubgroup({g⋅(h⋅g¯). h∈H},P)" using conj_group_is_group by auto moreover from assms(1) g have "H≈{g⋅(h⋅g¯). h∈H}" using conj_set_is_eqpoll group0_3_L2 by auto ultimately have "{g⋅(h⋅g¯). h∈H}=H" using assms(2) by auto then have "{g⋅(h⋅g¯). h∈H}⊆H" by auto } then show ?thesis using cont_conj_is_normal assms(1) by auto qed text{*The trivial subgroup is then a normal subgroup.*} corollary(in group0) trivial_normal_subgroup: shows "IsAnormalSubgroup(G,P,{𝟭})" proof- have "{𝟭}⊆G" using group0_2_L2 by auto moreover have "{𝟭}≠0" by auto moreover { fix a b assume "a∈{𝟭}""b∈{𝟭}" then have "a=𝟭""b=𝟭" by auto then have "P`⟨a,b⟩=𝟭⋅𝟭" by auto then have "P`⟨a,b⟩=𝟭" using group0_2_L2 by auto then have "P`⟨a,b⟩∈{𝟭}" by auto } then have "{𝟭}{is closed under}P" unfolding IsOpClosed_def by auto moreover { fix a assume "a∈{𝟭}" then have "a=𝟭" by auto then have "a¯=𝟭¯" by auto then have "a¯=𝟭" using group_inv_of_one by auto then have "a¯∈{𝟭}" by auto } then have "∀a∈{𝟭}. a¯∈{𝟭}" by auto ultimately have "IsAsubgroup({𝟭},P)" using group0_3_T3 by auto moreover { fix M assume M:"IsAsubgroup(M,P)" "{𝟭}≈M" then have "𝟭∈M" "M≈{𝟭}" using eqpoll_sym group0_3_L5 by auto then obtain f where "f∈bij(M,{𝟭})" unfolding eqpoll_def by auto then have inj:"f∈inj(M,{𝟭})" unfolding bij_def by auto then have fun:"f:M→{𝟭}" unfolding inj_def by auto { fix b assume "b∈M""b≠𝟭" then have "f`b≠f`𝟭" using inj `𝟭∈M` unfolding inj_def by auto then have "False" using `b∈M` `𝟭∈M` apply_type[OF fun] by auto } then have "M={𝟭}" using `𝟭∈M` by auto } ultimately show ?thesis using only_one_equipoll_sub by auto qed lemma(in group0) whole_normal_subgroup: shows "IsAnormalSubgroup(G,P,G)" unfolding IsAnormalSubgroup_def using group_op_closed inverse_in_group using group0_2_L2 group0_3_T3[of "G"] unfolding IsOpClosed_def by auto text{*Since the whole group and the trivial subgroup are normal, it is natural to define simplicity of groups in the following way:*} definition IsSimple ("[_,_]{is a simple group}" 89) where "[G,f]{is a simple group} ≡ IsAgroup(G,f)∧(∀M. IsAnormalSubgroup(G,f,M) ⟶ M=G∨M={TheNeutralElement(G,f)})" text{*From the definition follows that if a group has no subgroups, then it is simple.*} corollary (in group0) noSubgroup_imp_simple: assumes "∀H. IsAsubgroup(H,P)⟶ H=G∨H={𝟭}" shows "[G,P]{is a simple group}" proof- have "IsAgroup(G,P)" using groupAssum. moreover { fix M assume "IsAnormalSubgroup(G,P,M)" then have "IsAsubgroup(M,P)" unfolding IsAnormalSubgroup_def by auto with assms have "M=G∨M={𝟭}" by auto } ultimately show ?thesis unfolding IsSimple_def by auto qed text{*Since every subgroup is normal in abelian groups, it follows that commutative simple groups do not have subgroups.*} corollary (in group0) abelian_simple_noSubgroups: assumes "[G,P]{is a simple group}" "P{is commutative on}G" shows "∀H. IsAsubgroup(H,P)⟶ H=G∨H={𝟭}" proof(safe) fix H assume A:"IsAsubgroup(H,P)""H ≠ {𝟭}" then have "IsAnormalSubgroup(G,P,H)" using Group_ZF_2_4_L6(1) groupAssum assms(2) by auto with assms(1) A show "H=G" unfolding IsSimple_def by auto qed subsection{*Finite groups*} text{*The subgroup of a finite group is finite.*} lemma(in group0) finite_subgroup: assumes "Finite(G)" "IsAsubgroup(H,P)" shows "Finite(H)" using group0_3_L2 subset_Finite assms by force text{*The space of cosets is also finite. In particular, quotient groups.*} lemma(in group0) finite_cosets: assumes "Finite(G)" "IsAsubgroup(H,P)" "r=QuotientGroupRel(G,P,H)" shows "Finite(G//r)" proof- have fun:"{⟨g,r``{g}⟩. g∈G}:G→(G//r)" unfolding Pi_def function_def domain_def by auto { fix C assume C:"C∈G//r" then obtain c where c:"c∈C" using EquivClass_1_L5[OF Group_ZF_2_4_L1[OF assms(2)]] assms(3) by auto with C have "r``{c}=C" using EquivClass_1_L2[OF Group_ZF_2_4_L3] assms(2,3) by auto with c C have "⟨c,C⟩∈{⟨g,r``{g}⟩. g∈G}" using EquivClass_1_L1[OF Group_ZF_2_4_L3] assms(2,3) by auto then have "{⟨g,r``{g}⟩. g∈G}`c=C" "c∈G" using apply_equality fun by auto then have "∃c∈G. {⟨g,r``{g}⟩. g∈G}`c=C" by auto } with fun have surj:"{⟨g,r``{g}⟩. g∈G}∈surj(G,G//r)" unfolding surj_def by auto moreover from assms(1) obtain n where "n∈nat" "G≈n" unfolding Finite_def by auto then have G:"G≲n" "Ord(n)" using eqpoll_imp_lepoll by auto then have "G//r≲G" using surj_fun_inv_2 surj by auto with G(1) have "G//r≲n" using lepoll_trans by blast then show "Finite(G//r)" using lepoll_nat_imp_Finite `n∈nat` by auto qed text{*All the cosets are equipollent.*} lemma(in group0) cosets_equipoll: assumes "IsAsubgroup(H,P)" "r=QuotientGroupRel(G,P,H)" "g1∈G""g2∈G" shows "r``{g1}≈r``{g2}" proof- from assms(3,4) have GG:"(g1¯)⋅g2∈G" using inverse_in_group group_op_closed by auto then have "RightTranslation(G,P,(g1¯)⋅g2)∈bij(G,G)" using trans_bij(1) by auto moreover have sub2:"r``{g2}⊆G" using EquivClass_1_L1[OF Group_ZF_2_4_L3[OF assms(1)]] assms(2,4) unfolding quotient_def by auto have sub:"r``{g1}⊆G" using EquivClass_1_L1[OF Group_ZF_2_4_L3[OF assms(1)]] assms(2,3) unfolding quotient_def by auto ultimately have "restrict(RightTranslation(G,P,(g1¯)⋅g2),r``{g1})∈bij(r``{g1},RightTranslation(G,P,(g1¯)⋅g2)``(r``{g1}))" using restrict_bij unfolding bij_def by auto then have "r``{g1}≈RightTranslation(G,P,(g1¯)⋅g2)``(r``{g1})" unfolding eqpoll_def by auto then have A0:"r``{g1}≈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" using func_imagedef[OF group0_5_L1(1)[OF GG] sub] by auto { fix t assume "t∈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" then obtain q where q:"t=RightTranslation(G,P,(g1¯)⋅g2)`q" "q∈r``{g1}" by auto then have "⟨g1,q⟩∈r" "q∈G" using image_iff sub by auto then have "g1⋅(q¯)∈H" "q¯∈G" using assms(2) inverse_in_group unfolding QuotientGroupRel_def by auto from q(1) have t:"t=q⋅((g1¯)⋅g2)" using group0_5_L2(1)[OF GG] q(2) sub by auto then have "g2⋅t¯=g2⋅(q⋅((g1¯)⋅g2))¯" by auto then have "g2⋅t¯=g2⋅(((g1¯)⋅g2)¯⋅q¯)" using group_inv_of_two[OF `q∈G` GG] by auto then have "g2⋅t¯=g2⋅(((g2¯)⋅g1¯¯)⋅q¯)" using group_inv_of_two[OF inverse_in_group[OF assms(3)] assms(4)] by auto then have "g2⋅t¯=g2⋅(((g2¯)⋅g1)⋅q¯)" using group_inv_of_inv assms(3) by auto moreover have "t∈G" using t `q∈G` `g2∈G` inverse_in_group[OF assms(3)] group_op_closed by auto have "(g2¯)⋅g1∈G" using assms(3) inverse_in_group[OF assms(4)] group_op_closed by auto with assms(4) `q¯∈G` have "g2⋅(((g2¯)⋅g1)⋅q¯)=g2⋅((g2¯)⋅g1)⋅q¯" using group_oper_assoc by auto moreover have "g2⋅((g2¯)⋅g1)=g2⋅(g2¯)⋅g1" using assms(3) inverse_in_group[OF assms(4)] assms(4) group_oper_assoc by auto then have "g2⋅((g2¯)⋅g1)=g1" using group0_2_L6[OF assms(4)] group0_2_L2 assms(3) by auto ultimately have "g2⋅t¯=g1⋅q¯" by auto with `g1⋅(q¯)∈H` have "g2⋅t¯∈H" by auto then have "⟨g2,t⟩∈r" using assms(2) unfolding QuotientGroupRel_def using assms(4) `t∈G` by auto then have "t∈r``{g2}" using image_iff assms(4) by auto } then have A1:"{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}⊆r``{g2}" by auto { fix t assume "t∈r``{g2}" then have "⟨g2,t⟩∈r" "t∈G" using sub2 image_iff by auto then have H:"g2⋅t¯∈H" using assms(2) unfolding QuotientGroupRel_def by auto then have G:"g2⋅t¯∈G" using group0_3_L2 assms(1) by auto then have "g1⋅(g1¯⋅(g2⋅t¯))=g1⋅g1¯⋅(g2⋅t¯)" using group_oper_assoc[OF assms(3) inverse_in_group[OF assms(3)]] by auto then have "g1⋅(g1¯⋅(g2⋅t¯))=g2⋅t¯" using group0_2_L6[OF assms(3)] group0_2_L2 G by auto with H have HH:"g1⋅(g1¯⋅(g2⋅t¯))∈H" by auto have GGG:"t⋅g2¯∈G" using `t∈G` inverse_in_group[OF assms(4)] group_op_closed by auto have "(t⋅g2¯)¯=g2¯¯⋅t¯" using group_inv_of_two[OF `t∈G` inverse_in_group[OF assms(4)]] by auto also have "…=g2⋅t¯" using group_inv_of_inv[OF assms(4)] by auto ultimately have "(t⋅g2¯)¯=g2⋅t¯" by auto then have "g1¯⋅(t⋅g2¯)¯=g1¯⋅(g2⋅t¯)" by auto then have "((t⋅g2¯)⋅g1)¯=g1¯⋅(g2⋅t¯)" using group_inv_of_two[OF GGG assms(3)] by auto then have HHH:"g1⋅((t⋅g2¯)⋅g1)¯∈H" using HH by auto have "(t⋅g2¯)⋅g1∈G" using assms(3) `t∈G` inverse_in_group[OF assms(4)] group_op_closed by auto with HHH have "⟨g1,(t⋅g2¯)⋅g1⟩∈r" using assms(2,3) unfolding QuotientGroupRel_def by auto then have rg1:"t⋅g2¯⋅g1∈r``{g1}" using image_iff by auto have "t⋅g2¯⋅g1⋅((g1¯)⋅g2)=t⋅(g2¯⋅g1)⋅((g1¯)⋅g2)" using group_oper_assoc[OF `t∈G` inverse_in_group[OF assms(4)] assms(3)] by auto also have "…=t⋅((g2¯⋅g1)⋅((g1¯)⋅g2))" using group_oper_assoc[OF `t∈G` group_op_closed[OF inverse_in_group[OF assms(4)] assms(3)] GG] by auto also have "…=t⋅(g2¯⋅(g1⋅((g1¯)⋅g2)))" using group_oper_assoc[OF inverse_in_group[OF assms(4)] assms(3) GG] by auto also have "…=t⋅(g2¯⋅(g1⋅(g1¯)⋅g2))" using group_oper_assoc[OF assms(3) inverse_in_group[OF assms(3)] assms(4)] by auto also have "…=t" using group0_2_L6[OF assms(3)]group0_2_L6[OF assms(4)] group0_2_L2 `t∈G` assms(4) by auto ultimately have "t⋅g2¯⋅g1⋅((g1¯)⋅g2)=t" by auto then have "RightTranslation(G,P,(g1¯)⋅g2)`(t⋅g2¯⋅g1)=t" using group0_5_L2(1)[OF GG] `(t⋅g2¯)⋅g1∈G` by auto then have "t∈{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" using rg1 by force } then have "r``{g2}⊆{RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" by blast with A1 have "r``{g2}={RightTranslation(G,P,(g1¯)⋅g2)`t. t∈r``{g1}}" by auto with A0 show ?thesis by auto qed text{*The order of a subgroup multiplied by the order of the space of cosets is the order of the group. We only prove the theorem for finite groups.*} theorem(in group0) Lagrange: assumes "Finite(G)" "IsAsubgroup(H,P)" "r=QuotientGroupRel(G,P,H)" shows "|G|=|H| #* |G//r|" proof- have "Finite(G//r)" using assms finite_cosets by auto moreover have un:"⋃(G//r)=G" using Union_quotient Group_ZF_2_4_L3 assms(2,3) by auto then have "Finite(⋃(G//r))" using assms(1) by auto moreover have "∀c1∈(G//r). ∀c2∈(G//r). c1≠c2 ⟶ c1∩c2=0" using quotient_disj[OF Group_ZF_2_4_L3[OF assms(2)]] assms(3) by auto moreover have "∀aa∈G. aa∈H ⟷ ⟨aa,𝟭⟩∈r" using Group_ZF_2_4_L5C assms(3) by auto then have "∀aa∈G. aa∈H ⟷ ⟨𝟭,aa⟩∈r" using Group_ZF_2_4_L2 assms(2,3) unfolding sym_def by auto then have "∀aa∈G. aa∈H ⟷ aa∈r``{𝟭}" using image_iff by auto then have H:"H=r``{𝟭}" using group0_3_L2[OF assms(2)] assms(3) unfolding QuotientGroupRel_def by auto { fix c assume "c∈(G//r)" then obtain g where "g∈G" "c=r``{g}" unfolding quotient_def by auto then have "c≈r``{𝟭}" using cosets_equipoll[OF assms(2,3)] group0_2_L2 by auto then have "|c|=|H|" using H cardinal_cong by auto } then have "∀c∈(G//r). |c|=|H|" by auto ultimately show ?thesis using card_partition un by auto qed subsection{*Subgroups generated by sets*} text{*Given a subset of a group, we can ask ourselves which is the smallest group that contains that set; if it even exists.*} lemma(in group0) inter_subgroups: assumes "∀H∈ℌ. IsAsubgroup(H,P)" "ℌ≠0" shows "IsAsubgroup(⋂ℌ,P)" proof- from assms have "𝟭∈⋂ℌ" using group0_3_L5 by auto then have "⋂ℌ≠0" by auto moreover { fix A B assume "A∈⋂ℌ""B∈⋂ℌ" then have "∀H∈ℌ. A∈H∧B∈H" by auto then have "∀H∈ℌ. A⋅B∈H" using assms(1) group0_3_L6 by auto then have "A⋅B∈⋂ℌ" using assms(2) by auto } then have "(⋂ℌ){is closed under}P" using IsOpClosed_def by auto moreover { fix A assume "A∈⋂ℌ" then have "∀H∈ℌ. A∈H" by auto then have "∀H∈ℌ. A¯∈H" using assms(1) group0_3_T3A by auto then have "A¯∈⋂ℌ" using assms(2) by auto } then have "∀A∈⋂ℌ. A¯∈⋂ℌ" by auto moreover have "⋂ℌ⊆G" using assms(1,2) group0_3_L2 by force ultimately show ?thesis using group0_3_T3 by auto qed text{*As the previous lemma states, the subgroup that contains a subset can be defined as an intersection of subgroups.*} definition(in group0) SubgroupGenerated ("⟨_⟩⇩_{G}" 80) where "⟨X⟩⇩_{G}≡ ⋂{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}" theorem(in group0) subgroupGen_is_subgroup: assumes "X⊆G" shows "IsAsubgroup(⟨X⟩⇩_{G},P)" proof- have "restrict(P,G×G)=P" using group_oper_assocA restrict_idem unfolding Pi_def by auto then have "IsAsubgroup(G,P)" unfolding IsAsubgroup_def using groupAssum by auto with assms have "G∈{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}" by auto then have "{H∈Pow(G). X⊆H ∧ IsAsubgroup(H,P)}≠0" by auto then show ?thesis using inter_subgroups unfolding SubgroupGenerated_def by auto qed subsection{*Homomorphisms*} text{*A homomorphism is a function between groups that preserves group operations.*} definition Homomor ("_{is a homomorphism}{_,_}→{_,_}" 85) where "IsAgroup(G,P) ⟹ IsAgroup(H,F) ⟹ Homomor(f,G,P,H,F) ≡ ∀g1∈G. ∀g2∈G. f`(P`⟨g1,g2⟩)=F`⟨f`g1,f`g2⟩" text{*Now a lemma about the definition:*} lemma homomor_eq: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "g1∈G" "g2∈G" shows "f`(P`⟨g1,g2⟩)=F`⟨f`g1,f`g2⟩" 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 where "End(G,P) ≡ {f:G→G. Homomor(f,G,P,G,P)}" 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 "f1∈End(G,P)""f2∈End(G,P)" shows "Composition(G)`⟨f1,f2⟩∈End(G,P)" proof- from assms have fun:"f1:G→G""f2:G→G" unfolding End_def by auto then have fun2:"f1 O f2:G→G" using comp_fun by auto have comp:"Composition(G)`⟨f1,f2⟩=f1 O f2" using func_ZF_5_L2 fun by auto { fix g1 g2 assume AS2:"g1∈G""g2∈G" then have g1g2:"g1⋅g2∈G" using group_op_closed by auto from fun2 have "(f1 O f2)`(g1⋅g2)=f1`(f2`(g1⋅g2))" using comp_fun_apply fun(2) g1g2 by auto also have "…=f1`((f2`g1)⋅(f2`g2))" using assms(2) unfolding End_def Homomor_def[OF groupAssum groupAssum] using AS2 by auto moreover have "f2`g1∈G""f2`g2∈G" using fun(2) AS2 apply_type by auto ultimately have "(f1 O f2)`(g1⋅g2)=(f1`(f2`g1))⋅(f1`(f2`g2))" using assms(1) unfolding End_def Homomor_def[OF groupAssum groupAssum] using AS2 by auto then have "(f1 O f2)`(g1⋅g2)=((f1 O f2)`g1)⋅((f1 O f2)`g2)" using comp_fun_apply fun(2) AS2 by auto } then have "∀g1∈G. ∀g2∈G. (f1 O f2)`(g1⋅g2)=((f1 O f2)`g1)⋅((f1 O f2)`g2)" by auto then have "(f1 O f2)∈End(G,P)" unfolding End_def Homomor_def[OF groupAssum groupAssum] using fun2 by auto with comp show "Composition(G)`⟨f1,f2⟩∈End(G,P)" by auto qed theorem(in group0) end_comp_monoid: shows "IsAmonoid(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))" and "TheNeutralElement(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))=id(G)" proof- have fun:"id(G):G→G" unfolding id_def by auto { fix g h assume "g∈G""h∈G" then have id:"g⋅h∈G""id(G)`g=g""id(G)`h=h" using group_op_closed by auto then have "id(G)`(g⋅h)=g⋅h" unfolding id_def by auto with id(2,3) have "id(G)`(g⋅h)=(id(G)`g)⋅(id(G)`h)" by auto } with fun have "id(G)∈End(G,P)" unfolding End_def Homomor_def[OF groupAssum groupAssum] by auto moreover from Group_ZF_2_5_L2(2) have A0:"id(G)=TheNeutralElement(G → G, Composition(G))" 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 auto moreover from end_composition have A3:"End(G,P){is closed under}Composition(G)" unfolding IsOpClosed_def by auto ultimately show "IsAmonoid(End(G,P),restrict(Composition(G),End(G,P)×End(G,P)))" using monoid0.group0_1_T1 unfolding monoid0_def using Group_ZF_2_5_L2(1) by force 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),restrict(Composition(G),End(G,P)×End(G,P)))=id(G)" using group0_1_L6 by auto qed text{*The set of endomorphisms is closed under pointwise addition. This is so because the group is abelian.*} theorem(in group0) end_pointwise_addition: assumes "f∈End(G,P)""g∈End(G,P)""P{is commutative on}G""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 auto then have fun2:"F`⟨f,g⟩:G→G" using monoid0.Group_ZF_2_1_L0 group0_2_L1 assms(4) by auto { fix g1 g2 assume AS:"g1∈G""g2∈G" then have "g1⋅g2∈G" using group_op_closed by auto then have "(F`⟨f,g⟩)`(g1⋅g2)=(f`(g1⋅g2))⋅(g`(g1⋅g2))" using Group_ZF_2_1_L3 fun assms(4) by auto also have "…=(f`(g1)⋅f`(g2))⋅(g`(g1)⋅g`(g2))" using assms unfolding End_def Homomor_def[OF groupAssum groupAssum] using AS by auto ultimately have "(F`⟨f,g⟩)`(g1⋅g2)=(f`(g1)⋅f`(g2))⋅(g`(g1)⋅g`(g2))" by auto moreover have "f`g1∈G""f`g2∈G""g`g1∈G""g`g2∈G" using fun apply_type AS by auto ultimately have "(F`⟨f,g⟩)`(g1⋅g2)=(f`(g1)⋅g`(g1))⋅(f`(g2)⋅g`(g2))" using group0_4_L8(3) assms(3) by auto with AS have "(F`⟨f,g⟩)`(g1⋅g2)=((F`⟨f,g⟩)`g1)⋅((F`⟨f,g⟩)`g2)" using Group_ZF_2_1_L3 fun assms(4) by auto } with fun2 show ?thesis unfolding End_def Homomor_def[OF groupAssum groupAssum] by auto qed text{*The inverse of an abelian group is an endomorphism.*} lemma(in group0) end_inverse_group: assumes "P{is commutative on}G" shows "GroupInv(G,P)∈End(G,P)" proof- { fix s t assume AS:"s∈G""t∈G" then have elinv:"s¯∈G""t¯∈G" using inverse_in_group by auto have "(s⋅t)¯=t¯⋅s¯" using group_inv_of_two AS by auto then have "(s⋅t)¯=s¯⋅t¯" using assms(1) elinv unfolding IsCommutative_def by auto } then have "∀s∈G. ∀t∈G. GroupInv(G,P)`(s⋅t)=GroupInv(G,P)`(s)⋅GroupInv(G,P)`(t)" by auto with group0_2_T2 groupAssum show ?thesis unfolding End_def using Homomor_def by auto qed 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 group0) end_addition_group: assumes "P{is commutative on}G" "F = P {lifted to function space over} G" shows "IsAgroup(End(G,P),restrict(F,End(G,P)×End(G,P)))" "restrict(F,End(G,P)×End(G,P)){is commutative on}End(G,P)" proof- from end_comp_monoid(1) monoid0.group0_1_L3A have "End(G,P)≠0" unfolding monoid0_def by auto moreover have "End(G,P)⊆G→G" unfolding End_def by auto moreover have "End(G,P){is closed under}F" unfolding IsOpClosed_def using end_pointwise_addition assms(1,2) by auto moreover { fix ff assume AS:"ff∈End(G,P)" then have "restrict(Composition(G),End(G,P)×End(G,P))`⟨GroupInv(G,P), ff⟩∈End(G,P)" using monoid0.group0_1_L1 unfolding monoid0_def using end_composition(1) end_inverse_group[OF assms(1)] by force then have "Composition(G)`⟨GroupInv(G,P), ff⟩∈End(G,P)" using AS end_inverse_group[OF assms(1)] by auto then have "GroupInv(G,P) O ff∈End(G,P)" using func_ZF_5_L2 AS group0_2_T2 groupAssum unfolding End_def by auto then have "GroupInv(G→G,F)`ff∈End(G,P)" using Group_ZF_2_1_L6 assms(2) AS unfolding End_def by auto } then have "∀ff∈End(G,P). GroupInv(G→G,F)`ff∈End(G,P)" by auto ultimately show "IsAgroup(End(G,P),restrict(F,End(G,P)×End(G,P)))" using group0.group0_3_T3 Group_ZF_2_1_T2[OF assms(2)] unfolding IsAsubgroup_def group0_def by auto show "restrict(F,End(G,P)×End(G,P)){is commutative on}End(G,P)" using Group_ZF_2_1_L7[OF assms(2,1)] unfolding End_def IsCommutative_def by auto qed lemma(in group0) distributive_comp_pointwise: assumes "P{is commutative on}G" "F = P {lifted to function space over} G" shows "IsDistributive(End(G,P),restrict(F,End(G,P)×End(G,P)),restrict(Composition(G),End(G,P)×End(G,P)))" proof- { fix b c d assume AS:"b∈End(G,P)""c∈End(G,P)""d∈End(G,P)" have ig1:"Composition(G) `⟨b, F ` ⟨c, d⟩⟩ =b O (F`⟨c,d⟩)" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] AS unfolding End_def using func_ZF_5_L2 by auto have ig2:"F `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩=F `⟨b O c,b O d⟩" using AS unfolding End_def using func_ZF_5_L2 by auto have comp1fun:"(b O (F`⟨c,d⟩)):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force have comp2fun:"(F `⟨b O c,b O d⟩):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force { fix g assume gG:"g∈G" then have "(b O (F`⟨c,d⟩))`g=b`((F`⟨c,d⟩)`g)" using comp_fun_apply monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] AS(2,3) unfolding End_def by force also have "…=b`(c`(g)⋅d`(g))" using Group_ZF_2_1_L3[OF assms(2)] AS(2,3) gG unfolding End_def by auto ultimately have "(b O (F`⟨c,d⟩))`g=b`(c`(g)⋅d`(g))" by auto moreover have "c`g∈G""d`g∈G" using AS(2,3) unfolding End_def using apply_type gG by auto ultimately have "(b O (F`⟨c,d⟩))`g=(b`(c`g))⋅(b`(d`g))" using AS(1) unfolding End_def Homomor_def[OF groupAssum groupAssum] by auto then have "(b O (F`⟨c,d⟩))`g=((b O c)`g)⋅((b O d)`g)" using comp_fun_apply gG AS(2,3) unfolding End_def by auto then have "(b O (F`⟨c,d⟩))`g=(F`⟨b O c,b O d⟩)`g" using gG Group_ZF_2_1_L3[OF assms(2) comp_fun comp_fun gG] AS unfolding End_def by auto } then have "∀g∈G. (b O (F`⟨c,d⟩))`g=(F`⟨b O c,b O d⟩)`g" by auto then have "b O (F`⟨c,d⟩)=F`⟨b O c,b O d⟩" using fun_extension[OF comp1fun comp2fun] by auto with ig1 ig2 have "Composition(G) `⟨b, F ` ⟨c, d⟩⟩ =F `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩" by auto moreover have "F ` ⟨c, d⟩=restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩" using AS(2,3) restrict by auto moreover have "Composition(G) `⟨b , c⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , c⟩" "Composition(G) `⟨b , d⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , d⟩" using restrict AS by auto moreover have "Composition(G) `⟨b, F ` ⟨c, d⟩⟩ =restrict(Composition(G),End(G,P)×End(G,P)) `⟨b, F ` ⟨c, d⟩⟩" using AS(1) end_pointwise_addition[OF AS(2,3) assms] by auto moreover have "F `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩=restrict(F,End(G,P)×End(G,P)) `⟨Composition(G) `⟨b , c⟩,Composition(G) `⟨b , d⟩⟩" using end_composition[OF AS(1,2)] end_composition[OF AS(1,3)] by auto ultimately have eq1:"restrict(Composition(G),End(G,P)×End(G,P)) `⟨b, restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , c⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨b , d⟩⟩" by auto have ig1:"Composition(G) `⟨ F ` ⟨c, d⟩,b⟩ = (F`⟨c,d⟩) O b" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] AS unfolding End_def using func_ZF_5_L2 by auto have ig2:"F `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩=F `⟨c O b,d O b⟩" using AS unfolding End_def using func_ZF_5_L2 by auto have comp1fun:"((F`⟨c,d⟩) O b):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force have comp2fun:"(F `⟨c O b,d O b⟩):G→G" using monoid0.Group_ZF_2_1_L0[OF group0_2_L1 assms(2)] comp_fun AS unfolding End_def by force { fix g assume gG:"g∈G" then have bg:"b`g∈G" using AS(1) unfolding End_def using apply_type by auto from gG have "((F`⟨c,d⟩) O b)`g=(F`⟨c,d⟩)`(b`g)" using comp_fun_apply AS(1) unfolding End_def by force also have "…=(c`(b`g))⋅(d`(b`g))" using Group_ZF_2_1_L3[OF assms(2)] AS(2,3) bg unfolding End_def by auto also have "…=((c O b)`g)⋅((d O b)`g)" using comp_fun_apply gG AS unfolding End_def by auto also have "…=(F`⟨c O b,d O b⟩)`g" using gG Group_ZF_2_1_L3[OF assms(2) comp_fun comp_fun gG] AS unfolding End_def by auto ultimately have"((F`⟨c,d⟩) O b)`g=(F`⟨c O b,d O b⟩)`g" by auto } then have "∀g∈G. ((F`⟨c,d⟩) O b)`g=(F`⟨c O b,d O b⟩)`g" by auto then have "(F`⟨c,d⟩) O b=F`⟨c O b,d O b⟩" using fun_extension[OF comp1fun comp2fun] by auto with ig1 ig2 have "Composition(G) `⟨F ` ⟨c, d⟩,b⟩ =F `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩" by auto moreover have "F ` ⟨c, d⟩=restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩" using AS(2,3) restrict by auto moreover have "Composition(G) `⟨c , b⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨c , b⟩" "Composition(G) `⟨d , b⟩=restrict(Composition(G),End(G,P)×End(G,P)) `⟨d , b⟩" using restrict AS by auto moreover have "Composition(G) `⟨F ` ⟨c, d⟩,b⟩ =restrict(Composition(G),End(G,P)×End(G,P)) `⟨F ` ⟨c, d⟩,b⟩" using AS(1) end_pointwise_addition[OF AS(2,3) assms] by auto moreover have "F `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩=restrict(F,End(G,P)×End(G,P)) `⟨Composition(G) `⟨c , b⟩,Composition(G) `⟨d , b⟩⟩" using end_composition[OF AS(2,1)] end_composition[OF AS(3,1)] by auto ultimately have eq2:"restrict(Composition(G),End(G,P)×End(G,P)) `⟨ restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩,b⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨c ,b⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨d , b⟩⟩" by auto with eq1 have "(restrict(Composition(G),End(G,P)×End(G,P)) `⟨b, restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨b , c⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨b , d⟩⟩)∧ (restrict(Composition(G),End(G,P)×End(G,P)) `⟨ restrict(F,End(G,P)×End(G,P)) ` ⟨c, d⟩,b⟩ =restrict(F,End(G,P)×End(G,P)) `⟨restrict(Composition(G),End(G,P)×End(G,P)) `⟨c ,b⟩,restrict(Composition(G),End(G,P)×End(G,P))`⟨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 group0) end_is_ring: assumes "P{is commutative on}G" "F = P {lifted to function space over} G" shows "IsAring(End(G,P),restrict(F,End(G,P)×End(G,P)),restrict(Composition(G),End(G,P)×End(G,P)))" unfolding IsAring_def using end_addition_group[OF assms] end_comp_monoid(1) distributive_comp_pointwise[OF assms] by auto 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 and commutes with the inverse.*} 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- have g:"TheNeutralElement(G,P)=P`⟨TheNeutralElement(G,P),TheNeutralElement(G,P)⟩" "TheNeutralElement(G,P)∈G" using assms(1) group0.group0_2_L2 unfolding group0_def by auto from g(1) have "f`TheNeutralElement(G,P)=f`(P`⟨TheNeutralElement(G,P),TheNeutralElement(G,P)⟩)" by auto also have "…=F`⟨f`TheNeutralElement(G,P),f`TheNeutralElement(G,P)⟩" using assms(3) unfolding Homomor_def[OF assms(1,2)] using g(2) by auto ultimately have "f`TheNeutralElement(G,P)=F`⟨f`TheNeutralElement(G,P),f`TheNeutralElement(G,P)⟩" by auto moreover have h:"f`TheNeutralElement(G,P)∈H" using g(2) apply_type[OF assms(4)] by auto then have "f`TheNeutralElement(G,P)=F`⟨f`TheNeutralElement(G,P),TheNeutralElement(H,F)⟩" using assms(2) group0.group0_2_L2 unfolding group0_def by auto ultimately have "F`⟨f`TheNeutralElement(G,P),TheNeutralElement(H,F)⟩=F`⟨f`TheNeutralElement(G,P),f`TheNeutralElement(G,P)⟩" by auto with h have "LeftTranslation(H,F,f`TheNeutralElement(G,P))`TheNeutralElement(H,F)=LeftTranslation(H,F,f`TheNeutralElement(G,P))`(f`TheNeutralElement(G,P))" using group0.group0_5_L2(2)[OF _ h] assms(2) group0.group0_2_L2 unfolding group0_def by auto moreover have "LeftTranslation(H,F,f`TheNeutralElement(G,P))∈bij(H,H)" using group0.trans_bij(2) assms(2) h unfolding group0_def by auto then have "LeftTranslation(H,F,f`TheNeutralElement(G,P))∈inj(H,H)" unfolding bij_def by auto ultimately show "f`TheNeutralElement(G,P)=TheNeutralElement(H,F)" using h assms(2) group0.group0_2_L2 unfolding inj_def group0_def by force qed 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- have im:"f`g∈H" using apply_type[OF assms(4,5)]. have inv:"GroupInv(G,P)`g∈G" using group0.inverse_in_group[OF _ assms(5)] assms(1) unfolding group0_def by auto then have inv2:"f`(GroupInv(G,P)`g)∈H"using apply_type[OF assms(4)] by auto have "f`TheNeutralElement(G,P)=f`(P`⟨g,GroupInv(G,P)`g⟩)" using assms(1,5) group0.group0_2_L6 unfolding group0_def by auto also have "…=F`⟨f`g,f`(GroupInv(G,P)`g)⟩" using assms(3) unfolding Homomor_def[OF assms(1,2)] using assms(5) inv by auto ultimately have "TheNeutralElement(H,F)=F`⟨f`g,f`(GroupInv(G,P)`g)⟩" using image_neutral[OF assms(1-4)] by auto then show ?thesis using group0.group0_2_L9(2)[OF _ im inv2] assms(2) unfolding group0_def by auto qed text{*The kernel of an homomorphism is a normal subgroup.*} theorem kerner_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)})" proof- have xy:"∀x y. ⟨x, y⟩ ∈ f ⟶ (∀y'. ⟨x, y'⟩ ∈ f ⟶ y = y')" using assms(4) unfolding Pi_def function_def by force { fix g1 g2 assume "g1∈f-``{TheNeutralElement(H,F)}""g2∈f-``{TheNeutralElement(H,F)}" then have "⟨g1,TheNeutralElement(H,F)⟩∈f""⟨g2,TheNeutralElement(H,F)⟩∈f" using vimage_iff by auto moreover then have G:"g1∈G""g2∈G" using assms(4) unfolding Pi_def by auto then have "⟨g1,f`g1⟩∈f""⟨g2,f`g2⟩∈f" using apply_Pair[OF assms(4)] by auto moreover note xy ultimately have "f`g1=TheNeutralElement(H,F)""f`g2=TheNeutralElement(H,F)" by auto moreover have "f`(P`⟨g1,g2⟩)=F`⟨f`g1,f`g2⟩" using assms(3) G unfolding Homomor_def[OF assms(1,2)] by auto ultimately have "f`(P`⟨g1,g2⟩)=F`⟨TheNeutralElement(H,F),TheNeutralElement(H,F)⟩" by auto also have "…=TheNeutralElement(H,F)" using group0.group0_2_L2 assms(2) unfolding group0_def by auto ultimately have "f`(P`⟨g1,g2⟩)=TheNeutralElement(H,F)" by auto moreover from G have "P`⟨g1,g2⟩∈G" using group0.group_op_closed assms(1) unfolding group0_def by auto ultimately have "⟨P`⟨g1,g2⟩,TheNeutralElement(H,F)⟩∈f" using apply_Pair[OF assms(4)] by force then have "P`⟨g1,g2⟩∈f-``{TheNeutralElement(H,F)}" using vimage_iff by auto } then have "f-``{TheNeutralElement(H,F)} {is closed under}P" unfolding IsOpClosed_def by auto moreover have A:"f-``{TheNeutralElement(H,F)} ⊆ G" using func1_1_L3 assms(4) by auto moreover have "f`TheNeutralElement(G,P)=TheNeutralElement(H,F)" using image_neutral assms by auto then have "⟨TheNeutralElement(G,P),TheNeutralElement(H,F)⟩∈f" using apply_Pair[OF assms(4)] group0.group0_2_L2 assms(1) unfolding group0_def by force then have "TheNeutralElement(G,P)∈f-``{TheNeutralElement(H,F)}" using vimage_iff by auto then have "f-``{TheNeutralElement(H,F)}≠0" by auto moreover { fix x assume "x∈f-``{TheNeutralElement(H,F)}" then have "⟨x,TheNeutralElement(H,F)⟩∈f" and x:"x∈G" using vimage_iff A by auto moreover from x have "⟨x,f`x⟩∈f" using apply_Pair[OF assms(4)] by auto ultimately have "f`x=TheNeutralElement(H,F)" using xy by auto moreover have "f`(GroupInv(G,P)`x)=GroupInv(H,F)`(f`x)" using x image_inv assms by auto ultimately have "f`(GroupInv(G,P)`x)=GroupInv(H,F)`TheNeutralElement(H,F)" by auto then have "f`(GroupInv(G,P)`x)=TheNeutralElement(H,F)" using group0.group_inv_of_one assms(2) unfolding group0_def by auto moreover have "⟨GroupInv(G,P)`x,f`(GroupInv(G,P)`x)⟩∈f" using apply_Pair[OF assms(4)] x group0.inverse_in_group assms(1) unfolding group0_def by auto ultimately have "⟨GroupInv(G,P)`x,TheNeutralElement(H,F)⟩∈f" by auto then have "GroupInv(G,P)`x∈f-``{TheNeutralElement(H,F)}" using vimage_iff by auto } then have "∀x∈f-``{TheNeutralElement(H,F)}. GroupInv(G,P)`x∈f-``{TheNeutralElement(H,F)}" by auto ultimately have SS:"IsAsubgroup(f-``{TheNeutralElement(H,F)},P)" using group0.group0_3_T3 assms(1) unfolding group0_def by auto { fix g h assume AS:"g∈G""h∈f-``{TheNeutralElement(H,F)}" from AS(1) have im:"f`g∈H" using assms(4) apply_type by auto then have iminv:"GroupInv(H,F)`(f`g)∈H" using assms(2) group0.inverse_in_group unfolding group0_def by auto from AS have "h∈G" and inv:"GroupInv(G,P)`g∈G" using A group0.inverse_in_group assms(1) unfolding group0_def by auto then have P:"P`⟨h,GroupInv(G,P)`g⟩∈G" using assms(1) group0.group_op_closed unfolding group0_def by auto with `g∈G` have "P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩∈G" using assms(1) group0.group_op_closed unfolding group0_def by auto then have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=F`⟨f`g,f`(P`⟨h,GroupInv(G,P)`g⟩)⟩" using assms(3) unfolding Homomor_def[OF assms(1,2)] using `g∈G` P by auto also have "…=F`⟨f`g,F`(⟨f`h,f`(GroupInv(G,P)`g)⟩)⟩" using assms(3) unfolding Homomor_def[OF assms(1,2)] using `h∈G` inv by auto also have "…=F`⟨f`g,F`(⟨f`h,GroupInv(H,F)`(f`g)⟩)⟩" using image_inv[OF assms `g∈G`] by auto ultimately have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=F`⟨f`g,F`(⟨f`h,GroupInv(H,F)`(f`g)⟩)⟩" by auto moreover from AS(2) have "f`h=TheNeutralElement(H,F)" using func1_1_L15[OF assms(4)] by auto ultimately have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=F`⟨f`g,F`(⟨TheNeutralElement(H,F),GroupInv(H,F)`(f`g)⟩)⟩" by auto also have "…=F`⟨f`g,GroupInv(H,F)`(f`g)⟩" using assms(2) im group0.group0_2_L2 unfolding group0_def using iminv by auto also have "…=TheNeutralElement(H,F)" using assms(2) group0.group0_2_L6 im unfolding group0_def by auto ultimately have "f`(P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩)=TheNeutralElement(H,F)" by auto moreover from P `g∈G` have "P`⟨g,P`⟨h,GroupInv(G,P)`g⟩⟩∈G" using group0.group_op_closed assms(1) unfolding group0_def by auto ultimately have "P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩∈f-``{TheNeutralElement(H,F)}" using func1_1_L15[OF assms(4)] by auto } then have "∀g∈G. {P`⟨g,P`⟨h,GroupInv(G,P)`g⟩ ⟩. h∈f-``{TheNeutralElement(H,F)}}⊆f-``{TheNeutralElement(H,F)}" by auto then show ?thesis using group0.cont_conj_is_normal assms(1) SS unfolding group0_def by auto qed text{*The image of a homomorphism is a subgroup.*} theorem image_sub: assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "f:G→H" shows "IsAsubgroup(f``G,F)" proof- have "TheNeutralElement(G,P)∈G" using group0.group0_2_L2 assms(1) unfolding group0_def by auto then have "TheNeutralElement(H,F)∈f``G" using func_imagedef[OF assms(4),of "G"] image_neutral[OF assms] by force then have "f``G≠0" by auto moreover { fix h1 h2 assume "h1∈f``G""h2∈f``G" then obtain g1 g2 where "h1=f`g1" "h2=f`g2" and p:"g1∈G""g2∈G" using func_imagedef[OF assms(4)] by auto then have "F`⟨h1,h2⟩=F`⟨f`g1,f`g2⟩" by auto also have "…=f`(P`⟨g1,g2⟩)" using assms(3) unfolding Homomor_def[OF assms(1,2)] using p by auto ultimately have "F`⟨h1,h2⟩=f`(P`⟨g1,g2⟩)" by auto moreover have "P`⟨g1,g2⟩∈G" using p group0.group_op_closed assms(1) unfolding group0_def by auto ultimately have "F`⟨h1,h2⟩∈f``G" using func_imagedef[OF assms(4)] by auto } then have "f``G {is closed under} F" unfolding IsOpClosed_def by auto moreover have "f``G⊆H" using func1_1_L6(2) assms(4) by auto moreover { fix h assume "h∈f``G" then obtain g where "h=f`g" and p:"g∈G" using func_imagedef[OF assms(4)] by auto then have "GroupInv(H,F)`h=GroupInv(H,F)`(f`g)" by auto then have "GroupInv(H,F)`h=f`(GroupInv(G,P)`g)" using p image_inv[OF assms] by auto then have "GroupInv(H,F)`h∈f``G" using p group0.inverse_in_group assms(1) unfolding group0_def using func_imagedef[OF assms(4)] by auto } then have "∀h∈f``G. GroupInv(H,F)`h∈f``G" by auto ultimately show ?thesis using group0.group0_3_T3 assms(2) unfolding group0_def by auto 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 "PP ≡ QuotientGroupOp(G,P,f-``{TheNeutralElement(H,F)})" shows "∃ff. Homomor(ff,G//r,PP,f``G,restrict(F,(f``G)×(f``G))) ∧ ff∈bij(G//r,f``G)" proof- let ?ff="{⟨r``{g},f`g⟩. g∈G}" { fix t assume "t∈{⟨r``{g},f`g⟩. g∈G}" then obtain g where "t=⟨r``{g},f`g⟩" "g∈G" by auto moreover then have "r``{g}∈G//r" unfolding r_def quotient_def by auto moreover from `g∈G` have "f`g∈f``G" using func_imagedef[OF assms(4)] by auto ultimately have "t∈(G//r)×f``G" by auto } then have "?ff∈Pow((G//r)×f``G)" by auto moreover have "(G//r)⊆domain(?ff)" unfolding domain_def quotient_def by auto moreover { fix x y t assume A:"⟨x,y⟩∈?ff" "⟨x,t⟩∈?ff" then obtain gy gr where "⟨x, y⟩=⟨r``{gy},f`gy⟩" "⟨x, t⟩=⟨r``{gr},f`gr⟩" and p:"gr∈G""gy∈G" by auto then have B:"r``{gy}=r``{gr}""y=f`gy""t=f`gr" by auto from B(2,3) have q:"y∈H""t∈H" using apply_type p assms(4) by auto have "⟨gy,gr⟩∈r" using eq_equiv_class[OF B(1) _ p(1)] group0.Group_ZF_2_4_L3 kerner_normal_sub[OF assms(1-4)] assms(1) unfolding group0_def IsAnormalSubgroup_def r_def by auto then have "P`⟨gy,GroupInv(G,P)`gr⟩∈f-``{TheNeutralElement(H,F)}" unfolding r_def QuotientGroupRel_def by auto then have eq:"f`(P`⟨gy,GroupInv(G,P)`gr⟩)=TheNeutralElement(H,F)" using func1_1_L15[OF assms(4)] by auto from B(2,3) have "F`⟨y,GroupInv(H,F)`t⟩=F`⟨f`gy,GroupInv(H,F)`(f`gr)⟩" by auto also have "…=F`⟨f`gy,f`(GroupInv(G,P)`gr)⟩" using image_inv[OF assms(1-4)] p(1) by auto also have "…=f`(P`⟨gy,GroupInv(G,P)`gr⟩)" using assms(3) unfolding Homomor_def[OF assms(1,2)] using p(2) group0.inverse_in_group assms(1) p(1) unfolding group0_def by auto ultimately have "F`⟨y,GroupInv(H,F)`t⟩=TheNeutralElement(H,F)" using eq by auto then have "y=t" using assms(2) group0.group0_2_L11A q unfolding group0_def by auto } then have "∀x y. ⟨x,y⟩∈?ff ⟶ (∀y'. ⟨x,y'⟩∈?ff ⟶ y=y')" by auto ultimately have ff_fun:"?ff:G//r→f``G" unfolding Pi_def function_def by auto { fix a1 a2 assume AS:"a1∈G//r""a2∈G//r" then obtain g1 g2 where p:"g1∈G""g2∈G" and a:"a1=r``{g1}""a2=r``{g2}" unfolding quotient_def by auto have "equiv(G,r)" using group0.Group_ZF_2_4_L3 kerner_normal_sub[OF assms(1-4)] assms(1) unfolding group0_def IsAnormalSubgroup_def r_def by auto moreover have "Congruent2(r,P)" using Group_ZF_2_4_L5A[OF assms(1) kerner_normal_sub[OF assms(1-4)]] unfolding r_def by auto moreover have "PP=ProjFun2(G,r,P)" unfolding PP_def QuotientGroupOp_def r_def by auto moreover note a p ultimately have "PP`⟨a1,a2⟩=r``{P`⟨g1,g2⟩}" using group0.Group_ZF_2_2_L2 assms(1) unfolding group0_def by auto then have "⟨PP`⟨a1,a2⟩,f`(P`⟨g1,g2⟩)⟩∈?ff" using group0.group_op_closed[OF _ p] assms(1) unfolding group0_def by auto then have eq:"?ff`(PP`⟨a1,a2⟩)=f`(P`⟨g1,g2⟩)" using apply_equality ff_fun by auto from p a have "⟨a1,f`g1⟩∈?ff""⟨a2,f`g2⟩∈?ff" by auto then have "?ff`a1=f`g1""?ff`a2=f`g2" using apply_equality ff_fun by auto then have "F`⟨?ff`a1,?ff`a2⟩=F`⟨f`g1,f`g2⟩" by auto also have "…=f`(P`⟨g1,g2⟩)" using assms(3) unfolding Homomor_def[OF assms(1,2)] using p by auto ultimately have "F`⟨?ff`a1,?ff`a2⟩=?ff`(PP`⟨a1,a2⟩)" using eq by auto moreover have "?ff`a1∈f``G""?ff`a2∈f``G" using ff_fun apply_type AS by auto ultimately have "restrict(F,f``G×f``G)`⟨?ff`a1,?ff`a2⟩=?ff`(PP`⟨a1,a2⟩)" by auto } then have r:"∀a1∈G//r. ∀a2∈G//r. restrict(F,f``G×f``G)`⟨?ff`a1,?ff`a2⟩=?ff`(PP`⟨a1,a2⟩)" by auto have G:"IsAgroup(G//r,PP)" using Group_ZF_2_4_T1[OF assms(1) kerner_normal_sub[OF assms(1-4)]] unfolding r_def PP_def by auto have H:"IsAgroup(f``G, restrict(F,f``G×f``G))" using image_sub[OF assms(1-4)] unfolding IsAsubgroup_def . have HOM:"Homomor(?ff,G//r,PP,f``G,restrict(F,(f``G)×(f``G)))" using r unfolding Homomor_def[OF G H] by auto { fix b1 b2 assume AS:"?ff`b1=?ff`b2""b1∈G//r""b2∈G//r" have invb2:"GroupInv(G//r,PP)`b2∈G//r" using group0.inverse_in_group[OF _ AS(3)] G unfolding group0_def by auto with AS(2) have "PP`⟨b1,GroupInv(G//r,PP)`b2⟩∈G//r" using group0.group_op_closed G unfolding group0_def by auto moreover then obtain gg where gg:"gg∈G""PP`⟨b1,GroupInv(G//r,PP)`b2⟩=r``{gg}" unfolding quotient_def by auto ultimately have E:"?ff`(PP`⟨b1,GroupInv(G//r,PP)`b2⟩)=f`gg" using apply_equality[OF _ ff_fun] by auto from invb2 have pp:"?ff`(GroupInv(G//r,PP)`b2)∈f``G" using apply_type ff_fun by auto from AS(2,3) have fff:"?ff`b1∈f``G""?ff`b2∈f``G" using apply_type[OF ff_fun] by auto from fff(1) pp have EE:"F`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩=restrict(F,f``G×f``G)`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩" by auto from fff have fff2:"?ff`b1∈H""?ff`b2∈H" using func1_1_L6(2)[OF assms(4)] by auto with AS(1) have "TheNeutralElement(H,F)=F`⟨?ff`b1,GroupInv(H,F)`(?ff`b2)⟩" using group0.group0_2_L6(1) assms(2) unfolding group0_def by auto also have "…=F`⟨?ff`b1,restrict(GroupInv(H,F),f``G)`(?ff`b2)⟩" using restrict fff(2) by auto also have "…=F`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩" using image_inv[OF G H HOM ff_fun AS(3)] group0.group0_3_T1[OF _ image_sub[OF assms(1-4)]] assms(2) unfolding group0_def by auto also have "…=restrict(F,f``G×f``G)`⟨?ff`b1,?ff`(GroupInv(G//r,PP)`b2)⟩" using EE by auto also have "…=?ff`(PP`⟨b1,GroupInv(G//r,PP)`b2⟩)" using HOM unfolding Homomor_def[OF G H] using AS(2) group0.inverse_in_group[OF _ AS(3)] G unfolding group0_def by auto also have "…=f`gg" using E by auto ultimately have "f`gg=TheNeutralElement(H,F)" by auto then have "gg∈f-``{TheNeutralElement(H,F)}" using func1_1_L15[OF assms(4)] `gg∈G` by auto then have "r``{gg}=TheNeutralElement(G//r,PP)" using group0.Group_ZF_2_4_L5E[OF _ kerner_normal_sub[OF assms(1-4)] `gg∈G` ] using assms(1) unfolding group0_def r_def PP_def by auto with gg(2) have "PP`⟨b1,GroupInv(G//r,PP)`b2⟩=TheNeutralElement(G//r,PP)" by auto then have "b1=b2" using group0.group0_2_L11A[OF _ AS(2,3)] G unfolding group0_def by auto } then have "?ff∈inj(G//r,f``G)" unfolding inj_def using ff_fun by auto moreover { fix m assume "m∈f``G" then obtain g where "g∈G""m=f`g" using func_imagedef[OF assms(4)] by auto then have "⟨r``{g},m⟩∈?ff" by auto then have "?ff`(r``{g})=m" using apply_equality ff_fun by auto then have "∃A∈G//r. ?ff`A=m" unfolding quotient_def using `g∈G` by auto } ultimately have "?ff∈bij(G//r,f``G)" unfolding bij_def surj_def using ff_fun by auto with HOM show ?thesis by auto qed text{*As a last result, 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 h1 h2 assume A:"h1∈H" "h2∈H" from A(1) obtain g1 where g1:"g1∈G" "f`g1=h1" using assms(1) unfolding bij_def surj_def by auto moreover from A(2) obtain g2 where g2:"g2∈G" "f`g2=h2" using assms(1) unfolding bij_def surj_def by auto ultimately have "F`⟨f`g1,f`g2⟩=F`⟨h1,h2⟩" by auto then have "f`(P`⟨g1,g2⟩)=F`⟨h1,h2⟩" using assms(2,3,4) homomor_eq g1(1) g2(1) by auto then have "converse(f)`(f`(P`⟨g1,g2⟩))=converse(f)`(F`⟨h1,h2⟩)" by auto then have "P`⟨g1,g2⟩=converse(f)`(F`⟨h1,h2⟩)" using left_inverse assms(1) group0.group_op_closed assms(2) g1(1) g2(1) unfolding group0_def bij_def by auto moreover from g1(2) have "converse(f)`(f`g1)=converse(f)`h1" by auto then have "g1=converse(f)`h1" using left_inverse assms(1) unfolding bij_def using g1(1) by auto moreover from g2(2) have "converse(f)`(f`g2)=converse(f)`h2" by auto then have "g2=converse(f)`h2" using left_inverse assms(1) unfolding bij_def using g2(1) by auto ultimately have "P`⟨converse(f)`h1,converse(f)`h2⟩=converse(f)`(F`⟨h1,h2⟩)" by auto } then show ?thesis using assms(2,3) Homomor_def by auto qed end