IsarMathLib

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

theory Module_ZF imports Ring_ZF_3 Field_ZF
begin

A module is a generalization of the concept of a vector space in which scalars do not form a field but a ring.

Definition and basic properties of modules

Let \(R\) be a ring and \(M\) be an abelian group. The most common definition of a left \(R\)-module posits the existence of a scalar multiplication operation \(R\times M\rightarrow M\) satisfying certain four properties. Here we take a bit more concise and abstract approach defining a module as a ring action on an abelian group.

We know that endomorphisms of an abelian group \(\cal{M}\) form a ring with pointwise addition as the additive operation and composition as the ring multiplication. This asssertion is a bit imprecise though as the domain of pointwise addition is a binary operation on the space of functions \(\cal{M}\rightarrow \cal{M}\) (i.e. its domain is \((\cal{M}\rightarrow \cal{M})\times \cal{M}\rightarrow \cal{M}\)) while we need the space of endomorphisms to be the domain of the ring addition and multiplication. Therefore, to get the actual additive operation we need to restrict the pointwise addition of functions \(\cal{M}\rightarrow \cal{M}\) to the set of endomorphisms of \(\cal{M}\). Recall from the Group_ZF_5 that the InEnd operator restricts an operation to the set of endomorphisms and see the func_ZF theory for definitions of lifting an operation on a set to a function space over that set.

definition

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

Similarly we define the multiplication in the ring of endomorphisms as the restriction of compositions to the endomorphisms of \(\cal{M}\). See the func_ZF theory for the definition of the Composition operator.

definition

\( \text{EndMult}(\mathcal{M} ,A) \equiv \text{InEnd}( \text{Composition}(\mathcal{M} ),\mathcal{M} ,A) \)

We can now reformulate the theorem end_is_ring from the Group_ZF_5 theory in terms of the addition and multiplication of endomorphisms defined above.

lemma (in abelian_group) end_is_ring1:

shows \( \text{IsAring}( \text{End}(G,P), \text{EndAdd}(G,P), \text{EndMult}(G,P)) \) using end_is_ring unfolding EndAdd_def, EndMult_def

We define an action as a homomorphism into a space of endomorphisms (typically of some abelian group). In the definition below \(S\) is the set of scalars, \(A\) is the addition operation on this set, \(M\) is multiplication on the set, \(V\) is the group, \(A_V\) is the group operation, and \(H\) is the ring homomorphism that of the ring of scalars to the ring of endomorphisms of the group. On the right hand side of the definition \( \text{End}(V,A_V) \) is the set of endomorphisms, This definition is only ever used as part of the definition of a module and vector space, it's just convenient to split it off to shorten the main definitions.

definition

\( \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)) \)

A module is a ring action on an abelian group.

definition

\( \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) \)

The next locale defines context (i.e. common assumptions and notation) when considering modules. We reuse notation from the ring0 locale and add notation specific to modules. The addition and multiplication in the ring of scalars is denoted \(+\) and \(\cdot\), resp. The addition of module elements will be denoted \(+_V\). The multiplication (scaling) of scalars by module elemenst will be denoted \(\cdot_S\). \(\Theta\) is the zero module element, i.e. the neutral element of the abelian group of the module elements.

locale module0 = ring0 +

assumes mAbGr: \( \text{IsAgroup}(\mathcal{M} ,A_M) \wedge (A_M \text{ is commutative on } \mathcal{M} ) \)

assumes mAction: \( \text{IsAction}(R,A,M,\mathcal{M} ,A_M,H) \)

defines \( \Theta \equiv \text{ TheNeutralElement}(\mathcal{M} ,A_M) \)

defines \( v_1 +_V v_2 \equiv A_M\langle v_1,v_2\rangle \)

defines \( s \cdot _S v \equiv (H(s))(v) \)

defines \( - v \equiv \text{GroupInv}(\mathcal{M} ,A_M)(v) \)

defines \( v_1 -_V v_2 \equiv v_1 +_V ( - v_2) \)

We indeed talk about modules in the module0 context.

lemma (in module0) module_in_module0:

shows \( \text{IsLeftModule}(R,A,M,\mathcal{M} ,A_M,H) \) using ringAssum, mAbGr, mAction unfolding IsLeftModule_def

Theorems proven in the abelian_group context are valid as applied to the module0 context as applied to the abelian group of module elements.

lemma (in module0) abelian_group_valid_module0:

shows \( abelian\_group(\mathcal{M} ,A_M) \) using mAbGr, group0_def, abelian_group_def, abelian_group_axioms_def

Another way to state that theorems proven in the abelian_group context can be used in the module0 context:

sublocale module0 < mod_ab_gr: abelian_group

using abelian_group_valid_module0

Theorems proven in the ring_homo context are valid in the module0 context, as applied to ring \(R\) and the ring of endomorphisms of the group of module elements.

lemma (in module0) ring_homo_valid_module0:

shows \( ring\_homo(R,A,M, \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M), \text{EndMult}(\mathcal{M} ,A_M),H) \) using ringAssum, mAction, abelian_group_valid_module0, end_is_ring1 unfolding IsAction_def, ring_homo_def

Another way to make theorems proven in the ring_homo context available in the module0 context:

sublocale module0 < vec_act_homo: ring_homo

using ring_homo_valid_module0

In the ring of endomorphisms of the module the neutral element of the the multiplicative operation is the identity function. The neutral element of the additive operation is the zero valued constant function, which is also the value of the homomorphism that defines the module at zero.

lemma (in module0) add_mult_neut_elems:

shows \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} , A_M), \text{EndMult}(\mathcal{M} ,A_M)) = id(\mathcal{M} ) \) and \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M)) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \), \( H( 0 ) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \)proof
show \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} , A_M), \text{EndMult}(\mathcal{M} , A_M)) = id(\mathcal{M} ) \) using end_comp_monoid(2) unfolding EndMult_def
have \( H( 0 ) = \text{ TheNeutralElement}( \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M)) \) using homomor_dest_zero
also
show \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} , A_M), \text{EndAdd}(\mathcal{M} , A_M)) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \) using end_add_neut_elem unfolding EndAdd_def
finally show \( H( 0 ) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \)
qed

The value of the homomorphism defining the module is an endomorphism of the group of module elements and hence a function that maps the module into itself.

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} \) using mAction, assms, apply_funtype unfolding IsAction_def, ringHomomor_def, End_def

In the module0 context the neutral element of addition of module elements is denoted \(\Theta\). Of course \(\Theta\) is an element of the module.

lemma (in module0) zero_in_mod:

shows \( \Theta \in \mathcal{M} \) using group0_2_L2

\(\Theta\) is indeed the neutral element of addition of module elements.

lemma (in module0) zero_neutral:

assumes \( x\in \mathcal{M} \)

shows \( x +_V \Theta = x \) and \( \Theta +_V x = x \) using assms, group0_2_L2

Module axioms

A more common definition of a module assumes that \(R\) is a ring, \(V\) is an abelian group and lists a couple of properties that the multiplications of scalars (elements of \(R\)) by the elements of the module \(V\) should have. In this section we show that the definition of a module as a ring action on an abelian group \(V\) implies these properties.

\(\Theta\) is fixed by scalar multiplication.

lemma (in module0) zero_fixed:

assumes \( r\in R \)

shows \( r \cdot _S \Theta = \Theta \)proof
have \( \text{Homomor}(Hr,\mathcal{M} ,A_M,\mathcal{M} ,A_M) \) using assms, H_val_type(1) unfolding End_def
with image_neutral, mAbGr have \( (Hr)\text{ TheNeutralElement}(\mathcal{M} ,A_M) = \text{ TheNeutralElement}(\mathcal{M} ,A_M) \)
then show \( thesis \)
qed

The scalar multiplication is distributive with respect to the module addition.

lemma (in module0) module_ax1:

assumes \( r\in R \), \( x\in \mathcal{M} \), \( y\in \mathcal{M} \)

shows \( r\cdot _S(x+_Vy) = r\cdot _Sx +_V r\cdot _Sy \) using assms, H_val_type(1), endomor_eq

The scalar addition is distributive with respect to scalar multiplication.

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 \) using assms, homomor_dest_add, H_val_type(1), end_pointwise_add_val unfolding EndAdd_def

Multiplication by scalars is associative with multiplication of scalars.

lemma (in module0) module_ax3:

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

shows \( (r\cdot s)\cdot _Sx = r\cdot _S(s\cdot _Sx) \)proof
let \( e = \text{EndMult}(\mathcal{M} ,A_M)\langle H(r),H(s)\rangle \)
have \( (r\cdot s)\cdot _Sx = (H(r\cdot s))(x) \)
also
have \( (H(r\cdot s))(x) = e(x) \)proof
from mAction, assms(1,2) have \( H(r\cdot s) = e \) using homomor_dest_mult unfolding IsAction_def
then show \( thesis \) by (rule same_constr )
qed
also
have \( e(x) = r\cdot _S(s\cdot _Sx) \)proof
from assms(1,2) have \( e(x) = ( \text{Composition}(\mathcal{M} )\langle H(r),H(s)\rangle )(x) \) using H_val_type(1) unfolding EndMult_def
also
from assms have \( .\ .\ .\ = r\cdot _S(s\cdot _Sx) \) using H_val_type(2), func_ZF_5_L3
finally show \( e(x) = r\cdot _S(s\cdot _Sx) \)
qed
finally show \( thesis \)
qed

Scaling a module element by one gives the same module element.

lemma (in module0) module_ax4:

assumes \( x\in \mathcal{M} \)

shows \( 1 \cdot _Sx = x \)proof
let \( n = \text{ TheNeutralElement}( \text{End}(\mathcal{M} ,A_M), \text{EndMult}(\mathcal{M} ,A_M)) \)
from mAction have \( H(\text{ TheNeutralElement}(R,M)) = n \) unfolding IsAction_def, ringHomomor_def
moreover
have \( \text{ TheNeutralElement}(R,M) = 1 \)
ultimately have \( H(1 ) = n \)
also
have \( n = id(\mathcal{M} ) \) by (rule add_mult_neut_elems )
finally have \( H(1 ) = id(\mathcal{M} ) \)
with assms show \( 1 \cdot _Sx = x \)
qed

Multiplying by zero is zero.

lemma (in module0) mult_zero:

assumes \( g\in \mathcal{M} \)

shows \( 0 \cdot _Sg = \Theta \) using assms, add_mult_neut_elems(3), func1_3_L2

Taking inverses in a module is just multiplying by \(-1\)

lemma (in module0) inv_module:

assumes \( g\in \mathcal{M} \)

shows \( ( - 1 )\cdot _Sg = - g \)proof
have \( 1 \in R \) using Ring_ZF_1_L2(2)
then have \( ( - 1 ) \in R \) using Ring_ZF_1_L3(1)
with assms have \( g +_V (( - 1 )\cdot _Sg) = (1 \cdot _Sg) +_V (( - 1 )\cdot _Sg) \) using module_ax4
also
from assms, \( 1 \in R \), \( ( - 1 ) \in R \) have \( \ldots = (1 - 1 )\cdot _Sg \) using module_ax2 unfolding ringsub_def
also
from \( 1 \in R \) have \( \ldots = 0 \cdot _Sg \) using Ring_ZF_1_L3(7)
also
from assms have \( \ldots = \Theta \) using mult_zero
finally have \( g +_V (( - 1 )\cdot _Sg) = \Theta \)
moreover
from \( ( - 1 ) \in R \) have \( H( - 1 )\in \mathcal{M} \rightarrow \mathcal{M} \) using H_val_type(2)
with assms have \( ( - 1 )\cdot _Sg \in \mathcal{M} \) unfolding End_def using apply_type
ultimately show \( thesis \) using assms, group0_2_L9(2)
qed
end
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 EndAdd: \( \text{EndAdd}(\mathcal{M} ,A) \equiv \text{InEnd}(A \text{ lifted to function space over } \mathcal{M} ,\mathcal{M} ,A) \)
Definition of EndMult: \( \text{EndMult}(\mathcal{M} ,A) \equiv \text{InEnd}( \text{Composition}(\mathcal{M} ),\mathcal{M} ,A) \)
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) abelian_group_valid_module0: shows \( abelian\_group(\mathcal{M} ,A_M) \)
lemma (in abelian_group) end_is_ring1: shows \( \text{IsAring}( \text{End}(G,P), \text{EndAdd}(G,P), \text{EndMult}(G,P)) \)
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)) \)
lemma (in module0) ring_homo_valid_module0: shows \( ring\_homo(R,A,M, \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M), \text{EndMult}(\mathcal{M} ,A_M),H) \)
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 ring_homo) homomor_dest_zero: shows \( f( 0 _R) = 0 _S \)
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 ) \)
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 End: \( \text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,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 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 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 ring_homo) homomor_dest_add:

assumes \( x\in R \), \( y\in R \)

shows \( f(x + _Ry) = (f(x)) + _S(f(y)) \)
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 ring_homo) homomor_dest_mult:

assumes \( x\in R \), \( y\in R \)

shows \( f(x\cdot _Ry) = (f(x))\cdot _S(f(y)) \)
lemma same_constr:

assumes \( x=y \)

shows \( P(x) = P(y) \)
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 func_ZF_5_L3:

assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \) and \( x\in X \)

shows \( ( \text{Composition}(X)\langle f,g\rangle )(x) = f(g(x)) \)
lemma (in module0) add_mult_neut_elems: shows \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} , A_M), \text{EndMult}(\mathcal{M} ,A_M)) = id(\mathcal{M} ) \) and \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M)) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \), \( H( 0 ) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \)
lemma (in module0) add_mult_neut_elems: shows \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} , A_M), \text{EndMult}(\mathcal{M} ,A_M)) = id(\mathcal{M} ) \) and \( \text{ TheNeutralElement}( \text{End}(\mathcal{M} ,A_M), \text{EndAdd}(\mathcal{M} ,A_M)) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \), \( H( 0 ) = \text{ConstantFunction}(\mathcal{M} ,\Theta ) \)
lemma func1_3_L2:

assumes \( x\in X \)

shows \( \text{ConstantFunction}(X,c)(x) = c \)
lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
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 \)
lemma (in module0) module_ax4:

assumes \( x\in \mathcal{M} \)

shows \( 1 \cdot _Sx = x \)
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 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 \)
lemma (in module0) mult_zero:

assumes \( g\in \mathcal{M} \)

shows \( 0 \cdot _Sg = \Theta \)
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} \)