begin
When the operation \(P\) in the group \((G,P)\) is commutative (i.e. the group the abelian) the space \( \text{End}(G,P) \) of homomorphisms of a group \((G,P)\) into itself has a nice structure.
First ring of endomorphisms of an abelian group
In this section we show that for an abelian group \((G,P)\) the space \( \text{End}(G,P) \) (defined in the Group_ZF_2 theory) forms a ring.
The set of endomorphisms is closed under pointwise addition (derived from the group operation). This is so because the group is abelian.
theorem (in abelian_group) end_pointwise_addition:
assumes \( f\in \text{End}(G,P) \), \( g\in \text{End}(G,P) \)
defines \( F \equiv P \text{ lifted to function space over } G \)
shows \( F\langle f,g\rangle \in \text{End}(G,P) \)proof from assms(1,2) have fun: \( f:G\rightarrow G \), \( g\in G\rightarrow G \) unfolding End_def
with assms(3) have fun2: \( F\langle f,g\rangle :G\rightarrow G \) using Group_ZF_2_1_L0, group0_2_L1
{
fix \( g_1 \) \( g_2 \)
assume \( g_1\in G \), \( g_2\in G \)
with isAbelian, assms, fun have \( (F\langle f,g\rangle )(g_1\cdot g_2) = (F\langle f,g\rangle )(g_1)\cdot (F\langle f,g\rangle )(g_2) \) using Group_ZF_2_1_L3, group_op_closed, endomor_eq, apply_type, group0_4_L8(3), Group_ZF_2_1_L3
with fun2 show \( thesis \) using eq_endomor
qed
The value of a product of endomorphisms on a group element is the product of values.
lemma (in abelian_group) end_pointwise_add_val:
assumes \( f\in \text{End}(G,P) \), \( g\in \text{End}(G,P) \), \( x\in G \), \( F = P \text{ lifted to function space over } G \)
shows \( (\text{InEnd}(F,G,P)\langle f,g\rangle )(x) = (f(x))\cdot (g(x)) \) using assms, group_oper_fun, group0_1_L3B, func_ZF_1_L4 unfolding End_defThe operation of taking the inverse in an abelian group is an endomorphism.
lemma (in abelian_group) end_inverse_group:
shows \( \text{GroupInv}(G,P) \in \text{End}(G,P) \) using inverse_in_group, group_inv_of_two, isAbelian, IsCommutative_def, group0_2_T2, groupAssum, Homomor_def unfolding End_def, IsMorphism_defThe set of homomorphisms of an abelian group is an abelian subgroup of the group of functions from a set to a group, under pointwise addition.
theorem (in abelian_group) end_addition_group:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsAgroup}( \text{End}(G,P),\text{InEnd}(F,G,P)) \) and \( \text{InEnd}(F,G,P) \text{ is commutative on } \text{End}(G,P) \)proof have \( \text{End}(G,P)\neq 0 \) using end_comp_monoid(1), group0_1_L3A unfolding monoid0_def
moreover
have \( \text{End}(G,P) \subseteq G\rightarrow G \) unfolding End_def
moreover from isAbelian, assms(1) have \( \text{End}(G,P)\text{ is closed under } F \) unfolding IsOpClosed_def using end_pointwise_addition
moreover from groupAssum, assms(1) have \( \forall f\in \text{End}(G,P).\ \text{GroupInv}(G\rightarrow G,F)(f) \in \text{End}(G,P) \) using group0_1_L1, end_composition(1), end_inverse_group, func_ZF_5_L2, group0_2_T2, Group_ZF_2_1_L6 unfolding monoid0_def, End_def
ultimately show \( \text{IsAgroup}( \text{End}(G,P),\text{InEnd}(F,G,P)) \) using assms(1), group0_3_T3, Group_ZF_2_1_T2 unfolding IsAsubgroup_def, group0_def
from assms(1), isAbelian show \( \text{InEnd}(F,G,P) \text{ is commutative on } \text{End}(G,P) \) using Group_ZF_2_1_L7 unfolding End_def, IsCommutative_def
qed
Endomorphisms form a subgroup of the space of functions that map the group to itself.
lemma (in abelian_group) end_addition_subgroup:
shows \( \text{IsAsubgroup}( \text{End}(G,P),P \text{ lifted to function space over } G) \) using end_addition_group unfolding IsAsubgroup_defThe neutral element of the group of endomorphisms of a group is the constant function with value equal to the neutral element of the group.
lemma (in abelian_group) end_add_neut_elem:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{ TheNeutralElement}( \text{End}(G,P),\text{InEnd}(F,G,P)) = \text{ConstantFunction}(G,1 ) \) using assms, end_addition_subgroup, lift_group_subgr_neutFor the endomorphisms of a group \(G\) the group operation lifted to the function space over \(G\) is distributive with respect to the composition operation.
lemma (in abelian_group) distributive_comp_pointwise:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsDistributive}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P)) \)proof let \( C_G = \text{Composition}(G) \)
let \( C_E = \text{InEnd}(C_G,G,P) \)
let \( F_E = \text{InEnd}(F,G,P) \)
{
fix \( b \) \( c \) \( d \)
assume AS: \( b\in \text{End}(G,P) \), \( c\in \text{End}(G,P) \), \( d\in \text{End}(G,P) \)
with assms(1) have ig1: \( C_G \langle b, F \langle c, d\rangle \rangle = b\circ (F\langle c,d\rangle ) \) using Group_ZF_2_1_L0, func_ZF_5_L2 unfolding End_def
with AS have ig2: \( F\langle C_G\langle b,c\rangle ,C_G \langle b,d\rangle \rangle = F\langle b\circ c,b\circ d\rangle \) unfolding End_def using func_ZF_5_L2
from assms(1), AS have comp1fun: \( (b\circ (F\langle c,d\rangle )):G\rightarrow G \) using Group_ZF_2_1_L0, comp_fun unfolding End_def
from assms(1), AS have comp2fun: \( (F \langle b\circ c,b\circ d\rangle ) : G\rightarrow G \) using Group_ZF_2_1_L0, comp_fun unfolding End_def
{
fix \( g \)
assume \( g\in G \)
with assms(1), AS(2,3) have \( (b\circ (F\langle c,d\rangle ))(g) = b((F\langle c,d\rangle )(g)) \) using comp_fun_apply, Group_ZF_2_1_L0 unfolding End_def
with groupAssum, assms(1), AS, \( g\in G \) have \( (b\circ (F\langle c,d\rangle ))(g) = (F\langle b\circ c,b\circ d\rangle )(g) \) using Group_ZF_2_1_L3, apply_type, homomor_eq, comp_fun unfolding End_def
hence \( \forall g\in G.\ (b\circ (F\langle c,d\rangle ))(g) = (F\langle b\circ c,b\circ d\rangle )(g) \)
with comp1fun, comp2fun, ig1, ig2 have \( C_G\langle b,F\langle c, d\rangle \rangle = F\langle C_G\langle b , c\rangle ,C_G\langle b,d\rangle \rangle \) using func_eq
moreover
from AS(2,3) have \( F\langle c, d\rangle = F_E\langle c, d\rangle \) using restrict
moreover from AS have \( C_G\langle b,c\rangle = C_E\langle b,c\rangle \) and \( C_G\langle b,d\rangle = C_E\langle b,d\rangle \) using restrict
moreover from assms, AS have \( C_G\langle b,F \langle c,d\rangle \rangle = C_E\langle b, F\langle c, d\rangle \rangle \) using end_pointwise_addition
moreover from AS have \( F\langle C_G\langle b,c\rangle ,C_G\langle b,d\rangle \rangle = F_E\langle C_G \langle b,c\rangle ,C_G \langle b,d\rangle \rangle \) using end_composition
ultimately have eq1: \( C_E\langle b, F_E\langle c,d\rangle \rangle = F_E \langle C_E\langle b,c\rangle ,C_E\langle b,d\rangle \rangle \)
from assms(1), AS have compfun: \( (F\langle c,d\rangle )\circ b : G\rightarrow G \), \( F\langle c\circ b,d\circ b\rangle : G\rightarrow G \) using Group_ZF_2_1_L0, comp_fun unfolding End_def
{
fix \( g \)
assume \( g\in G \)
with AS(1) have bg: \( b(g) \in G \) unfolding End_def using apply_type
from \( g\in G \), AS(1) have \( ((F\langle c,d\rangle )\circ b)g = (F\langle c,d\rangle )(b(g)) \) using comp_fun_apply unfolding End_def
also
from assms(1), AS(2,3), bg have \( \ldots = (c(b(g)))\cdot (d(b(g))) \) using Group_ZF_2_1_L3 unfolding End_def
also from \( g\in G \), AS have \( \ldots = ((c\circ b)(g))\cdot ((d\circ b)(g)) \) using comp_fun_apply unfolding End_def
also from assms(1), \( g\in G \), AS have \( \ldots = (F\langle c\circ b,d\circ b\rangle )g \) using comp_fun, Group_ZF_2_1_L3 unfolding End_def
finally have \( ((F\langle c,d\rangle )\circ b)(g) = (F\langle c\circ b,d\circ b\rangle )(g) \)
hence \( \forall g\in G.\ ((F\langle c,d\rangle )\circ b)(g) = (F\langle c\circ b,d\circ b\rangle )(g) \)
with compfun have \( (F\langle c,d\rangle )\circ b = F\langle c\circ b,d\circ b\rangle \) using func_eq
with assms(1), AS have \( C_G\langle F\langle c,d\rangle ,b\rangle = F\langle C_G\langle c,b\rangle ,C_G\langle d , b\rangle \rangle \) using Group_ZF_2_1_L0, func_ZF_5_L2 unfolding End_def
moreover
from AS(2,3) have \( F\langle c, d\rangle = F_E\langle c, d\rangle \) using restrict
moreover from AS have \( C_G\langle c,b\rangle = C_E\langle c , b\rangle \), \( C_G\langle d,b\rangle = C_E\langle d,b\rangle \) using restrict
moreover from assms, AS have \( C_G\langle F\langle c,d\rangle ,b\rangle = C_E\langle F\langle c,d\rangle ,b\rangle \) using end_pointwise_addition
moreover from AS have \( F\langle C_G\langle c,b\rangle ,C_G\langle d,b\rangle \rangle = F_E\langle C_G\langle c,b\rangle ,C_G\langle d,b\rangle \rangle \) using end_composition
ultimately have \( C_E\langle F_E\langle c,d\rangle ,b\rangle = F_E\langle C_E\langle c,b\rangle ,C_E\langle d,b\rangle \rangle \)
with eq1 have \( (C_E\langle b, F_E\langle c, d\rangle \rangle = F_E\langle C_E\langle b,c\rangle ,C_E\langle b,d\rangle \rangle ) \wedge \)
\( (C_E\langle F_E\langle c,d\rangle ,b\rangle = F_E\langle C_E\langle c,b\rangle ,C_E\langle d,b\rangle \rangle ) \)
then show \( thesis \) unfolding IsDistributive_def
qed
The endomorphisms of an abelian group is in fact a ring with the previous operations.
theorem (in abelian_group) end_is_ring:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsAring}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P)) \) using assms, end_addition_group, end_comp_monoid(1), distributive_comp_pointwise unfolding IsAring_defThe theorems proven in the ring0 context are valid in the abelian_group context as applied to the endomorphisms of \(G\).
sublocale abelian_group < endo_ring: ring0
using end_is_ring unfolding ring0_def
First isomorphism theorem
Now we will prove that any homomorphism \(f:G\to H\) defines a bijective homomorphism between \(G/H\) and \(f(G)\).
A group homomorphism sends the neutral element to the neutral element.
lemma image_neutral:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( f(\text{ TheNeutralElement}(G,P)) = \text{ TheNeutralElement}(H,F) \)proof let \( e_G = \text{ TheNeutralElement}(G,P) \)
let \( e_H = \text{ TheNeutralElement}(H,F) \)
from assms(3) have ff: \( f:G\rightarrow H \) unfolding Homomor_def
have g: \( e_G = P\langle e_G,e_G\rangle \), \( e_G \in G \) using assms(1), group0_2_L2 unfolding group0_def
with assms have \( f(e_G) = F\langle f(e_G),f(e_G)\rangle \) unfolding Homomor_def, IsMorphism_def
moreover
from ff, g(2) have h: \( f(e_G) \in H \) using apply_type
with assms(2) have \( f(e_G) = F\langle f(e_G),e_H\rangle \) using group0_2_L2 unfolding group0_def
ultimately have \( F\langle f(e_G),e_H\rangle = F\langle f(e_G),f(e_G)\rangle \)
with assms(2), h have \( \text{LeftTranslation}(H,F,f(e_G))(e_H) = \text{LeftTranslation}(H,F,f(e_G))(f(e_G)) \) using group0_5_L2(2), group0_2_L2 unfolding group0_def
moreover
qed
from assms(2), h have \( \text{LeftTranslation}(H,F,f(e_G))\in \text{inj}(H,H) \) using trans_bij(2) unfolding group0_def, bij_def
ultimately show \( thesis \) using h, assms(2), group0_2_L2 unfolding inj_def, group0_def
If \(f:G\rightarrow H\) is a homomorphism, then it commutes with the inverse
lemma image_inv:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( g\in G \)
shows \( f( \text{GroupInv}(G,P)(g)) = \text{GroupInv}(H,F)(f(g)) \)proof from assms(3) have ff: \( f:G\rightarrow H \) unfolding Homomor_def
with assms(4) have im: \( f(g)\in H \) using apply_type
from assms(1,4) have inv: \( \text{GroupInv}(G,P)(g)\in G \) using inverse_in_group unfolding group0_def
with ff have inv2: \( f( \text{GroupInv}(G,P)g)\in H \) using apply_type
from assms(1,4) have \( f(\text{ TheNeutralElement}(G,P)) = f(P\langle g, \text{GroupInv}(G,P)(g)\rangle ) \) using group0_2_L6 unfolding group0_def
also
qed
from assms, inv have \( \ldots = F\langle f(g),f( \text{GroupInv}(G,P)(g))\rangle \) unfolding Homomor_def, IsMorphism_def
finally have \( f(\text{ TheNeutralElement}(G,P)) = F\langle f(g),f( \text{GroupInv}(G,P)(g))\rangle \)
with assms, im, inv2 show \( thesis \) using group0_2_L9, image_neutral unfolding group0_def
The preimage of a subgroup is a subgroup
theorem preimage_sub:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( \text{IsAsubgroup}(K,F) \)
shows \( \text{IsAsubgroup}(f^{-1}(K),P) \)proof from assms(3) have ff: \( f:G\rightarrow H \) unfolding Homomor_def
from assms(2) have Hgr: \( group0(H,F) \) unfolding group0_def
from assms(1) have Ggr: \( group0(G,P) \) unfolding group0_def
moreover
qed
from assms, ff, Ggr, Hgr have \( \text{ TheNeutralElement}(G,P) \in f^{-1}(K) \) using image_neutral, group0_3_L5, func1_1_L15, group0_2_L2
hence \( f^{-1}(K)\neq 0 \)
moreover from ff have \( f^{-1}(K) \subseteq G \) using func1_1_L3
moreover from assms, ff, Ggr, Hgr have \( f^{-1}(K) \text{ is closed under } P \) using func1_1_L15, group0_3_L6, group_op_closed, func1_1_L15 unfolding IsOpClosed_def, Homomor_def, IsMorphism_def
moreover from assms, ff, Ggr, Hgr have \( \forall x\in f^{-1}(K).\ \text{GroupInv}(G, P)(x) \in f^{-1}(K) \) using group0_3_T3A, image_inv, func1_1_L15, inverse_in_group
ultimately show \( thesis \) by (rule group0_3_T3 )
The preimage of a normal subgroup is normal
theorem preimage_normal_subgroup:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( \text{IsAnormalSubgroup}(H,F,K) \)
shows \( \text{IsAnormalSubgroup}(G,P,f^{-1}(K)) \)proof from assms(3) have ff: \( f:G\rightarrow H \) unfolding Homomor_def
from assms(2) have Hgr: \( group0(H,F) \) unfolding group0_def
with assms(4) have \( K\subseteq H \) using group0_3_L2 unfolding IsAnormalSubgroup_def
from assms(1) have Ggr: \( group0(G,P) \) unfolding group0_def
moreover
}
}
qed
from assms have \( \text{IsAsubgroup}(f^{-1}(K),P) \) using preimage_sub unfolding IsAnormalSubgroup_def
moreover {
fix \( g \)
assume gG: \( g\in G \)
{
fix \( h \)
assume \( h \in \{P\langle g,P\langle h, \text{GroupInv}(G, P)(g)\rangle \rangle .\ h \in f^{-1}(K)\} \)
then obtain \( k \) where k: \( h = P\langle g,P\langle k, \text{GroupInv}(G, P)(g)\rangle \rangle \), \( k \in f^{-1}(K) \)
from k(1) have \( f(h) = f(P\langle g,P\langle k, \text{GroupInv}(G, P)(g)\rangle \rangle ) \)
moreover
from ff, k(2) have \( k\in G \) using vimage_iff unfolding Pi_def
ultimately have f: \( f(h) = F\langle f(g),F\langle f(k), \text{GroupInv}(H,F)(f(g))\rangle \rangle \) using assms(1-4), Ggr, gG, group_op_closed, inverse_in_group, image_inv, homomor_eq
from assms(1), ff, Ggr, \( g\in G \), k have \( h\in G \) using group_op_closed, inverse_in_group, func1_1_L15
from assms(4), ff, k(2), \( g\in G \) have \( f(k)\in K \), \( f(g)\in H \) and \( F\langle F\langle f(g),f(k)\rangle , \text{GroupInv}(H,F)(f(g))\rangle \in K \) using func1_1_L15, apply_type unfolding IsAnormalSubgroup_def
moreover
from \( f(k)\in K \), \( K\subseteq H \), Hgr, f, \( f(g)\in H \) have \( f(h) = F\langle F\langle f(g),f(k)\rangle , \text{GroupInv}(H,F)(f(g))\rangle \) using group_oper_assoc, inverse_in_group
ultimately have \( f(h) \in K \)
with ff, \( h\in G \) have \( h \in f^{-1}(K) \) using func1_1_L15
hence \( \{P\langle g,P\langle h, \text{GroupInv}(G,P)(g)\rangle \rangle .\ h\in f^{-1}(K)\} \subseteq f^{-1}(K) \)
hence \( \forall g\in G.\ \{P\langle g, P\langle h, \text{GroupInv}(G, P)(g)\rangle \rangle .\ h\in f^{-1}(K)\} \subseteq f^{-1}(K) \)
ultimately show \( thesis \) using cont_conj_is_normal
The kernel of an homomorphism is a normal subgroup.
corollary kernel_normal_sub:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( \text{IsAnormalSubgroup}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\}) \) using assms, preimage_normal_subgroup, trivial_normal_subgroup unfolding group0_defThe image of a subgroup is a subgroup
theorem image_subgroup:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( f:G\rightarrow H \), \( \text{IsAsubgroup}(K,P) \)
shows \( \text{IsAsubgroup}(fK,F) \)proof from assms(1,5) have sub: \( K\subseteq G \) using group0_3_L2 unfolding group0_def
from assms(2) have \( group0(H,F) \) unfolding group0_def
moreover
}
}
qed
from assms(4) have \( f(K) \subseteq H \) using func_imagedef, sub, apply_type
moreover from assms(1,4,5), sub have \( f(\text{ TheNeutralElement}(G,P)) \in f(K) \) using group0_3_L5, func_imagedef unfolding group0_def
hence \( f(K) \neq 0 \)
moreover {
fix \( x \)
assume \( x\in f(K) \)
with assms(4), sub obtain \( q \) where q: \( q\in K \), \( x=f(q) \) using func_imagedef
with assms(1-4), sub have \( \text{GroupInv}(H,F)(x) = f( \text{GroupInv}(G,P)q) \) using image_inv
with assms(1,4,5), q(1), sub have \( \text{GroupInv}(H,F)(x) \in f(K) \) using group0_3_T3A, func_imagedef unfolding group0_def
hence \( \forall x\in f(K).\ \text{GroupInv}(H, F)(x) \in f(K) \)
moreover {
fix \( x \) \( y \)
assume \( x\in f(K) \), \( y\in f(K) \)
with assms(4), sub obtain \( q_x \) \( q_y \) where q: \( q_x\in K \), \( x=f(q_x) \), \( q_y\in K \), \( y=f(q_y) \) using func_imagedef
with assms(1-3), sub have \( F\langle x,y\rangle = f(P\langle q_x,q_y\rangle ) \) using homomor_eq
moreover
from assms(1,5), q(1,3) have \( P\langle q_x,q_y\rangle \in K \) using group0_3_L6 unfolding group0_def
ultimately have \( F\langle x,y\rangle \in f(K) \) using assms(4), sub, func_imagedef
then have \( f(K) \text{ is closed under } F \) unfolding IsOpClosed_def
ultimately show \( thesis \) using group0_3_T3
The image of a group under a homomorphism is a subgroup of the target group.
corollary image_group:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( \text{IsAsubgroup}(f(G),F) \)proof from assms(1) have \( \text{restrict}(P,G\times G) = P \) using group_oper_fun, restrict_domain unfolding group0_def
with assms show \( thesis \) using image_subgroup unfolding Homomor_def, IsAsubgroup_def
qed
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 \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\}) \) and \( \mathcal{P} \equiv \text{QuotientGroupOp}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\}) \)
shows \( \exists \mathfrak{f} .\ \text{Homomor}(\mathfrak{f} ,G//r,\mathcal{P},f(G),\text{restrict}(F,(f(G))\times (f(G)))) \wedge \mathfrak{f} \in \text{bij}(G//r,f(G)) \)proof let \( \mathfrak{f} = \{\langle r\{g\},f(g)\rangle .\ g\in G\} \)
from assms(3) have ff: \( f:G\rightarrow H \) unfolding Homomor_def
from assms(1-5) have \( \text{equiv}(G,r) \) using Group_ZF_2_4_L3, kernel_normal_sub unfolding group0_def, IsAnormalSubgroup_def
from assms(4), ff have \( \mathfrak{f} \in Pow((G//r)\times f(G)) \) unfolding quotient_def using func_imagedef
moreover
}
{
have \( (G//r) \subseteq domain(\mathfrak{f} ) \) unfolding domain_def, quotient_def
moreover {
fix \( x \) \( y \) \( t \)
assume A: \( \langle x,y\rangle \in \mathfrak{f} \), \( \langle x,t\rangle \in \mathfrak{f} \)
then obtain \( g_y \) \( g_r \) where \( \langle x, y\rangle =\langle r\{g_y\},f(g_y)\rangle \), \( \langle x, t\rangle =\langle r\{g_r\},f(g_r)\rangle \) and \( g_r\in G \), \( g_y\in G \)
hence B: \( r\{g_y\}=r\{g_r\} \), \( y=f(g_y) \), \( t=f(g_r) \)
from ff, \( g_y\in G \), \( g_r\in G \), B(2,3) have \( y\in H \), \( t\in H \) using apply_type
with \( \text{equiv}(G,r) \), \( g_r\in G \), \( r\{g_y\}=r\{g_r\} \) have \( \langle g_y,g_r\rangle \in r \) using same_image_equiv
with assms(4), ff have \( f(P\langle g_y, \text{GroupInv}(G,P)(g_r)\rangle ) = \text{ TheNeutralElement}(H,F) \) unfolding QuotientGroupRel_def using func1_1_L15
with assms(1-4), B(2,3), \( g_y\in G \), \( g_r\in G \), \( y\in H \), \( t\in H \) have \( y=t \) using image_inv, inverse_in_group, group0_2_L11A unfolding group0_def, Homomor_def, IsMorphism_def
hence \( \forall x y.\ \langle x,y\rangle \in \mathfrak{f} \longrightarrow (\forall z.\ \langle x,z\rangle \in \mathfrak{f} \longrightarrow y=z) \)
ultimately have ff_fun: \( \mathfrak{f} :G//r\rightarrow f(G) \) unfolding Pi_def, function_def
fix \( a_1 \) \( a_2 \)
assume AS: \( a_1\in G//r \), \( a_2\in G//r \)
then obtain \( g_1 \) \( g_2 \) where \( g_1\in G \), \( g_2\in G \) and a: \( a_1=r\{g_1\} \), \( a_2=r\{g_2\} \) unfolding quotient_def
with assms, \( \text{equiv}(G,r) \) have \( \langle \mathcal{P}\langle a_1,a_2\rangle ,f(P\langle g_1,g_2\rangle )\rangle \in \mathfrak{f} \) using Group_ZF_2_4_L5A, kernel_normal_sub, Group_ZF_2_2_L2, group_op_closed unfolding QuotientGroupOp_def, group0_def
with ff_fun have eq: \( \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle ) = f(P\langle g_1,g_2\rangle ) \) using apply_equality
from \( g_1\in G \), \( g_2\in G \), a have \( \langle a_1,f(g_1)\rangle \in \mathfrak{f} \) and \( \langle a_2,f(g_2)\rangle \in \mathfrak{f} \)
with assms(1,2,3), ff_fun, \( g_1\in G \), \( g_2\in G \), eq have \( F\langle \mathfrak{f} (a_1),\mathfrak{f} (a_2)\rangle = \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle ) \) using apply_equality unfolding Homomor_def, IsMorphism_def
moreover
from AS, ff_fun have \( \mathfrak{f} (a_1) \in f(G) \), \( \mathfrak{f} (a_2) \in f(G) \) using apply_type
ultimately have \( \text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (a_1),\mathfrak{f} (a_2)\rangle = \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle ) \)
hence r: \( \forall a_1\in G//r.\ \forall a_2\in G//r.\ \text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (a_1),\mathfrak{f} (a_2)\rangle = \mathfrak{f} (\mathcal{P}\langle a_1,a_2\rangle ) \)
with ff_fun have HOM: \( \text{Homomor}(\mathfrak{f} ,G//r,\mathcal{P},f(G),\text{restrict}(F,(f(G))\times (f(G)))) \) unfolding Homomor_def, IsMorphism_def
from assms have G: \( \text{IsAgroup}(G//r,\mathcal{P}) \) and H: \( \text{IsAgroup}(f(G), \text{restrict}(F,f(G)\times f(G))) \) using Group_ZF_2_4_T1, kernel_normal_sub, image_group unfolding IsAsubgroup_def
{
fix \( b_1 \) \( b_2 \)
assume AS: \( \mathfrak{f} (b_1) = \mathfrak{f} (b_2) \), \( b_1\in G//r \), \( b_2\in G//r \)
from G, AS(3) have invb2: \( \text{GroupInv}(G//r,\mathcal{P})(b_2)\in G//r \) using inverse_in_group unfolding group0_def
with G, AS(2) have I: \( \mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle \in G//r \) using group_op_closed unfolding group0_def
then obtain \( g \) where \( g\in G \) and gg: \( \mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle =r\{g\} \) unfolding quotient_def
from \( g\in G \) have \( \langle r\{g\},f(g)\rangle \in \mathfrak{f} \)
with ff_fun, gg have E: \( \mathfrak{f} (\mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle ) = f(g) \) using apply_equality
from ff_fun, invb2 have pp: \( \mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\in f(G) \) using apply_type
from ff_fun, AS(2,3) have fff: \( \mathfrak{f} (b_1) \in f(G) \), \( \mathfrak{f} (b_2) \in f(G) \) using apply_type
from fff(1), pp have EE: \( F\langle \mathfrak{f} (b_1),\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\rangle =\)
\( \text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (b_1),\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\rangle \)
from ff have \( f(G) \subseteq H \) using func1_1_L6(2)
with fff have \( \mathfrak{f} (b_1)\in H \), \( \mathfrak{f} (b_2)\in H \)
with assms(1-4), G, H, HOM, ff_fun, AS(1,3), fff(2), EE have \( \text{ TheNeutralElement}(H,F) = \)
\( \text{restrict}(F,f(G)\times f(G))\langle \mathfrak{f} (b_1),\mathfrak{f} ( \text{GroupInv}(G//r,\mathcal{P})(b_2))\rangle \) using group0_2_L6(1), restrict, image_inv, group0_3_T1, image_group unfolding group0_def
also
from G, H, HOM, AS(2,3), E have \( \ldots = f(g) \) using inverse_in_group unfolding group0_def, IsMorphism_def, Homomor_def
finally have \( \text{ TheNeutralElement}(H,F) = f(g) \)
with ff, \( g\in G \) have \( g\in f^{-1}\{\text{ TheNeutralElement}(H,F)\} \) using func1_1_L15
with assms, \( g\in G \), gg have \( \mathcal{P}\langle b_1, \text{GroupInv}(G//r,\mathcal{P})(b_2)\rangle = \text{ TheNeutralElement}(G//r,\mathcal{P}) \) using Group_ZF_2_4_L5E, kernel_normal_sub unfolding group0_def
with AS(2,3), G have \( b_1=b_2 \) using group0_2_L11A unfolding group0_def
with ff_fun have \( \mathfrak{f} \in \text{inj}(G//r,f(G)) \) unfolding inj_def
moreover {
}
ultimately have \( \mathfrak{f} \in \text{bij}(G//r,fG) \) unfolding bij_def, surj_def using ff_fun
qed
fix \( m \)
assume \( m \in f(G) \)
with ff obtain \( g \) where \( g\in G \), \( m=f(g) \) using func_imagedef
hence \( \langle r\{g\},m\rangle \in \mathfrak{f} \)
with ff_fun have \( \mathfrak{f} (r\{g\})=m \) using apply_equality
with \( g\in G \) have \( \exists A\in G//r.\ \mathfrak{f} (A) = m \) unfolding quotient_def
with HOM show \( thesis \)
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\in \text{bij}(G,H) \), \( \text{IsAgroup}(G,P) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( \text{Homomor}(converse(f),H,F,G,P) \)proof{
}
fix \( h_1 \) \( h_2 \)
assume \( h_1\in H \), \( h_2\in H \)
with assms(1) obtain \( g_1 \) \( g_2 \) where g1: \( g_1\in G \), \( f(g_1)=h_1 \) and g2: \( g_2\in G \), \( f(g_2)=h_2 \) unfolding bij_def, surj_def
with assms(2,3) have \( converse(f)(f(P\langle g_1,g_2\rangle )) = converse(f)(F\langle h_1,h_2\rangle ) \) using homomor_eq
with assms(1,2), g1, g2 have \( P\langle converse(f)(h_1),converse(f)(h_2)\rangle = converse(f)(F\langle h_1,h_2\rangle ) \) using left_inverse, group_op_closed unfolding group0_def, bij_def
with assms(1) show \( thesis \) using bij_converse_bij, bij_is_fun unfolding Homomor_def, IsMorphism_def
qed
A very important homomorphism is given by taking every element to its class in a group quotient. Recall that \(\lambda x\in X. p(x)\) is an alternative notation for function defined as a set of pairs, see lemma lambda_fun_alt in theory func1.thy.
lemma (in group0) quotient_map:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \)
defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \) and \( q \equiv \lambda x\in G.\ \text{QuotientGroupRel}(G,P,H)\{x\} \)
shows \( \text{Homomor}(q,G,P,G//r, \text{QuotientGroupOp}(G,P,H)) \) using groupAssum, assms, group_op_closed, lam_funtype, lamE, EquivClass_1_L10, Group_ZF_2_4_L3, Group_ZF_2_4_L5A, Group_ZF_2_4_T1 unfolding IsAnormalSubgroup_def, QuotientGroupOp_def, Homomor_def, IsMorphism_defIn the context of group0, we may use all results of semigr0.
sublocale group0 < semigroup: semigr0
unfolding semigr0_def using groupAssum, IsAgroup_def, IsAmonoid_def
end
Definition of End:
\( \text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\} \)
lemma (in monoid0) Group_ZF_2_1_L0:
assumes \( F = f \text{ lifted to function space over } X \) and \( s:X\rightarrow G \), \( r:X\rightarrow G \)
shows \( F\langle s,r\rangle : X\rightarrow G \) lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in group0) Group_ZF_2_1_L3:
assumes \( F = P \text{ lifted to function space over } X \) and \( s:X\rightarrow G \), \( r:X\rightarrow G \) and \( x\in X \)
shows \( (F\langle s,r\rangle )(x) = s(x)\cdot r(x) \) lemma (in group0) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) lemma (in group0) endomor_eq:
assumes \( f \in \text{End}(G,P) \), \( g_1\in G \), \( g_2\in G \)
shows \( f(g_1\cdot g_2) = f(g_1)\cdot f(g_2) \) lemma (in group0) group0_4_L8:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1}) \), \( a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d) \), \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \), \( a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1} \), \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \) lemma (in group0) eq_endomor:
assumes \( f:G\rightarrow G \) and \( \forall g_1\in G.\ \forall g_2\in G.\ f(g_1\cdot g_2)=f(g_1)\cdot f(g_2) \)
shows \( f \in \text{End}(G,P) \) lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
lemma (in monoid0) group0_1_L3B: shows \( \text{range}(f) = G \)
theorem func_ZF_1_L4:
assumes \( f : Y\times Y\rightarrow Y \) and \( F = f \text{ lifted to function space over } X \) and \( s:X\rightarrow \text{range}(f) \), \( r:X\rightarrow \text{range}(f) \) and \( x\in X \)
shows \( (F\langle s,r\rangle )(x) = f\langle s(x),r(x)\rangle \) lemma (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\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} \)Definition of IsCommutative:
\( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
theorem group0_2_T2:
assumes \( \text{IsAgroup}(G,f) \)
shows \( \text{GroupInv}(G,f) : G\rightarrow G \)Definition of Homomor:
\( \text{Homomor}(f,G,P,H,F) \equiv f:G\rightarrow H \wedge \text{IsMorphism}(G,P,F,f) \)
Definition of IsMorphism:
\( \text{IsMorphism}(G,P,F,f) \equiv \forall g_1\in G.\ \forall g_2\in G.\ f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle \)
theorem (in group0) end_comp_monoid: shows \( \text{IsAmonoid}( \text{End}(G,P),\text{InEnd}( \text{Composition}(G),G,P)) \) and \( \text{ TheNeutralElement}( \text{End}(G,P),\text{InEnd}( \text{Composition}(G),G,P)) = id(G) \)
lemma (in monoid0) group0_1_L3A: shows \( G\neq 0 \)
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 \)
theorem (in abelian_group) end_pointwise_addition:
assumes \( f\in \text{End}(G,P) \), \( g\in \text{End}(G,P) \)
defines \( F \equiv P \text{ lifted to function space over } G \)
shows \( F\langle f,g\rangle \in \text{End}(G,P) \) lemma (in monoid0) group0_1_L1:
assumes \( a\in G \), \( b\in G \)
shows \( a\oplus b \in G \) lemma (in group0) end_composition:
assumes \( f_1\in \text{End}(G,P) \), \( f_2\in \text{End}(G,P) \)
shows \( \text{Composition}(G)\langle f_1,f_2\rangle \in \text{End}(G,P) \) lemma (in abelian_group) end_inverse_group: shows \( \text{GroupInv}(G,P) \in \text{End}(G,P) \)
lemma func_ZF_5_L2:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \)
shows \( \text{Composition}(X)\langle f,g\rangle = f\circ g \) lemma (in group0) Group_ZF_2_1_L6:
assumes \( F = P \text{ lifted to function space over } X \)
shows \( \forall s\in (X\rightarrow G).\ \text{GroupInv}(X\rightarrow G,F)(s) = \text{GroupInv}(G,P)\circ s \) 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) \) theorem (in group0) Group_ZF_2_1_T2:
assumes \( F = P \text{ lifted to function space over } X \)
shows \( \text{IsAgroup}(X\rightarrow G,F) \)Definition of IsAsubgroup:
\( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H)) \)
lemma (in group0) Group_ZF_2_1_L7:
assumes \( F = P \text{ lifted to function space over } X \) and \( P \text{ is commutative on } G \)
shows \( F \text{ is commutative on } (X\rightarrow G) \) theorem (in abelian_group) end_addition_group:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsAgroup}( \text{End}(G,P),\text{InEnd}(F,G,P)) \) and \( \text{InEnd}(F,G,P) \text{ is commutative on } \text{End}(G,P) \) lemma (in abelian_group) end_addition_subgroup: shows \( \text{IsAsubgroup}( \text{End}(G,P),P \text{ lifted to function space over } G) \)
lemma (in group0) lift_group_subgr_neut:
assumes \( F = P \text{ lifted to function space over } X \) and \( \text{IsAsubgroup}(H,F) \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(F,H\times H)) = \text{ConstantFunction}(X,1 ) \) lemma homomor_eq:
assumes \( \text{Homomor}(f,G,P,H,F) \), \( g_1\in G \), \( g_2\in G \)
shows \( f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle \) lemma func_eq:
assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)
shows \( f = g \) lemma (in group0) end_composition:
assumes \( f_1\in \text{End}(G,P) \), \( f_2\in \text{End}(G,P) \)
shows \( \text{Composition}(G)\langle f_1,f_2\rangle \in \text{End}(G,P) \)Definition of IsDistributive:
\( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \)
\( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
lemma (in abelian_group) distributive_comp_pointwise:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsDistributive}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P)) \)Definition of IsAring:
\( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \)
\( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)
theorem (in abelian_group) end_is_ring:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsAring}( \text{End}(G,P),\text{InEnd}(F,G,P),\text{InEnd}( \text{Composition}(G),G,P)) \) 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_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) 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 (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_2_L9:
assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)
shows \( a = b^{-1} \) and \( b = a^{-1} \) lemma image_neutral:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( f(\text{ TheNeutralElement}(G,P)) = \text{ TheNeutralElement}(H,F) \) lemma (in group0) group0_3_L5:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( 1 \in H \) lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma func1_1_L3:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(D) \subseteq X \) lemma (in group0) group0_3_L6:
assumes \( \text{IsAsubgroup}(H,P) \) and \( a\in H \), \( b\in H \)
shows \( a\cdot b \in H \) theorem (in group0) group0_3_T3A:
assumes \( \text{IsAsubgroup}(H,P) \) and \( h\in H \)
shows \( h^{-1}\in H \) lemma image_inv:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( g\in G \)
shows \( f( \text{GroupInv}(G,P)(g)) = \text{GroupInv}(H,F)(f(g)) \) lemma (in group0) group0_3_L2:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( H \subseteq G \)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 preimage_sub:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( \text{IsAsubgroup}(K,F) \)
shows \( \text{IsAsubgroup}(f^{-1}(K),P) \) 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 \) 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) \) theorem preimage_normal_subgroup:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( \text{IsAnormalSubgroup}(H,F,K) \)
shows \( \text{IsAnormalSubgroup}(G,P,f^{-1}(K)) \) corollary (in group0) trivial_normal_subgroup: shows \( \text{IsAnormalSubgroup}(G,P,\{1 \}) \)
lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma restrict_domain:
assumes \( f:X\rightarrow Y \)
shows \( \text{restrict}(f,X) = f \) theorem image_subgroup:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( f:G\rightarrow H \), \( \text{IsAsubgroup}(K,P) \)
shows \( \text{IsAsubgroup}(fK,F) \) lemma (in group0) Group_ZF_2_4_L3:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{equiv}(G, \text{QuotientGroupRel}(G,P,H)) \) corollary kernel_normal_sub:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( \text{IsAnormalSubgroup}(G,P,f^{-1}\{\text{ TheNeutralElement}(H,F)\}) \) lemma same_image_equiv:
assumes \( \text{equiv}(A,r) \), \( y\in A \), \( r\{x\} = r\{y\} \)
shows \( \langle x,y\rangle \in r \)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_2_L11A:
assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} = 1 \)
shows \( a=b \) lemma Group_ZF_2_4_L5A:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \)
shows \( \text{Congruent2}( \text{QuotientGroupRel}(G,P,H),P) \) lemma (in group0) Group_ZF_2_2_L2:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,P) \) and \( F = \text{ProjFun2}(G,r,P) \) and \( a\in G \), \( b\in G \)
shows \( F\langle r\{a\},r\{b\}\rangle = r\{a\cdot b\} \)Definition of QuotientGroupOp:
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
theorem Group_ZF_2_4_T1:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \)
shows \( \text{IsAgroup}(G// \text{QuotientGroupRel}(G,P,H), \text{QuotientGroupOp}(G,P,H)) \) corollary image_group:
assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)
shows \( \text{IsAsubgroup}(f(G),F) \) lemma func1_1_L6:
assumes \( f:X\rightarrow Y \)
shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \) lemma (in group0) group0_2_L6:
assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \) theorem (in group0) group0_3_T1:
assumes \( \text{IsAsubgroup}(H,P) \) and \( g = \text{restrict}(P,H\times H) \)
shows \( \text{GroupInv}(H,g) = \text{restrict}( \text{GroupInv}(G,P),H) \) lemma (in group0) Group_ZF_2_4_L5E:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \) and \( a\in G \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e \)
shows \( r\{a\} = e \longleftrightarrow a\in H \) lemma EquivClass_1_L10:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( x\in A \), \( y\in A \)
shows \( \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\rangle \} \)Definition of IsAgroup:
\( \text{IsAgroup}(G,f) \equiv \)
\( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)
Definition of IsAmonoid:
\( \text{IsAmonoid}(G,f) \equiv \)
\( f \text{ is associative on } G \wedge \)
\( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8