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
In 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 \emptyset \) 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)) \)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 Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
