begin
In this theory we study group homomorphisms.
Homomorphisms
A homomorphism is a function between groups that preserves the group operations.
In general we may have a homomorphism not only between groups, but also between various algebraic structures with one operation like magmas, semigroups, quasigroups, loops and monoids. In all cases the homomorphism is defined by using the morphism property. In the multiplicative notation we we will write that \(f\) has a morphism property if \(f(x\cdot_G y) = f(x)\cdot_H f(y)\) for all \(x,y\in G\). Below we write this definition in raw set theory notation and use the expression IsMorphism instead of the possible, but longer HasMorphismProperty.
definition
\( \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 \)
A function \(f:G\rightarrow H\) between algebraic structures \((G,\cdot_G)\) and \((H,\cdot_H)\) with one operation (each) is a homomorphism if it has the morphism property.
definition
\( \text{Homomor}(f,G,P,H,F) \equiv f:G\rightarrow H \wedge \text{IsMorphism}(G,P,F,f) \)
Now a lemma about the definition:
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 \) using assms unfolding Homomor_def, IsMorphism_defAn endomorphism is a homomorphism from a group to the same group. We define \( \text{End}(G,P) \) as the set of endomorphisms for a given group. As we show later when the group is abelian, the set of endomorphisms with pointwise adddition and composition as multiplication forms a ring.
definition
\( \text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\} \)
The defining property of an endomorphism written in notation used in group0 context:
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) \) using assms, homomor_eq unfolding End_defA function that maps a group \(G\) into itself and satisfies \(f(g_1\cdot g2) = f(g_1)\cdot f(g_2)\) is an endomorphism.
lemma (in group0) eq_endomor:
assumes \( f:G\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) \) using assms unfolding End_def, Homomor_def, IsMorphism_defThe set of endomorphisms forms a submonoid of the monoid of function from a set to that set under composition.
lemma (in group0) end_composition:
assumes \( f_1\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) \)proof from assms have fun: \( f_1:G\rightarrow G \), \( f_2:G\rightarrow G \) unfolding End_def
then have \( f_1\circ f_2:G\rightarrow G \) using comp_fun
from assms, fun(2) have \( \forall g_1\in G.\ \forall g_2\in G.\ (f_1\circ f_2)(g_1\cdot g_2) = ((f_1\circ f_2)(g_1))\cdot ((f_1\circ f_2)(g_2)) \) using group_op_closed, comp_fun_apply, endomor_eq, apply_type
with fun, \( f_1\circ f_2:G\rightarrow G \) show \( thesis \) using eq_endomor, func_ZF_5_L2
qed
We will use some binary operations that are naturally defined on the function space \(G\rightarrow G\), but we consider them restricted to the endomorphisms of \(G\). To shorten the notation in such case we define an abbreviation \( \text{InEnd}(F,G,P) \) which restricts a binary operation \(F\) to the set of endomorphisms of \(G\).
abbreviation
\( \text{InEnd}(F,G,P) \equiv \text{restrict}(F, \text{End}(G,P)\times \text{End}(G,P)) \)
Endomoprhisms of a group form a monoid with composition as the binary operation, and the identity map as the neutral element.
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) \)proof let \( C_0 = \text{InEnd}( \text{Composition}(G),G,P) \)
have fun: \( id(G):G\rightarrow G \) unfolding id_def
{
fix \( g \) \( h \)
assume \( g\in G \), \( h\in G \)
then have \( id(G)(g\cdot h)=(id(G)g)\cdot (id(G)h) \) using group_op_closed
with groupAssum, fun have \( id(G) \in \text{End}(G,P) \) using eq_endomor
moreover
have A0: \( id(G)=\text{ TheNeutralElement}(G \rightarrow G, \text{Composition}(G)) \) using Group_ZF_2_5_L2(2)
ultimately have A1: \( \text{ TheNeutralElement}(G \rightarrow G, \text{Composition}(G)) \in \text{End}(G,P) \)
moreover
have A2: \( \text{End}(G,P) \subseteq G\rightarrow G \) unfolding End_def
moreover have A3: \( \text{End}(G,P) \text{ is closed under } \text{Composition}(G) \) using end_composition unfolding IsOpClosed_def
ultimately show \( \text{IsAmonoid}( \text{End}(G,P),C_0) \) using group0_1_T1, Group_ZF_2_5_L2(1) unfolding monoid0_def
have \( \text{IsAmonoid}(G\rightarrow G, \text{Composition}(G)) \) using Group_ZF_2_5_L2(1)
with A0, A1, A2, A3 show \( \text{ TheNeutralElement}( \text{End}(G,P),C_0) = id(G) \) using group0_1_L6
qed
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 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 \)
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 \)Definition of End:
\( \text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\} \)
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) 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 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 Group_ZF_2_5_L2: shows \( \text{IsAmonoid}(X\rightarrow X, \text{Composition}(X)) \), \( id(X) = \text{ TheNeutralElement}(X\rightarrow X, \text{Composition}(X)) \)
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 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 monoid0) group0_1_T1:
assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \) lemma Group_ZF_2_5_L2: shows \( \text{IsAmonoid}(X\rightarrow X, \text{Composition}(X)) \), \( id(X) = \text{ TheNeutralElement}(X\rightarrow X, \text{Composition}(X)) \)
lemma group0_1_L6:
assumes \( \text{IsAmonoid}(G,f) \) and \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) = \text{ TheNeutralElement}(G,f) \) 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) 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) 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 \) 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 \)
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 (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 func_eq:
assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)
shows \( f = g \)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