IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory IntModule_ZF imports Module_ZF IntGroup_ZF

begin

In this section we show that the integers, as a ring, have only one module structure on each abelian group. We will show that the module structure is unique, but we will also show which action is the one that defines that module structure.

Integer powers as the only integer actions on abelian groups

As we show in theorem powz_maps_int_End in the IntGroup theory the mapping $\mathbb{Z}\ni n\mapsto (G\ni x\mapsto x^n)$ maps integers to endomorphisms of the abelian group $G$. We will show here that this mapping is the unique action of integers on that group.

When $\mathbb{Z}$ acts on a group, that action is unique.

lemma (in int0) action_unique:

assumes $ \text{IsLeftModule}(int,IntegerAddition,IntegerMultiplication,G,f,S_1) $ and $ \text{IsLeftModule}(int,IntegerAddition,IntegerMultiplication,G,f,S_2) $

shows $ S_1 = S_2 $proof

let $ A_Z = IntegerAddition $

let $ M_Z = IntegerMultiplication $

from assms have mod0: $ module0(\mathbb{Z} ,A_Z,M_Z,G,f,S_1) $, $ module0(\mathbb{Z} ,A_Z,M_Z,G,f,S_2) $ unfolding module0_def, IsLeftModule_def, ring0_def, module0_axioms_def

{

fix $ r $

assume rg: $ r\in \mathbb{Z} $

from mod0(1) have eq: $ \forall g\in G.\ (S_1( 0 ))(g) = \text{ TheNeutralElement}(G, f) $ using mult_zero

with mod0(1) have $ S_1( 0 ) = \{\langle g,\text{ TheNeutralElement}(G,f)\rangle .\ g\in G\} $ using Int_ZF_1_L8A(1), H_val_type(2), fun_is_set_of_pairs

then have s1: $ S_1( 0 ) = \text{ConstantFunction}(G,\text{ TheNeutralElement}(G, f)) $ unfolding ConstantFunction_def

from mod0(2) have eq: $ \forall g\in G.\ (S_2( 0 ))(g) = \text{ TheNeutralElement}(G, f) $ using mult_zero

with mod0(2) have $ (S_2( 0 )):G\rightarrow G $ using Int_ZF_1_L8A(1), H_val_type

with eq, s1 have $ S_1( 0 ) = S_2( 0 ) $ unfolding ConstantFunction_def using fun_is_set_of_pairs

{

assume $ r\leq 0 $

then have $ r\in \mathbb{Z} $ using OrderedGroup_ZF_1_L4(1)

have $ S_1(r) = S_2(r) $proof

{

fix $ n $

assume $ n\leq 0 $, $ S_1(n) = S_2(n) $

from $ n\leq 0 $ have $ n\in \mathbb{Z} $ using OrderedGroup_ZF_1_L4(1)

have $ ( - 1 ) \in \mathbb{Z} $ using inverse_in_group, Int_ZF_1_T2(3), Ring_ZF_1_L2(2), Int_ZF_1_1_L2(3)

{

fix $ t $

assume t: $ t\in G $

with mod0(1), $ S_1(n) = S_2(n) $, $ n\in \mathbb{Z} $, $ ( - 1 )\in \mathbb{Z} $ have $ S_1(n + ( - 1 ))(t) = (f\langle (S_2(n))(t),(S_1( - 1 ))(t)\rangle ) $ using module_ax2, t

moreover

from mod0(1) have ex: $ \forall g\in G.\ S_1( - 1 )(g) = \text{GroupInv}(G, f)(g) $ using inv_module, apply_type, H_val_type(2), Ring_ZF_1_L2(2), Int_ZF_1_1_L2(3), module_ax4

moreover

from mod0(1) have $ S_1( - 1 ):G\rightarrow G $ using H_val_type(2), Ring_ZF_1_L2(2), Int_ZF_1_1_L2(3), Ring_ZF_1_L3(1), Int_ZF_1_1_L2(3)

moreover

from assms(1) have $ \text{GroupInv}(G, f): G\rightarrow G $ using group0_2_T2 unfolding IsLeftModule_def

with ex, $ S_1( - 1 ):G\rightarrow G $ have $ S_1( - 1 ) = \text{GroupInv}(G, f) $ using func_eq

ultimately have A: $ S_1(n + ( - 1 ))(t) = f\langle (S_2(n))(t), \text{GroupInv}(G, f) t\rangle $

from assms(2), $ ( - 1 ) \in \mathbb{Z} $, $ n\in \mathbb{Z} $, mod0(2), t, $ S_1(n) = S_2(n) $ have $ (S_2(n + - 1 ))(t) = f\langle (S_2(n))(t),(S_2( - 1 ))(t)\rangle $ using module_ax2

moreover

from mod0(2) have ex: $ \forall g\in G.\ (S_2( - 1 ))(g) = \text{GroupInv}(G, f)(g) $ using inv_module, apply_type, H_val_type(2), Ring_ZF_1_L2(2), Int_ZF_1_1_L2(3), module_ax4

moreover

from mod0(2) have $ S_2( - 1 ): G\rightarrow G $ using H_val_type(2), Ring_ZF_1_L2(2), Int_ZF_1_1_L2(3), Ring_ZF_1_L3(1), Int_ZF_1_1_L2(3)

with ex, $ \text{GroupInv}(G, f): G\rightarrow G $ have $ S_2( - 1 ) = \text{GroupInv}(G, f) $ using func_eq

ultimately have $ S_2(n + ( - 1 ))(t) = f\langle (S_2(n))(t), \text{GroupInv}(G, f)(t)\rangle $

with A have $ (S_1(n + ( - 1 )))(t) = S_2(n + ( - 1 ))(t) $

}

hence $ \forall t\in G.\ S_1(n + - 1 )(t) = S_2(n + ( - 1 ))(t) $

moreover

from mod0, $ ( - 1 ) \in \mathbb{Z} $, $ n\in \mathbb{Z} $ have $ S_1(n + ( - 1 )):G\rightarrow G $ and $ S_2(n + ( - 1 )):G\rightarrow G $ using group_op_closed, Int_ZF_1_T2(3), H_val_type(2)

ultimately have $ S_1(n + ( - 1 )) = S_2(n + ( - 1 )) $ using func_eq

}

hence $ \forall n.\ (n\leq 0 ) \wedge (S_1(n) = S_2(n))\longrightarrow S_1(n - 1 ) = S_2(n - 1 ) $

with $ r\leq 0 $, $ S_1( 0 ) = S_2( 0 ) $ show $ S_1(r) = S_2(r) $ using Back_induct_on_int

qed

}

moreover {

assume $ 0 \leq r $

then have $ r\in \mathbb{Z} $ using OrderedGroup_ZF_1_L4(2)

have $ S_1(r) = S_2(r) $proof

{

fix $ m $

assume $ 0 \leq m $, $ S_1(m) = S_2(m) $

from $ 0 \leq m $ have $ m\in \mathbb{Z} $ using OrderedGroup_ZF_1_L4(2)

have $ 1 \in \mathbb{Z} $ using Int_ZF_1_L8A(2)

{

fix $ t $

assume $ t\in G $

with assms(1), $ m\in \mathbb{Z} $, $ 1 \in \mathbb{Z} $, mod0(1), $ S_1(m) = S_2(m) $ have $ S_1(m + 1 )t = f\langle (S_2(m))(t),t\rangle $ using module_ax2, module_ax4

moreover

from mod0(2), $ m\in \mathbb{Z} $, $ 1 \in \mathbb{Z} $, $ t\in G $ have $ (S_2(m + 1 ))(t) = f\langle (S_2(m))(t),t\rangle $ using module_ax2, module_ax4

ultimately have $ (S_1(m + 1 ))(t) = (S_2(m + 1 ))(t) $

}

hence $ \forall t\in G.\ (S_1(m + 1 ))(t) = (S_2(m + 1 ))(t) $

moreover

from mod0, $ 1 \in \mathbb{Z} $, $ m\in \mathbb{Z} $ have $ S_1(m + 1 ):G\rightarrow G $ and $ S_2(m + 1 ):G\rightarrow G $ using group_op_closed, Int_ZF_1_T2(3), H_val_type(2), H_val_type(2)

ultimately have $ S_1(m + 1 ) = S_2(m + 1 ) $ using func_eq

}

hence $ \forall m.\ ( 0 \leq m) \wedge S_1(m) = S_2(m) \longrightarrow S_1(m + 1 ) = S_2(m + 1 ) $

with $ 0 \leq r $, $ S_1( 0 ) = S_2( 0 ) $ show $ S_1(r) = S_2(r) $ using Induction_on_int

qed

} moreover

have $ IntegerOrder \text{ is total on } \mathbb{Z} $ using Int_ZF_2_T1(2)

ultimately have $ S_1(r) = S_2(r) $ unfolding IsTotal_def using rg, Int_ZF_1_L8(1), Ring_ZF_1_L2(1), Int_ZF_1_1_L2(3)

}

hence $ \forall r\in \mathbb{Z} .\ S_1(r) = S_2(r) $

moreover

from assms have $ S_1:\mathbb{Z} \rightarrow \text{End}(G,f) $, $ S_2:\mathbb{Z} \rightarrow \text{End}(G,f) $ using module_action_type(3)

ultimately show $ S_1 = S_2 $ using func_eq

qed

We can use theorems proven in the abelian_group locale in the abgroup_int0 locale.

sublocale abgroup_int0 < abgroup: abelian_group

proof

from isAbelian show $ P \text{ is commutative on } G $

qed

The rest of the propositions in this section concern the mapping $\mathbb{Z}\ni n\mapsto (G\ni x\mapsto x^n)$. To simplify the statements and proofs we will denote this mapping as $\mathcal{S}$.

locale abgroup_int1 = abgroup_int0 +

defines $ \mathcal{S} \equiv \{\langle z,\{\langle x,x^{z}\rangle .\ x\in G\}\rangle .\ z\in \mathbb{Z} \} $

The mapping $\mathcal{S}$ is a group homomorphism between $(\mathbb{Z},+)$ and $(G,P)$

lemma (in abgroup_int1) group_action_int_add_morphism:

assumes $ r\in \mathbb{Z} $, $ s\in \mathbb{Z} $, $ g\in G $

shows $ (\mathcal{S} (r + s))(g) = ((\mathcal{S} (r))(g))\cdot ((\mathcal{S} (s))(g)) $ using assms, int_sum_type, ZF_fun_from_tot_val1, powz_hom_prop

Same as in lemma group_action_int_add_morphism above, but not pointwise:

lemma (in abgroup_int1) group_action_int_add_morphism_fun:

assumes $ r\in \mathbb{Z} $, $ s\in \mathbb{Z} $

shows $ \mathcal{S} (r + s) = \text{EndAdd}(G,P)\langle \mathcal{S} (r),\mathcal{S} (s)\rangle $proof

let $ F = \text{EndAdd}(G,P)\langle \mathcal{S} (r),\mathcal{S} (s)\rangle $

from assms have $ \mathcal{S} (r) \in \text{End}(G,P) $, $ \mathcal{S} (s) \in \text{End}(G,P) $, $ \mathcal{S} (r + s) \in \text{End}(G,P) $ using powz_maps_int_End, int_sum_type, apply_funtype

have $ \text{EndAdd}(G,P): \text{End}(G,P)\times \text{End}(G,P)\rightarrow \text{End}(G,P) $ using end_addition_group unfolding EndAdd_def, IsAgroup_def, IsAmonoid_def, IsAssociative_def

with $ \mathcal{S} (r) \in \text{End}(G,P) $, $ \mathcal{S} (s) \in \text{End}(G,P) $ have $ F:G\rightarrow G $ using apply_funtype unfolding End_def

moreover

from $ \mathcal{S} (r + s) \in \text{End}(G,P) $ have $ \mathcal{S} (r + s):G\rightarrow G $ unfolding End_def

moreover

from assms, $ \mathcal{S} (r) \in \text{End}(G,P) $, $ \mathcal{S} (s) \in \text{End}(G,P) $ have $ \forall g\in G.\ (\mathcal{S} (r + s))(g) = F(g) $ using group_action_int_add_morphism, end_pointwise_add_val unfolding EndAdd_def

ultimately show $ \mathcal{S} (r + s) = F $ using func_eq

qed

The mapping $\mathcal{S}$ is a homomorphism between $(\mathbb{Z},\cdot)$ and $(G\to G, \circ)$

lemma (in abgroup_int1) group_action_int_mult_morphism:

assumes $ r\in \mathbb{Z} $, $ s\in \mathbb{Z} $

shows $ \mathcal{S} (r\cdot _Zs) = \text{EndMult}(G,P)\langle \mathcal{S} (r),\mathcal{S} (s)\rangle $proof

from assms have $ \mathcal{S} (r) \in \text{End}(G,P) $, $ \mathcal{S} (s) \in \text{End}(G,P) $, $ \mathcal{S} (r\cdot _Zs) \in \text{End}(G,P) $ using powz_maps_int_End, int_prod_type, apply_funtype

from assms have I: $ \mathcal{S} (r\cdot _Zs) = \{\langle x,x^{s\cdot _Zr}\rangle .\ x\in G\} $, $ \mathcal{S} (r) = \{\langle x,x^{r}\rangle .\ x\in G\} $, $ \mathcal{S} (s) = \{\langle x,x^{s}\rangle .\ x\in G\} $ using int_prod_type, ZF_fun_from_tot_val1, Int_ZF_1_L4(2)

from assms(1,2) have $ \{\langle x,x^{s\cdot _Zr}\rangle .\ x\in G\} = \{\langle x,(x^{s})^{r}\rangle .\ x\in G\} $ using powz_mult

with assms(1,2), I have $ \mathcal{S} (r\cdot _Zs) = \mathcal{S} (r)\circ \mathcal{S} (s) $ using powz_type, comp_fun_expr

with $ \mathcal{S} (r) \in \text{End}(G,P) $, $ \mathcal{S} (s) \in \text{End}(G,P) $ show $ thesis $ unfolding EndMult_def using inend_composition_val

qed

The action maps the integer $1$ to the identity, i.e. the neutral element of the composition of endomorphisms (which is the multiplication operation of the ring of endomorphisms of the group).

lemma (in abgroup_int1) group_action_int_unit:

shows $ \mathcal{S} (1 _Z) = \text{ TheNeutralElement}( \text{End}(G,P), \text{EndMult}(G,P)) $proof

have $ \text{ TheNeutralElement}( \text{End}(G,P), \text{EndMult}(G,P)) = id(G) $ using end_comp_monoid(2) unfolding EndMult_def

then show $ thesis $ using Int_ZF_1_L8A(2), ZF_fun_from_tot_val1, int_power_zero_one(2), id_diagonal

qed

The function from integers to endomorphisms of $G$ defined by $z\mapsto (x\mapsto x^z)$ is a module.

theorem (in abgroup_int1) group_action_int:

shows $ \text{IsLeftModule}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,G,P,\mathcal{S} ) $ using groupAssum, isAbelian, Int_ZF_1_1_L2, powz_maps_int_End, group_action_int_add_morphism_fun, group_action_int_mult_morphism, group_action_int_unit unfolding IsMorphism_def, ringHomomor_def, IsAction_def, IsLeftModule_def

If there is a $\mathbb{Z}$-module on an abelian group, it is the one found in the previous result.

theorem (in abgroup_int1) group_action_int_rev0:

assumes $ \text{IsLeftModule}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,G,P,S) $

shows $ S=\mathcal{S} $ using assms, group_action_int, action_unique

end

Definition of IsLeftModule: $ \text{IsLeftModule}(S,A,M,\mathcal{M} ,A_M,H) \equiv $ $ \text{IsAring}(S,A,M) \wedge \text{IsAgroup}(\mathcal{M} ,A_M) \wedge (A_M \text{ is commutative on } \mathcal{M} ) \wedge \text{IsAction}(S,A,M,\mathcal{M} ,A_M,H) $

lemma (in module0) mult_zero:

assumes $ g\in \mathcal{M} $

shows $ 0 \cdot _Sg = \Theta $

lemma (in int0) Int_ZF_1_L8A: shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $

lemma (in module0) H_val_type:

assumes $ r\in R $

shows $ H(r) \in \text{End}(\mathcal{M} ,A_M) $ and $ H(r):\mathcal{M} \rightarrow \mathcal{M} $

theorem fun_is_set_of_pairs:

assumes $ f:X\rightarrow Y $

shows $ f = \{\langle x,f(x)\rangle .\ x \in X\} $

Definition of ConstantFunction: $ \text{ConstantFunction}(X,c) \equiv X\times \{c\} $

lemma (in module0) H_val_type:

assumes $ r\in R $

shows $ H(r) \in \text{End}(\mathcal{M} ,A_M) $ and $ H(r):\mathcal{M} \rightarrow \mathcal{M} $

lemma (in group3) OrderedGroup_ZF_1_L4:

assumes $ a\leq b $

shows $ a\in G $, $ b\in G $

lemma (in group0) inverse_in_group:

assumes $ x\in G $

shows $ x^{-1}\in G $

theorem Int_ZF_1_T2: shows $ \text{IsAgroup}(int,IntegerAddition) $, $ IntegerAddition \text{ is commutative on } int $, $ group0(int,IntegerAddition) $

lemma (in ring0) Ring_ZF_1_L2: shows $ 0 \in R $, $ 1 \in R $, $ ( - 0 ) = 0 $, $ 2 \in R $

lemma (in int0) Int_ZF_1_1_L2: shows $ \text{IsAring}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) $, $ IntegerMultiplication \text{ is commutative on } \mathbb{Z} $, $ ring0(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) $

lemma (in module0) module_ax2:

assumes $ r\in R $, $ s\in R $, $ x\in \mathcal{M} $

shows $ (r + s)\cdot _Sx = r\cdot _Sx +_V s\cdot _Sx $

lemma (in module0) inv_module:

assumes $ g\in \mathcal{M} $

shows $ ( - 1 )\cdot _Sg = - g $

lemma (in module0) module_ax4:

assumes $ x\in \mathcal{M} $

shows $ 1 \cdot _Sx = x $

lemma (in ring0) Ring_ZF_1_L3:

assumes $ a\in R $

shows $ ( - a) \in R $, $ ( - ( - a)) = a $, $ a + 0 = a $, $ 0 + a = a $, $ a\cdot 1 = a $, $ 1 \cdot a = a $, $ a - a = 0 $, $ a - 0 = a $, $ 2 \cdot a = a + a $, $ ( - a) + a = 0 $

theorem group0_2_T2:

assumes $ \text{IsAgroup}(G,f) $

shows $ \text{GroupInv}(G,f) : G\rightarrow G $

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) group_op_closed:

assumes $ a\in G $, $ b\in G $

shows $ a\cdot b \in G $

theorem (in int0) Back_induct_on_int:

assumes $ k\leq i $ and $ P(i) $ and $ \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n - 1 ) $

shows $ P(k) $

lemma (in group3) OrderedGroup_ZF_1_L4:

assumes $ a\leq b $

shows $ a\in G $, $ b\in G $

lemma (in int0) Int_ZF_1_L8A: shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $

theorem (in int0) Induction_on_int:

assumes $ i\leq k $ and $ Q(i) $ and $ \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m + 1 ) $

shows $ Q(k) $

theorem (in int0) Int_ZF_2_T1: shows $ \text{IsAnOrdGroup}(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ IntegerOrder \text{ is total on } \mathbb{Z} $, $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) $

Definition of IsTotal: $ r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) $

lemma (in int0) Int_ZF_1_L8: shows $ (\$\!\#\! 0) = 0 $, $ (\$\!\#\! 1) = 1 $

lemma (in ring0) Ring_ZF_1_L2: shows $ 0 \in R $, $ 1 \in R $, $ ( - 0 ) = 0 $, $ 2 \in R $

lemma module_action_type:

assumes $ \text{IsLeftModule}(S,A,M,\mathcal{M} ,A_M,H) $

shows $ \text{IsAction}(S,A,M,\mathcal{M} ,A_M,H) $, $ \text{ringHomomor}(H,S,A,M, \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M), \text{EndMult}(\mathcal{M} ,A_M)) $, $ H:S\rightarrow \text{End}(\mathcal{M} ,A_M) $

lemma (in int0) int_sum_type:

assumes $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

shows $ m + n \in \mathbb{Z} $

lemma ZF_fun_from_tot_val1:

assumes $ x\in X $

shows $ \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) $

theorem (in group_int0) powz_hom_prop:

assumes $ z_1\in \mathbb{Z} $, $ z_2\in \mathbb{Z} $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

theorem (in abgroup_int0) powz_maps_int_End: shows $ \{\langle n,\{\langle x,x^{n}\rangle .\ x\in G\}\rangle .\ n\in \mathbb{Z} \} : \mathbb{Z} \rightarrow \text{End}(G,P) $

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) $

Definition of EndAdd: $ \text{EndAdd}(\mathcal{M} ,A) \equiv \text{InEnd}(A \text{ lifted to function space over } \mathcal{M} ,\mathcal{M} ,A) $

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)))) $

Definition of IsAssociative: $ P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge $ $ (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ $ $ ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) $

Definition of End: $ \text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\} $

lemma (in abgroup_int1) group_action_int_add_morphism:

assumes $ r\in \mathbb{Z} $, $ s\in \mathbb{Z} $, $ g\in G $

shows $ (\mathcal{S} (r + s))(g) = ((\mathcal{S} (r))(g))\cdot ((\mathcal{S} (s))(g)) $

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)) $

lemma (in int0) int_prod_type:

assumes $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

shows $ m\cdot n \in \mathbb{Z} $

lemma (in int0) Int_ZF_1_L4:

assumes $ x\in \mathbb{Z} $, $ y\in \mathbb{Z} $

shows $ x + y = y + x $, $ x\cdot y = y\cdot x $

lemma (in group_int0) powz_mult:

assumes $ z_1\in \mathbb{Z} $, $ z_2\in \mathbb{Z} $, $ x\in G $

shows $ x^{z_1\cdot _Zz_2} = (x^{z_1})^{z_2} $

lemma (in group_int0) powz_type:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z} \in G $

lemma comp_fun_expr:

assumes $ \forall x\in X.\ a(x)\in Y $, $ \forall y\in Y.\ b(y)\in Z $

shows $ \{\langle y,b(y)\rangle .\ y\in Y\}\circ \{\langle x,a(x)\rangle .\ x\in X\} = \{\langle x,b(a(x))\rangle .\ x\in X\} $

Definition of EndMult: $ \text{EndMult}(\mathcal{M} ,A) \equiv \text{InEnd}( \text{Composition}(\mathcal{M} ),\mathcal{M} ,A) $

lemma (in group0) inend_composition_val:

assumes $ f\in \text{End}(G,P) $, $ g\in \text{End}(G,P) $

shows $ \text{InEnd}( \text{Composition}(G),G,P)\langle f,g\rangle = (f\circ 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 group_int0) int_power_zero_one:

assumes $ x\in G $

shows $ x^{ 0 } = 1 $ and $ x^{1 _Z} = x $

lemma id_diagonal: shows $ id(X) = \{\langle x,x\rangle .\ x\in X\} $

lemma (in abgroup_int1) group_action_int_add_morphism_fun:

assumes $ r\in \mathbb{Z} $, $ s\in \mathbb{Z} $

shows $ \mathcal{S} (r + s) = \text{EndAdd}(G,P)\langle \mathcal{S} (r),\mathcal{S} (s)\rangle $

lemma (in abgroup_int1) group_action_int_mult_morphism:

assumes $ r\in \mathbb{Z} $, $ s\in \mathbb{Z} $

shows $ \mathcal{S} (r\cdot _Zs) = \text{EndMult}(G,P)\langle \mathcal{S} (r),\mathcal{S} (s)\rangle $

lemma (in abgroup_int1) group_action_int_unit: shows $ \mathcal{S} (1 _Z) = \text{ TheNeutralElement}( \text{End}(G,P), \text{EndMult}(G,P)) $

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 $

Definition of ringHomomor: $ \text{ringHomomor}(f,R,A,M,S,U,V) \equiv f:R\rightarrow S \wedge \text{IsMorphism}(R,A,U,f) \wedge \text{IsMorphism}(R,M,V,f) $ $ \wedge f(\text{ TheNeutralElement}(R,M)) = \text{ TheNeutralElement}(S,V) $

Definition of IsAction: $ \text{IsAction}(S,A,M,\mathcal{M} ,A_M,H) \equiv \text{ringHomomor}(H,S,A,M, \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M), \text{EndMult}(\mathcal{M} ,A_M)) $

theorem (in abgroup_int1) group_action_int: shows $ \text{IsLeftModule}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,G,P,\mathcal{S} ) $

lemma (in int0) action_unique:

assumes $ \text{IsLeftModule}(int,IntegerAddition,IntegerMultiplication,G,f,S_1) $ and $ \text{IsLeftModule}(int,IntegerAddition,IntegerMultiplication,G,f,S_2) $

shows $ S_1 = S_2 $