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