IsarMathLib

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

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.

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.

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.

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.

A module is a ring action on an abelian group.

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.

We indeed talk about modules in the module0 context.

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

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

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.

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

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.

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.

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

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

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.

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

The scalar addition is distributive with respect to scalar multiplication.

Multiplication by scalars is associative with multiplication of scalars.

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

Multiplying by zero is zero.

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