begin
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.
Conjugation of subgroups
First we show some properties of conjugation
The conjugate of a subgroup is a subgroup.
theorem (in group0) conj_group_is_group:
assumes \( \text{IsAsubgroup}(H,P) \), \( g\in G \)
shows \( \text{IsAsubgroup}(\{g\cdot (h\cdot g^{-1}).\ h\in H\},P) \)proof have sub: \( H\subseteq G \) using assms(1), group0_3_L2
from assms(2) have \( g^{-1}\in G \) using inverse_in_group
{
fix \( r \)
assume \( r\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)
then obtain \( h \) where h: \( h\in H \), \( r=g\cdot (h\cdot (g^{-1})) \)
from h(1) have \( h^{-1}\in H \) using group0_3_T3A, assms(1)
from h(1), sub have \( h\in G \)
then have \( h^{-1}\in G \) using inverse_in_group
with \( g^{-1}\in G \) have \( ((h^{-1})\cdot (g)^{-1})\in G \) using group_op_closed
from h(2) have \( r^{-1}=(g\cdot (h\cdot (g^{-1})))^{-1} \)
moreover
from \( h\in G \), \( g^{-1}\in G \) have s: \( h\cdot (g^{-1})\in G \) using group_op_closed
ultimately have \( r^{-1}=(h\cdot (g^{-1}))^{-1}\cdot (g)^{-1} \) using group_inv_of_two, assms(2)
moreover
from \( h\in G \), \( g^{-1}\in G \) have \( (h\cdot (g^{-1}))^{-1}=(g^{-1})^{-1}\cdot h^{-1} \) using group_inv_of_two
moreover have \( (g^{-1})^{-1}=g \) using group_inv_of_inv, assms(2)
ultimately have \( r^{-1}=(g\cdot (h^{-1}))\cdot (g)^{-1} \)
with \( h^{-1}\in G \), \( g^{-1}\in G \) have \( r^{-1}=g\cdot ((h^{-1})\cdot (g)^{-1}) \) using group_oper_assoc, assms(2)
moreover
from s, assms(2), h(2) have \( r\in G \) using group_op_closed
moreover note \( h^{-1}\in H \)
ultimately have \( r^{-1}\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \), \( r\in G \)
then have \( \forall r\in \{g\cdot (h\cdot g^{-1}).\ h\in H\}.\ r^{-1}\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \) and \( \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq G \)
moreover {
}
qed
fix \( s \) \( t \)
assume s: \( s\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \) and t: \( t\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)
then obtain \( hs \) \( ht \) where hs: \( hs\in H \), \( s=g\cdot (hs\cdot (g^{-1})) \) and ht: \( ht\in H \), \( t=g\cdot (ht\cdot (g^{-1})) \)
from hs(1) have \( hs\in G \) using sub
then have \( g\cdot hs\in G \) using group_op_closed, assms(2)
then have \( (g\cdot hs)^{-1}\in G \) using inverse_in_group
from ht(1) have \( ht\in G \) using sub
with \( g^{-1}:G \) have \( ht\cdot (g^{-1})\in G \) using group_op_closed
from hs(2), ht(2) have \( s\cdot t=(g\cdot (hs\cdot (g^{-1})))\cdot (g\cdot (ht\cdot (g^{-1}))) \)
moreover
from \( hs\in G \) have \( hs\cdot ht = hs\cdot 1 \cdot ht \) using group0_2_L2
then have \( hs\cdot ht = hs\cdot (g^{-1}\cdot g)\cdot ht \) using group0_2_L6, assms(2)
then have \( g\cdot (hs\cdot ht) = g\cdot (hs\cdot (g^{-1}\cdot g)\cdot ht) \)
with \( hs\in G \) have \( g\cdot (hs\cdot ht) = g\cdot ((hs\cdot g^{-1}\cdot g)\cdot ht) \) using group_oper_assoc, assms(2), inverse_in_group
with \( hs\in G \), \( ht\in G \) have \( g\cdot (hs\cdot ht) = g\cdot (hs\cdot g^{-1}\cdot (g\cdot ht)) \) using group_oper_assoc, assms(2), inverse_in_group, group_op_closed
with \( hs\in G \), \( ht\in G \) have \( g\cdot (hs\cdot ht) = g\cdot (hs\cdot g^{-1})\cdot (g\cdot ht) \) using group_oper_assoc, assms(2), inverse_in_group, group_op_closed
then have \( g\cdot (hs\cdot ht)\cdot g^{-1} = g\cdot (hs\cdot g^{-1})\cdot (g\cdot ht)\cdot g^{-1} \)
with \( hs\in G \), \( ht\in G \) have \( g\cdot ((hs\cdot ht)\cdot g^{-1}) = g\cdot (hs\cdot g^{-1})\cdot (g\cdot ht)\cdot g^{-1} \) using group_oper_assoc, inverse_in_group, assms(2), group_op_closed
with \( hs\in G \), \( ht\in G \) have \( g\cdot ((hs\cdot ht)\cdot g^{-1}) = (g\cdot (hs\cdot g^{-1}))\cdot (g\cdot (ht\cdot g^{-1})) \) using group_oper_assoc, inverse_in_group, assms(2), group_op_closed
ultimately have \( s\cdot t=g\cdot ((hs\cdot ht)\cdot (g^{-1})) \)
moreover
from hs(1), ht(1) have \( hs\cdot ht\in H \) using assms(1), group0_3_L6
ultimately have \( s\cdot t\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)
then have \( \{g\cdot (h\cdot g^{-1}).\ h\in H\} \text{ is closed under }P \) unfolding IsOpClosed_def
moreover from assms(1) have \( 1 \in H \) using group0_3_L5
then have \( g\cdot (1 \cdot g^{-1})\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)
then have \( \{g\cdot (h\cdot g^{-1}).\ h\in H\}\neq 0 \)
ultimately show \( thesis \) using group0_3_T3
Every set is equipollent with its conjugates.
theorem (in group0) conj_set_is_eqpoll:
assumes \( H\subseteq G \), \( g\in G \)
shows \( H\approx \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)proof have fun: \( \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}:H\rightarrow \{g\cdot (h\cdot g^{-1}).\ h\in H\} \) unfolding Pi_def, function_def, domain_def
{
fix \( h1 \) \( h2 \)
assume \( h1\in H \), \( h2\in H \), \( \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h1=\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h2 \)
with fun have \( g\cdot (h1\cdot g^{-1})=g\cdot (h2\cdot g^{-1}) \), \( h1\cdot g^{-1}\in G \), \( h2\cdot g^{-1}\in G \), \( h1\in G \), \( h2\in G \) using apply_equality, assms(1), group_op_closed, inverse_in_group, assms(2)
then have \( h1\cdot g^{-1}=h2\cdot g^{-1} \) using group0_2_L19(2), assms(2)
with \( h1\in G \), \( h2\in G \) have \( h1=h2 \) using group0_2_L19(1), inverse_in_group, assms(2)
then have \( \forall h1\in H.\ \forall h2\in H.\ \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h1=\{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h2 \longrightarrow h1=h2 \)
with fun have \( \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}\in \text{inj}(H,\{g\cdot (h\cdot g^{-1}).\ h\in H\}) \) unfolding inj_def
moreover {
}
qed
fix \( ghg \)
assume \( ghg\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)
then obtain \( h \) where \( h\in H \), \( ghg=g\cdot (h\cdot g^{-1}) \)
then have \( \langle h,ghg\rangle \in \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\} \)
then have \( \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h=ghg \) using apply_equality, fun
with \( h\in H \) have \( \exists h\in H.\ \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}h=ghg \)
with fun have \( \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}\in \text{surj}(H,\{g\cdot (h\cdot g^{-1}).\ h\in H\}) \) unfolding surj_def
ultimately have \( \{\langle h,g\cdot (h\cdot g^{-1})\rangle .\ h\in H\}\in \text{bij}(H,\{g\cdot (h\cdot g^{-1}).\ h\in H\}) \) unfolding bij_def
then show \( thesis \) unfolding eqpoll_def
Every normal subgroup contains its conjugate subgroups.
theorem (in group0) norm_group_cont_conj:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \), \( g\in G \)
shows \( \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H \)proof{
}
fix \( r \)
assume \( r\in \{g\cdot (h\cdot g^{-1}).\ h\in H\} \)
then obtain \( h \) where h: \( r=g\cdot (h\cdot g^{-1}) \), \( h\in H \)
moreover
from h(2) have \( h\in G \) using group0_3_L2, assms(1) unfolding IsAnormalSubgroup_def
moreover from assms(2) have \( g^{-1}\in G \) using inverse_in_group
ultimately have \( r=g\cdot h\cdot g^{-1} \), \( h\in H \) using group_oper_assoc, assms(2)
then have \( r\in H \) using assms unfolding IsAnormalSubgroup_def
then show \( \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H \)
qed
If a subgroup contains all its conjugate subgroups, then it is normal.
theorem (in group0) cont_conj_is_normal:
assumes \( \text{IsAsubgroup}(H,P) \), \( \forall g\in G.\ \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \)proof{
}
fix \( h \) \( g \)
assume \( h\in H \), \( g\in G \)
with assms(2) have \( g\cdot (h\cdot g^{-1})\in H \)
moreover
from \( g\in G \), \( h\in H \) have \( h\in G \), \( g^{-1}\in G \), \( g\in G \) using group0_3_L2, assms(1), inverse_in_group
ultimately have \( g\cdot h\cdot g^{-1}\in H \) using group_oper_assoc
then show \( thesis \) using assms(1) unfolding IsAnormalSubgroup_def
qed
If a group has only one subgroup of a given order, then this subgroup is normal.
corollary (in group0) only_one_equipoll_sub:
assumes \( \text{IsAsubgroup}(H,P) \), \( \forall M.\ \text{IsAsubgroup}(M,P)\wedge H\approx M \longrightarrow M=H \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \)proof{
}
fix \( g \)
assume g: \( g\in G \)
with assms(1) have \( \text{IsAsubgroup}(\{g\cdot (h\cdot g^{-1}).\ h\in H\},P) \) using conj_group_is_group
moreover
from assms(1), g have \( H\approx \{g\cdot (h\cdot g^{-1}).\ h\in H\} \) using conj_set_is_eqpoll, group0_3_L2
ultimately have \( \{g\cdot (h\cdot g^{-1}).\ h\in H\}=H \) using assms(2)
then have \( \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H \)
then show \( thesis \) using cont_conj_is_normal, assms(1)
qed
The trivial subgroup is then a normal subgroup.
corollary (in group0) trivial_normal_subgroup:
shows \( \text{IsAnormalSubgroup}(G,P,\{1 \}) \)proof have \( \{1 \}\subseteq G \) using group0_2_L2
moreover
}
}
have \( \{1 \}\neq 0 \)
moreover {
fix \( a \) \( b \)
assume \( a\in \{1 \} \), \( b\in \{1 \} \)
then have \( a=1 \), \( b=1 \)
then have \( P\langle a,b\rangle =1 \cdot 1 \)
then have \( P\langle a,b\rangle =1 \) using group0_2_L2
then have \( P\langle a,b\rangle \in \{1 \} \)
then have \( \{1 }\text{ is closed under }\} \) unfolding IsOpClosed_def
moreover {
fix \( a \)
assume \( a\in \{1 \} \)
then have \( a=1 \)
then have \( a^{-1}=1 ^{-1} \)
then have \( a^{-1}=1 \) using group_inv_of_one
then have \( a^{-1}\in \{1 \} \)
then have \( \forall a\in \{1 \}.\ a^{-1}\in \{1 \} \)
ultimately have \( \text{IsAsubgroup}(\{1 \},P) \) using group0_3_T3
moreover {
}
}
ultimately show \( thesis \) using only_one_equipoll_sub
qed
fix \( M \)
assume M: \( \text{IsAsubgroup}(M,P) \), \( \{1 \}\approx M \)
then have one: \( 1 \in M \), \( M\approx \{1 \} \) using eqpoll_sym, group0_3_L5
then obtain \( f \) where \( f\in \text{bij}(M,\{1 \}) \) unfolding eqpoll_def
then have inj: \( f\in \text{inj}(M,\{1 \}) \) unfolding bij_def
then have fun: \( f:M\rightarrow \{1 \} \) unfolding inj_def
{
fix \( b \)
assume b: \( b\in M \), \( b\neq 1 \)
with \( 1 \in M \) have \( fb\neq f1 \) using inj unfolding inj_def
moreover
from fun, b(1) have \( fb\in \{1 \} \) by (rule apply_type )
moreover from fun, one(1) have \( f1 \in \{1 \} \) by (rule apply_type )
ultimately have \( False \)
with \( 1 \in M \) have \( M=\{1 \} \)
The whole group is normal as a subgroup
lemma (in group0) whole_normal_subgroup:
shows \( \text{IsAnormalSubgroup}(G,P,G) \)proof have \( G\subseteq G \)
moreover
have \( \forall x\in G.\ x^{-1}\in G \) using inverse_in_group
moreover have \( G\neq 0 \) using group0_2_L2
moreover have \( G\text{ is closed under }P \) using group_op_closed unfolding IsOpClosed_def
ultimately have \( \text{IsAsubgroup}(G,P) \) using group0_3_T3
moreover {
}
ultimately show \( thesis \) unfolding IsAnormalSubgroup_def
qed
fix \( n \) \( g \)
assume ng: \( n\in G \), \( g\in G \)
then have \( P \langle P \langle g, n\rangle , \text{GroupInv}(G, P) g\rangle \in G \) using group_op_closed, inverse_in_group
Simple groups
In this subsection we study the groups that build the rest of the groups: the simple groups.
Since the whole group and the trivial subgroup are always normal, it is natural to define simplicity of groups in the following way:
definition
\( [G,f]\text{ is a simple group } \equiv \text{IsAgroup}(G,f) \wedge (\forall M.\ \text{IsAnormalSubgroup}(G,f,M) \longrightarrow M=G\vee M=\{\text{ TheNeutralElement}(G,f)\}) \)
From the definition follows that if a group has no subgroups, then it is simple.
corollary (in group0) noSubgroup_imp_simple:
assumes \( \forall H.\ \text{IsAsubgroup}(H,P)\longrightarrow H=G\vee H=\{1 \} \)
shows \( [G,P]\text{ is a simple group } \)proof have \( \text{IsAgroup}(G,P) \) using groupAssum
moreover {
}
ultimately show \( thesis \) unfolding IsSimple_def
qed
fix \( M \)
assume \( \text{IsAnormalSubgroup}(G,P,M) \)
then have \( \text{IsAsubgroup}(M,P) \) unfolding IsAnormalSubgroup_def
with assms have \( M=G\vee M=\{1 \} \)
We add a context for an abelian group
locale abelian_group = group0 +
assumes isAbelian: \( P \text{ is commutative on } G \)
Since every subgroup is normal in abelian groups, it follows that commutative simple groups do not have subgroups.
corollary (in abelian_group) abelian_simple_noSubgroups:
assumes \( [G,P]\text{ is a simple group } \)
shows \( \forall H.\ \text{IsAsubgroup}(H,P)\longrightarrow H=G\vee H=\{1 \} \)proof{
}
fix \( H \)
assume A: \( \text{IsAsubgroup}(H,P) \), \( H \neq \{1 \} \)
then have \( \text{IsAnormalSubgroup}(G,P,H) \) using Group_ZF_2_4_L6(1), groupAssum, isAbelian
with assms(1), A have \( H=G \) unfolding IsSimple_def
then show \( thesis \)
qed
Finite groups
This subsection deals with finite groups and their structure
The subgroup of a finite group is finite.
lemma (in group0) finite_subgroup:
assumes \( Finite(G) \), \( \text{IsAsubgroup}(H,P) \)
shows \( Finite(H) \) using group0_3_L2, subset_Finite, assmsThe space of cosets is also finite. In particular, quotient groups.
lemma (in group0) finite_cosets:
assumes \( Finite(G) \), \( \text{IsAsubgroup}(H,P) \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \)
shows \( Finite(G//r) \)proof have fun: \( \{\langle g,r\{g\}\rangle .\ g\in G\}:G\rightarrow (G//r) \) unfolding Pi_def, function_def, domain_def
{
fix \( C \)
assume C: \( C\in G//r \)
have equiv: \( \text{equiv}(G,r) \) using Group_ZF_2_4_L3, assms(2) unfolding r_def
then have \( \text{refl}(G,r) \) unfolding equiv_def
with C have \( C\neq 0 \) using EquivClass_1_L5
then obtain \( c \) where c: \( c\in C \)
with C have \( r\{c\}=C \) using EquivClass_1_L2, equiv
with c, C have \( \langle c,C\rangle \in \{\langle g,r\{g\}\rangle .\ g\in G\} \) using EquivClass_1_L1, equiv
then have \( \{\langle g,r\{g\}\rangle .\ g\in G\}c=C \), \( c\in G \) using apply_equality, fun
then have \( \exists c\in G.\ \{\langle g,r\{g\}\rangle .\ g\in G\}c=C \)
with fun have surj: \( \{\langle g,r\{g\}\rangle .\ g\in G\}\in \text{surj}(G,G//r) \) unfolding surj_def
from assms(1) obtain \( n \) where \( n\in nat \), \( G\approx n \) unfolding Finite_def
then have G: \( G\preceq n \), \( Ord(n) \) using eqpoll_imp_lepoll
then have \( G//r\preceq G \) using surj_fun_inv_2, surj
with G(1) have \( G//r\preceq n \) using lepoll_trans
with \( n\in nat \) show \( Finite(G//r) \) using lepoll_nat_imp_Finite
qed
All the cosets are equipollent.
lemma (in group0) cosets_equipoll:
assumes \( \text{IsAsubgroup}(H,P) \), \( g1\in G \), \( g2\in G \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \)
shows \( r\{g1\} \approx r\{g2\} \)proof have equiv: \( \text{equiv}(G,r) \) using Group_ZF_2_4_L3, assms(1) unfolding r_def
from assms(3,2) have GG: \( (g1^{-1})\cdot g2\in G \) using inverse_in_group, group_op_closed
then have bij: \( \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)\in \text{bij}(G,G) \) using trans_bij(1)
have \( r\{g2\}\in G//r \) using assms(3) unfolding quotient_def
then have sub2: \( r\{g2\}\subseteq G \) using EquivClass_1_L1, equiv, assms(3)
have \( r\{g1\}\in G//r \) using assms(2) unfolding quotient_def
then have sub: \( r\{g1\}\subseteq G \) using EquivClass_1_L1, equiv, assms(2)
with bij have \( \text{restrict}( \text{RightTranslation}(G,P,(g1^{-1})\cdot g2),r\{g1\})\in \text{bij}(r\{g1\}, \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)(r\{g1\})) \) using restrict_bij unfolding bij_def
then have \( r\{g1\}\approx \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)(r\{g1\}) \) unfolding eqpoll_def
with GG, sub have A0: \( r\{g1\}\approx \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\} \) using func_imagedef, group0_5_L1(1)
{
fix \( t \)
assume \( t\in \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\} \)
then obtain \( q \) where q: \( t= \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)q \), \( q\in r\{g1\} \)
then have \( \langle g1,q\rangle \in r \), \( q\in G \) using image_iff, sub
then have \( g1\cdot (q^{-1})\in H \), \( q^{-1}\in G \) using inverse_in_group unfolding r_def, QuotientGroupRel_def
from GG, q, sub have t: \( t=q\cdot ((g1^{-1})\cdot g2) \) using group0_5_L2(1)
then have \( g2\cdot t^{-1}=g2\cdot (q\cdot ((g1^{-1})\cdot g2))^{-1} \)
with \( q\in G \), GG have \( g2\cdot t^{-1}=g2\cdot (((g1^{-1})\cdot g2)^{-1}\cdot q^{-1}) \) using group_inv_of_two
then have \( g2\cdot t^{-1}=g2\cdot (((g2^{-1})\cdot g1^{-1}^{-1})\cdot q^{-1}) \) using group_inv_of_two, inverse_in_group, assms(2), assms(3)
then have \( g2\cdot t^{-1}=g2\cdot (((g2^{-1})\cdot g1)\cdot q^{-1}) \) using group_inv_of_inv, assms(2)
moreover
have \( (g2^{-1})\cdot g1\in G \) using assms(2), inverse_in_group, assms(3), group_op_closed
with assms(3), \( q^{-1}\in G \) have \( g2\cdot (((g2^{-1})\cdot g1)\cdot q^{-1})=g2\cdot ((g2^{-1})\cdot g1)\cdot q^{-1} \) using group_oper_assoc
moreover have \( g2\cdot ((g2^{-1})\cdot g1)=g2\cdot (g2^{-1})\cdot g1 \) using assms(2), inverse_in_group, assms(3), group_oper_assoc
then have \( g2\cdot ((g2^{-1})\cdot g1)=g1 \) using group0_2_L6, assms(3), group0_2_L2, assms(2)
ultimately have \( g2\cdot t^{-1}=g1\cdot q^{-1} \)
with \( g1\cdot (q^{-1})\in H \) have \( g2\cdot t^{-1}\in H \)
moreover
from t, \( q\in G \), \( g2\in G \) have \( t\in G \) using inverse_in_group, assms(2), group_op_closed
ultimately have \( \langle g2,t\rangle \in r \) unfolding QuotientGroupRel_def, r_def using assms(3)
then have \( t\in r\{g2\} \) using image_iff, assms(4)
then have A1: \( \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\}\subseteq r\{g2\} \)
{
fix \( t \)
assume \( t\in r\{g2\} \)
then have \( \langle g2,t\rangle \in r \), \( t\in G \) using sub2, image_iff
then have H: \( g2\cdot t^{-1}\in H \) unfolding QuotientGroupRel_def, r_def
then have G: \( g2\cdot t^{-1}\in G \) using group0_3_L2, assms(1)
then have \( g1\cdot (g1^{-1}\cdot (g2\cdot t^{-1}))=g1\cdot g1^{-1}\cdot (g2\cdot t^{-1}) \) using group_oper_assoc, assms(2), inverse_in_group
with G have \( g1\cdot (g1^{-1}\cdot (g2\cdot t^{-1}))=g2\cdot t^{-1} \) using group0_2_L6, assms(2), group0_2_L2
with H have HH: \( g1\cdot (g1^{-1}\cdot (g2\cdot t^{-1}))\in H \)
from \( t\in G \) have GGG: \( t\cdot g2^{-1}\in G \) using inverse_in_group, assms(3), group_op_closed
from \( t\in G \) have \( (t\cdot g2^{-1})^{-1}=g2^{-1}^{-1}\cdot t^{-1} \) using group_inv_of_two, inverse_in_group, assms(3)
also
have \( \ldots =g2\cdot t^{-1} \) using group_inv_of_inv, assms(3)
finally have \( (t\cdot g2^{-1})^{-1}=g2\cdot t^{-1} \)
then have \( g1^{-1}\cdot (t\cdot g2^{-1})^{-1}=g1^{-1}\cdot (g2\cdot t^{-1}) \)
then have \( ((t\cdot g2^{-1})\cdot g1)^{-1}=g1^{-1}\cdot (g2\cdot t^{-1}) \) using group_inv_of_two, GGG, assms(2)
then have HHH: \( g1\cdot ((t\cdot g2^{-1})\cdot g1)^{-1}\in H \) using HH
from \( t\in G \) have \( (t\cdot g2^{-1})\cdot g1\in G \) using assms(2), inverse_in_group, assms(3), group_op_closed
with HHH have \( \langle g1,(t\cdot g2^{-1})\cdot g1\rangle \in r \) using assms(2) unfolding r_def, QuotientGroupRel_def
then have rg1: \( t\cdot g2^{-1}\cdot g1\in r\{g1\} \) using image_iff
from assms(3) have \( g2^{-1}:G \) using inverse_in_group
from \( t\in G \) have \( t\cdot g2^{-1}\cdot g1\cdot ((g1^{-1})\cdot g2)=t\cdot (g2^{-1}\cdot g1)\cdot ((g1^{-1})\cdot g2) \) using group_oper_assoc, inverse_in_group, assms(3), assms(2)
also
from \( t\in G \) have \( \ldots =t\cdot ((g2^{-1}\cdot g1)\cdot ((g1^{-1})\cdot g2)) \) using group_oper_assoc, group_op_closed, inverse_in_group, assms(3), assms(2)
also from GG, \( g2^{-1}:G \) have \( \ldots =t\cdot (g2^{-1}\cdot (g1\cdot ((g1^{-1})\cdot g2))) \) using group_oper_assoc, assms(2)
also have \( \ldots =t\cdot (g2^{-1}\cdot (g1\cdot (g1^{-1})\cdot g2)) \) using group_oper_assoc, assms(2), inverse_in_group, assms(3)
also from \( t\in G \) have \( \ldots =t \) using group0_2_L6, assms(3), group0_2_L6, assms(2), group0_2_L2, assms(3)
finally have \( t\cdot g2^{-1}\cdot g1\cdot ((g1^{-1})\cdot g2)=t \)
with \( (t\cdot g2^{-1})\cdot g1\in G \), GG have \( \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)(t\cdot g2^{-1}\cdot g1)=t \) using group0_5_L2(1)
then have \( t\in \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\} \) using rg1
then have \( r\{g2\}\subseteq \{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\} \)
with A1 have \( r\{g2\}=\{ \text{RightTranslation}(G,P,(g1^{-1})\cdot g2)t.\ t\in r\{g1\}\} \)
with A0 show \( thesis \)
qed
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) \), \( \text{IsAsubgroup}(H,P) \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \)
shows \( |G|=|H| \cdot |G//r| \)proof have equiv: \( \text{equiv}(G,r) \) using Group_ZF_2_4_L3, assms(2) unfolding r_def
have \( r\{1 \} \subseteq G \) unfolding r_def, QuotientGroupRel_def
have \( \forall aa\in G.\ aa\in H \longleftrightarrow \langle aa,1 \rangle \in r \) using Group_ZF_2_4_L5C unfolding r_def
then have \( \forall aa\in G.\ aa\in H \longleftrightarrow \langle 1 ,aa\rangle \in r \) using equiv unfolding sym_def, equiv_def
then have \( \forall aa\in G.\ aa\in H \longleftrightarrow aa\in r\{1 \} \) using image_iff
with \( r\{1 \} \subseteq G \) have H: \( H=r\{1 \} \) using group0_3_L2, assms(2)
{
fix \( c \)
assume \( c\in (G//r) \)
then obtain \( g \) where \( g\in G \), \( c=r\{g\} \) unfolding quotient_def
then have \( c\approx r\{1 \} \) using cosets_equipoll, assms(2), group0_2_L2 unfolding r_def
then have \( |c|=|H| \) using H, cardinal_cong
then have \( \forall c\in (G//r).\ |c|=|H| \)
moreover
qed
have \( Finite(G//r) \) using assms, finite_cosets
moreover have \( \bigcup (G//r)=G \) using Union_quotient, Group_ZF_2_4_L3, assms(2,3)
moreover from \( \bigcup (G//r)=G \) have \( Finite(\bigcup (G//r)) \) using assms(1)
moreover have \( \forall c1\in (G//r).\ \forall c2\in (G//r).\ c1\neq c2 \longrightarrow c1\cap c2=0 \) using quotient_disj, equiv
ultimately show \( thesis \) using card_partition
Subgroups generated by sets
In this section we study the minimal subgroup containing a set
Since G is always a group containing the set, we may take the intersection of all subgroups bigger than the set; and hence the result is the subgroup we searched.
definition (in group0)
\( X\subseteq G \Longrightarrow \langle X\rangle _G \equiv \bigcap \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\} \)
Every generated subgroup is a subgroup
theorem (in group0) subgroupGen_is_subgroup:
assumes \( X\subseteq G \)
shows \( \text{IsAsubgroup}(\langle X\rangle _G,P) \)proof have \( \text{restrict}(P,G\times G)=P \) using group_oper_fun, restrict_idem unfolding Pi_def
then have \( \text{IsAsubgroup}(G,P) \) unfolding IsAsubgroup_def using groupAssum
with assms have \( G\in \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\} \)
then have \( \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}\neq 0 \)
then show \( thesis \) using subgroup_inter, SubgroupGenerated_def, assms
qed
The generated subgroup contains the original set
theorem (in group0) subgroupGen_contains_set:
assumes \( X\subseteq G \)
shows \( X \subseteq \langle X\rangle _G \)proof have \( \text{restrict}(P,G\times G)=P \) using group_oper_fun, restrict_idem unfolding Pi_def
then have \( \text{IsAsubgroup}(G,P) \) unfolding IsAsubgroup_def using groupAssum
with assms have \( G\in \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\} \)
then have \( \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\}\neq 0 \)
then show \( thesis \) using subgroup_inter, SubgroupGenerated_def, assms
qed
Given a subgroup that contains a set, the generated subgroup from that set is smaller than this subgroup
theorem (in group0) subgroupGen_minimal:
assumes \( \text{IsAsubgroup}(H,P) \), \( X\subseteq H \)
shows \( \langle X\rangle _G \subseteq H \)proof from assms have sub: \( X\subseteq G \) using group0_3_L2
from assms have \( H\in \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\} \) using group0_3_L2
then show \( thesis \) using sub, subgroup_inter, SubgroupGenerated_def, assms
qed
end
lemma (in group0) group0_3_L2:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( H \subseteq G \) lemma (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \) theorem (in group0) group0_3_T3A:
assumes \( \text{IsAsubgroup}(H,P) \) and \( h\in H \)
shows \( h^{-1}\in H \) lemma (in group0) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) lemma (in group0) group_inv_of_two:
assumes \( a\in G \) and \( b\in G \)
shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \) lemma (in group0) group_inv_of_inv:
assumes \( a\in G \)
shows \( a = (a^{-1})^{-1} \) lemma (in group0) group_oper_assoc:
assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \) lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group0) group0_2_L6:
assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \) lemma (in group0) group0_3_L6:
assumes \( \text{IsAsubgroup}(H,P) \) and \( a\in H \), \( b\in H \)
shows \( a\cdot b \in H \)Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma (in group0) group0_3_L5:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( 1 \in H \) theorem (in group0) group0_3_T3:
assumes \( H\neq 0 \) and \( H\subseteq G \) and \( H \text{ is closed under } P \) and \( \forall x\in H.\ x^{-1} \in H \)
shows \( \text{IsAsubgroup}(H,P) \) lemma (in group0) group0_2_L19:
assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\neq b \)
shows \( a\cdot c \neq b\cdot c \) and \( c\cdot a \neq c\cdot b \) lemma (in group0) group0_2_L19:
assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\neq b \)
shows \( a\cdot c \neq b\cdot c \) and \( c\cdot a \neq c\cdot b \)Definition of IsAnormalSubgroup:
\( \text{IsAnormalSubgroup}(G,P,N) \equiv \text{IsAsubgroup}(N,P) \wedge \)
\( (\forall n\in N.\ \forall g\in G.\ P\langle P\langle g,n \rangle , \text{GroupInv}(G,P)(g) \rangle \in N) \)
theorem (in group0) conj_group_is_group:
assumes \( \text{IsAsubgroup}(H,P) \), \( g\in G \)
shows \( \text{IsAsubgroup}(\{g\cdot (h\cdot g^{-1}).\ h\in H\},P) \) theorem (in group0) conj_set_is_eqpoll:
assumes \( H\subseteq G \), \( g\in G \)
shows \( H\approx \{g\cdot (h\cdot g^{-1}).\ h\in H\} \) theorem (in group0) cont_conj_is_normal:
assumes \( \text{IsAsubgroup}(H,P) \), \( \forall g\in G.\ \{g\cdot (h\cdot g^{-1}).\ h\in H\}\subseteq H \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \) lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
corollary (in group0) only_one_equipoll_sub:
assumes \( \text{IsAsubgroup}(H,P) \), \( \forall M.\ \text{IsAsubgroup}(M,P)\wedge H\approx M \longrightarrow M=H \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \)Definition of IsSimple:
\( [G,f]\text{ is a simple group } \equiv \text{IsAgroup}(G,f) \wedge (\forall M.\ \text{IsAnormalSubgroup}(G,f,M) \longrightarrow M=G\vee M=\{\text{ TheNeutralElement}(G,f)\}) \)
lemma Group_ZF_2_4_L6:
assumes \( \text{IsAgroup}(G,P) \) and \( P \text{ is commutative on } G \) and \( \text{IsAsubgroup}(H,P) \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \), \( \text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H)) \) lemma (in group0) Group_ZF_2_4_L3:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{equiv}(G, \text{QuotientGroupRel}(G,P,H)) \) lemma EquivClass_1_L5:
assumes \( \text{refl}(A,r) \) and \( C \in A//r \)
shows \( C\neq 0 \) lemma EquivClass_1_L2:
assumes \( \text{equiv}(A,r) \), \( C \in A//r \) and \( x\in C \)
shows \( r\{x\} = C \) lemma EquivClass_1_L1:
assumes \( \text{equiv}(A,r) \) and \( C \in A//r \) and \( x\in C \)
shows \( x\in A \) theorem surj_fun_inv_2:
assumes \( f:\text{surj}(A,B) \), \( A\preceq Q \), \( Ord(Q) \)
shows \( B\preceq A \) lemma (in group0) trans_bij:
assumes \( g\in G \)
shows \( \text{RightTranslation}(G,P,g) \in \text{bij}(G,G) \) and \( \text{LeftTranslation}(G,P,g) \in \text{bij}(G,G) \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma (in group0) group0_5_L1:
assumes \( g\in G \)
shows \( \text{RightTranslation}(G,P,g) : G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g) : G\rightarrow G \)Definition of QuotientGroupRel:
\( \text{QuotientGroupRel}(G,P,H) \equiv \)
\( \{\langle a,b\rangle \in G\times G.\ P\langle a, \text{GroupInv}(G,P)(b)\rangle \in H\} \)
lemma (in group0) group0_5_L2:
assumes \( g\in G \), \( a\in G \)
shows \( \text{RightTranslation}(G,P,g)(a) = a\cdot g \), \( \text{LeftTranslation}(G,P,g)(a) = g\cdot a \) lemma (in group0) Group_ZF_2_4_L5C:
assumes \( a\in G \)
shows \( \langle a,1 \rangle \in \text{QuotientGroupRel}(G,P,H) \longleftrightarrow a\in H \) lemma (in group0) cosets_equipoll:
assumes \( \text{IsAsubgroup}(H,P) \), \( g1\in G \), \( g2\in G \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \)
shows \( r\{g1\} \approx r\{g2\} \) lemma (in group0) finite_cosets:
assumes \( Finite(G) \), \( \text{IsAsubgroup}(H,P) \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \)
shows \( Finite(G//r) \) lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
Definition of IsAsubgroup:
\( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H)) \)
lemma (in group0) subgroup_inter:
assumes \( \ \lt H>\neq 0 \) and \( \forall H\in \ \lt H>.\ \text{IsAsubgroup}(H,P) \)
shows \( \text{IsAsubgroup}(\bigcap \ \lt H>,P) \)Definition of SubgroupGenerated:
\( X\subseteq G \Longrightarrow \langle X\rangle _G \equiv \bigcap \{H\in Pow(G).\ X\subseteq H \wedge \text{IsAsubgroup}(H,P)\} \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8