Theory Module_ZF
section ‹ Modules›
theory Module_ZF imports Ring_ZF_3 Field_ZF
begin
text‹A module is a generalization of the concept of a vector space in which scalars
do not form a field but a ring. ›
subsection‹Definition and basic properties of modules›
text‹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. ›
text‹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 "EndAdd(ℳ,A) ≡ InEnd(A {lifted to function space over} ℳ,ℳ,A)"
text‹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 "EndMult(ℳ,A) ≡ InEnd(Composition(ℳ),ℳ,A)"
text‹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 "IsAring(End(G,P),EndAdd(G,P),EndMult(G,P))"
using end_is_ring unfolding EndAdd_def EndMult_def by simp
text‹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 ‹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
"IsAction(S,A,M,ℳ,A⇩M,H) ≡ ringHomomor(H,S,A,M,End(ℳ,A⇩M),EndAdd(ℳ,A⇩M),EndMult(ℳ,A⇩M))"
text‹A module is a ring action on an abelian group.›
definition "IsLeftModule(S,A,M,ℳ,A⇩M,H) ≡
IsAring(S,A,M) ∧ IsAgroup(ℳ,A⇩M) ∧ (A⇩M {is commutative on} ℳ) ∧ IsAction(S,A,M,ℳ,A⇩M,H)"
text‹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 +
fixes ℳ A⇩M H
assumes mAbGr: "IsAgroup(ℳ,A⇩M) ∧ (A⇩M {is commutative on} ℳ)"
assumes mAction: "IsAction(R,A,M,ℳ,A⇩M,H)"
fixes zero_vec ("Θ")
defines zero_vec_def [simp]: "Θ ≡ TheNeutralElement(ℳ,A⇩M)"
fixes vAdd (infixl "+⇩V" 80)
defines vAdd_def [simp]: "v⇩1 +⇩V v⇩2 ≡ A⇩M`⟨v⇩1,v⇩2⟩"
fixes scal (infix "⋅⇩S" 90)
defines scal_def [simp]: "s ⋅⇩S v ≡ (H`(s))`(v)"
fixes negV ("─_")
defines negV_def [simp]: "─v ≡ GroupInv(ℳ,A⇩M)`(v)"
fixes vSub (infix "-⇩V" 80)
defines vSub_def [simp]: "v⇩1 -⇩V v⇩2 ≡ v⇩1 +⇩V (─v⇩2)"
text‹We indeed talk about modules in the ‹module0› context.›
lemma (in module0) module_in_module0: shows "IsLeftModule(R,A,M,ℳ,A⇩M,H)"
using ringAssum mAbGr mAction unfolding IsLeftModule_def by simp
text‹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(ℳ,A⇩M)"
using mAbGr group0_def abelian_group_def abelian_group_axioms_def
by simp
text‹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 "ℳ" "A⇩M" "Θ" vAdd negV
using abelian_group_valid_module0 by auto
text‹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,End(ℳ,A⇩M),EndAdd(ℳ,A⇩M),EndMult(ℳ,A⇩M),H)"
using ringAssum mAction abelian_group_valid_module0 abelian_group.end_is_ring1
unfolding IsAction_def ring_homo_def by simp
text‹Another way to make theorems proven in the ‹ring_homo› context available in the
‹module0› context: ›
sublocale module0 < vec_act_homo: ring_homo R A M
"End(ℳ,A⇩M)" "EndAdd(ℳ,A⇩M)" "EndMult(ℳ,A⇩M)" H
ringa
ringminus
ringsub
ringm
ringzero
ringone
ringtwo
ringsq
"λx y. EndAdd(ℳ,A⇩M) ` ⟨x, y⟩"
"λx. GroupInv(End(ℳ,A⇩M), EndAdd(ℳ, A⇩M))`(x)"
"λx y. EndAdd(ℳ,A⇩M)`⟨x,GroupInv(End(ℳ, A⇩M), EndAdd(ℳ, A⇩M))`(y)⟩"
"λx y. EndMult(ℳ,A⇩M)`⟨x, y⟩"
"TheNeutralElement(End(ℳ, A⇩M), EndAdd(ℳ, A⇩M))"
"TheNeutralElement(End(ℳ, A⇩M), EndMult(ℳ, A⇩M))"
"EndAdd(ℳ,A⇩M)`⟨TheNeutralElement(End(ℳ, A⇩M),EndMult(ℳ, A⇩M)),TheNeutralElement(End(ℳ, A⇩M), EndMult(ℳ,A⇩M))⟩"
"λx. EndMult(ℳ,A⇩M)`⟨x, x⟩"
using ring_homo_valid_module0 by auto
text‹In the ring of endomorphisms of the module the neutral element of the additive operation
is the zero valued constant function. The neutral element of the multiplicative operation is
the identity function.›
lemma (in module0) add_mult_neut_elems: shows
"TheNeutralElement(End(ℳ, A⇩M), EndMult(ℳ,A⇩M)) = id(ℳ)" and
"TheNeutralElement(End(ℳ,A⇩M),EndAdd(ℳ,A⇩M)) = ConstantFunction(ℳ,Θ)"
proof -
show "TheNeutralElement(End(ℳ, A⇩M), EndMult(ℳ, A⇩M)) = id(ℳ)"
using mod_ab_gr.end_comp_monoid(2) unfolding EndMult_def
by blast
show "TheNeutralElement(End(ℳ, A⇩M), EndAdd(ℳ, A⇩M)) = ConstantFunction(ℳ,Θ)"
using mod_ab_gr.end_add_neut_elem unfolding EndAdd_def by blast
qed
text‹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∈R" shows
"H`(r) ∈ End(ℳ,A⇩M)" and "H`(r):ℳ→ℳ"
using mAction assms apply_funtype unfolding IsAction_def ringHomomor_def End_def
by auto
text‹ 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 "Θ ∈ ℳ"
using mod_ab_gr.group0_2_L2 by simp
text‹ $\Theta$ is indeed the neutral element of addition of module elements.›
lemma (in module0) zero_neutral: assumes "x∈ℳ"
shows "x +⇩V Θ = x" and "Θ +⇩V x = x"
using assms mod_ab_gr.group0_2_L2 by simp_all
subsection‹Module axioms›
text‹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. ›
text‹The scalar multiplication is distributive with respect to the module addition.›
lemma (in module0) module_ax1: assumes "r∈R" "x∈ℳ" "y∈ℳ"
shows "r⋅⇩S(x+⇩Vy) = r⋅⇩Sx +⇩V r⋅⇩Sy"
using assms H_val_type(1) mod_ab_gr.endomor_eq by simp
text‹The scalar addition is distributive with respect to scalar multiplication.›
lemma (in module0) module_ax2: assumes "r∈R" "s∈R" "x∈ℳ"
shows "(r\<ra>s)⋅⇩Sx = r⋅⇩Sx +⇩V s⋅⇩Sx"
using assms vec_act_homo.homomor_dest_add H_val_type(1) mod_ab_gr.end_pointwise_add_val
unfolding EndAdd_def by simp
text‹Multiplication by scalars is associative with multiplication of scalars.›
lemma (in module0) module_ax3: assumes "r∈R" "s∈R" "x∈ℳ"
shows "(r⋅s)⋅⇩Sx = r⋅⇩S(s⋅⇩Sx)"
proof -
let ?e = "EndMult(ℳ,A⇩M)`⟨H`(r),H`(s)⟩"
have "(r⋅s)⋅⇩Sx = (H`(r⋅s))`(x)" by simp
also have "(H`(r⋅s))`(x) = ?e`(x)"
proof -
from mAction assms(1,2) have "H`(r⋅s) = ?e"
using vec_act_homo.homomor_dest_mult unfolding IsAction_def
by blast
then show ?thesis by (rule same_constr)
qed
also have "?e`(x) = r⋅⇩S(s⋅⇩Sx)"
proof -
from assms(1,2) have "?e`(x) = (Composition(ℳ)`⟨H`(r),H`(s)⟩)`(x)"
using H_val_type(1) unfolding EndMult_def by simp
also from assms have "... = r⋅⇩S(s⋅⇩Sx)" using H_val_type(2) func_ZF_5_L3
by simp
finally show "?e`(x) = r⋅⇩S(s⋅⇩Sx)" by blast
qed
finally show ?thesis by simp
qed
text‹Scaling a module element by one gives the same module element.›
lemma (in module0) module_ax4: assumes "x∈ℳ" shows "𝟭⋅⇩Sx = x"
proof -
let ?n = "TheNeutralElement(End(ℳ,A⇩M),EndMult(ℳ,A⇩M))"
from mAction have "H`(TheNeutralElement(R,M)) = ?n"
unfolding IsAction_def ringHomomor_def by blast
moreover have "TheNeutralElement(R,M) = 𝟭" by simp
ultimately have "H`(𝟭) = ?n" by blast
also have "?n = id(ℳ)" by (rule add_mult_neut_elems)
finally have "H`(𝟭) = id(ℳ)" by simp
with assms show "𝟭⋅⇩Sx = x" by simp
qed
end