# Theory Module

theory Module
imports Ring
```(*  Title:      HOL/Algebra/Module.thy
Author:     Clemens Ballarin, started 15 April 2003
with contributions by Martin Baillon
*)

theory Module
imports Ring
begin

section ‹Modules over an Abelian Group›

subsection ‹Definitions›

record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "⊙ı" 70)

locale module = R?: cring + M?: abelian_group M for M (structure) +
assumes smult_closed [simp, intro]:
"[| a ∈ carrier R; x ∈ carrier M |] ==> a ⊙⇘M⇙ x ∈ carrier M"
and smult_l_distr:
"[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊕ b) ⊙⇘M⇙ x = a ⊙⇘M⇙ x ⊕⇘M⇙ b ⊙⇘M⇙ x"
and smult_r_distr:
"[| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
a ⊙⇘M⇙ (x ⊕⇘M⇙ y) = a ⊙⇘M⇙ x ⊕⇘M⇙ a ⊙⇘M⇙ y"
and smult_assoc1:
"[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊗ b) ⊙⇘M⇙ x = a ⊙⇘M⇙ (b ⊙⇘M⇙ x)"
and smult_one [simp]:
"x ∈ carrier M ==> 𝟭 ⊙⇘M⇙ x = x"

locale algebra = module + cring M +
assumes smult_assoc2:
"[| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
(a ⊙⇘M⇙ x) ⊗⇘M⇙ y = a ⊙⇘M⇙ (x ⊗⇘M⇙ y)"

lemma moduleI:
fixes R (structure) and M (structure)
assumes cring: "cring R"
and abelian_group: "abelian_group M"
and smult_closed:
"!!a x. [| a ∈ carrier R; x ∈ carrier M |] ==> a ⊙⇘M⇙ x ∈ carrier M"
and smult_l_distr:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊕ b) ⊙⇘M⇙ x = (a ⊙⇘M⇙ x) ⊕⇘M⇙ (b ⊙⇘M⇙ x)"
and smult_r_distr:
"!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
a ⊙⇘M⇙ (x ⊕⇘M⇙ y) = (a ⊙⇘M⇙ x) ⊕⇘M⇙ (a ⊙⇘M⇙ y)"
and smult_assoc1:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊗ b) ⊙⇘M⇙ x = a ⊙⇘M⇙ (b ⊙⇘M⇙ x)"
and smult_one:
"!!x. x ∈ carrier M ==> 𝟭 ⊙⇘M⇙ x = x"
shows "module R M"
by (auto intro: module.intro cring.axioms abelian_group.axioms
module_axioms.intro assms)

lemma algebraI:
fixes R (structure) and M (structure)
assumes R_cring: "cring R"
and M_cring: "cring M"
and smult_closed:
"!!a x. [| a ∈ carrier R; x ∈ carrier M |] ==> a ⊙⇘M⇙ x ∈ carrier M"
and smult_l_distr:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊕ b) ⊙⇘M⇙ x = (a ⊙⇘M⇙ x) ⊕⇘M⇙ (b ⊙⇘M⇙ x)"
and smult_r_distr:
"!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
a ⊙⇘M⇙ (x ⊕⇘M⇙ y) = (a ⊙⇘M⇙ x) ⊕⇘M⇙ (a ⊙⇘M⇙ y)"
and smult_assoc1:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊗ b) ⊙⇘M⇙ x = a ⊙⇘M⇙ (b ⊙⇘M⇙ x)"
and smult_one:
"!!x. x ∈ carrier M ==> (one R) ⊙⇘M⇙ x = x"
and smult_assoc2:
"!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
(a ⊙⇘M⇙ x) ⊗⇘M⇙ y = a ⊙⇘M⇙ (x ⊗⇘M⇙ y)"
shows "algebra R M"
apply intro_locales
apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
apply (rule module_axioms.intro)
apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
apply (rule algebra_axioms.intro)
done

lemma (in algebra) R_cring: "cring R" ..

lemma (in algebra) M_cring: "cring M" ..

lemma (in algebra) module: "module R M"
by (auto intro: moduleI R_cring is_abelian_group smult_l_distr smult_r_distr smult_assoc1)

subsection ‹Basic Properties of Modules›

lemma (in module) smult_l_null [simp]:
"x ∈ carrier M ==> 𝟬 ⊙⇘M⇙ x = 𝟬⇘M⇙"
proof-
assume M : "x ∈ carrier M"
note facts = M smult_closed [OF R.zero_closed]
from facts have "𝟬 ⊙⇘M⇙ x = (𝟬 ⊕ 𝟬) ⊙⇘M⇙ x "
using smult_l_distr by auto
also have "... = 𝟬 ⊙⇘M⇙ x ⊕⇘M⇙ 𝟬 ⊙⇘M⇙ x"
using smult_l_distr[of 𝟬 𝟬 x] facts by auto
finally show "𝟬 ⊙⇘M⇙ x = 𝟬⇘M⇙" using facts
qed

lemma (in module) smult_r_null [simp]:
"a ∈ carrier R ==> a ⊙⇘M⇙ 𝟬⇘M⇙ = 𝟬⇘M⇙"
proof -
assume R: "a ∈ carrier R"
note facts = R smult_closed
from facts have "a ⊙⇘M⇙ 𝟬⇘M⇙ = (a ⊙⇘M⇙ 𝟬⇘M⇙ ⊕⇘M⇙ a ⊙⇘M⇙ 𝟬⇘M⇙) ⊕⇘M⇙ ⊖⇘M⇙ (a ⊙⇘M⇙ 𝟬⇘M⇙)"
also from R have "... = a ⊙⇘M⇙ (𝟬⇘M⇙ ⊕⇘M⇙ 𝟬⇘M⇙) ⊕⇘M⇙ ⊖⇘M⇙ (a ⊙⇘M⇙ 𝟬⇘M⇙)"
by (simp add: smult_r_distr del: M.l_zero M.r_zero)
also from facts have "... = 𝟬⇘M⇙"
finally show ?thesis .
qed

lemma (in module) smult_l_minus:
"⟦ a ∈ carrier R; x ∈ carrier M ⟧ ⟹ (⊖a) ⊙⇘M⇙ x = ⊖⇘M⇙ (a ⊙⇘M⇙ x)"
proof-
assume RM: "a ∈ carrier R" "x ∈ carrier M"
from RM have a_smult: "a ⊙⇘M⇙ x ∈ carrier M" by simp
from RM have ma_smult: "⊖a ⊙⇘M⇙ x ∈ carrier M" by simp
note facts = RM a_smult ma_smult
from facts have "(⊖a) ⊙⇘M⇙ x = (⊖a ⊙⇘M⇙ x ⊕⇘M⇙ a ⊙⇘M⇙ x) ⊕⇘M⇙ ⊖⇘M⇙(a ⊙⇘M⇙ x)"
also from RM have "... = (⊖a ⊕ a) ⊙⇘M⇙ x ⊕⇘M⇙ ⊖⇘M⇙(a ⊙⇘M⇙ x)"
also from facts smult_l_null have "... = ⊖⇘M⇙(a ⊙⇘M⇙ x)"
finally show ?thesis .
qed

lemma (in module) smult_r_minus:
"[| a ∈ carrier R; x ∈ carrier M |] ==> a ⊙⇘M⇙ (⊖⇘M⇙x) = ⊖⇘M⇙ (a ⊙⇘M⇙ x)"
proof -
assume RM: "a ∈ carrier R" "x ∈ carrier M"
note facts = RM smult_closed
from facts have "a ⊙⇘M⇙ (⊖⇘M⇙x) = (a ⊙⇘M⇙ ⊖⇘M⇙x ⊕⇘M⇙ a ⊙⇘M⇙ x) ⊕⇘M⇙ ⊖⇘M⇙(a ⊙⇘M⇙ x)"
also from RM have "... = a ⊙⇘M⇙ (⊖⇘M⇙x ⊕⇘M⇙ x) ⊕⇘M⇙ ⊖⇘M⇙(a ⊙⇘M⇙ x)"
also from facts smult_l_null have "... = ⊖⇘M⇙(a ⊙⇘M⇙ x)"
finally show ?thesis .
qed

lemma (in module) finsum_smult_ldistr:
"⟦ finite A; a ∈ carrier R; f: A → carrier M ⟧ ⟹
a ⊙⇘M⇙ (⨁⇘M⇙ i ∈ A. (f i)) = (⨁⇘M⇙ i ∈ A. ( a ⊙⇘M⇙ (f i)))"
proof (induct set: finite)
case empty then show ?case
by (metis M.finsum_empty M.zero_closed R.zero_closed r_null smult_assoc1 smult_l_null)
next
case (insert x F) then show ?case
qed

subsection ‹Submodules›

locale submodule = subgroup H "add_monoid M" for H and R :: "('a, 'b) ring_scheme" and M (structure)
+ assumes smult_closed [simp, intro]:
"⟦a ∈ carrier R; x ∈ H⟧ ⟹ a ⊙⇘M⇙ x ∈ H"

lemma (in module) submoduleI :
assumes subset: "H ⊆ carrier M"
and zero: "𝟬⇘M⇙ ∈ H"
and a_inv: "!!a. a ∈ H ⟹ ⊖⇘M⇙ a ∈ H"
and add : "⋀ a b. ⟦a ∈ H ; b ∈ H⟧ ⟹ a ⊕⇘M⇙ b ∈ H"
and smult_closed : "⋀ a x. ⟦a ∈ carrier R; x ∈ H⟧ ⟹ a ⊙⇘M⇙ x ∈ H"
shows "submodule H R M"
apply (intro submodule.intro subgroup.intro)
using assms unfolding submodule_axioms_def

lemma (in module) submoduleE :
assumes "submodule H R M"
shows "H ⊆ carrier M"
and "H ≠ {}"
and "⋀a. a ∈ H ⟹ ⊖⇘M⇙ a ∈ H"
and "⋀a b. ⟦a ∈ carrier R; b ∈ H⟧ ⟹ a ⊙⇘M⇙ b ∈ H"
and "⋀ a b. ⟦a ∈ H ; b ∈ H⟧ ⟹ a ⊕⇘M⇙ b ∈ H"
and "⋀ x. x ∈ H ⟹ (a_inv M x) ∈ H"
using group.subgroupE[of "add_monoid M" H, OF _ submodule.axioms(1)[OF assms]] a_comm_group
submodule.smult_closed[OF assms]
unfolding comm_group_def a_inv_def
by auto

lemma (in module) carrier_is_submodule :
"submodule (carrier M) R M"
apply (intro  submoduleI)
using a_comm_group group.inv_closed unfolding comm_group_def a_inv_def group_def monoid_def
by auto

lemma (in submodule) submodule_is_module :
assumes "module R M"
shows "module R (M⦇carrier := H⦈)"
proof (auto intro! : moduleI abelian_group.intro)
show "cring (R)" using assms unfolding module_def by auto
show "abelian_monoid (M⦇carrier := H⦈)"
using comm_monoid.submonoid_is_comm_monoid[OF _ subgroup_is_submonoid] assms
unfolding abelian_monoid_def module_def abelian_group_def
by auto
thus "abelian_group_axioms (M⦇carrier := H⦈)"
using subgroup_is_group assms
unfolding abelian_group_axioms_def comm_group_def abelian_monoid_def module_def abelian_group_def
by auto
show "⋀z. z ∈ H ⟹ 𝟭⇘R⇙ ⊙ z = z"
using subgroup.subset[OF subgroup_axioms] module.smult_one[OF assms]
by auto
fix a b x y assume a : "a ∈ carrier R" and b : "b ∈ carrier R" and x : "x ∈ H" and y : "y ∈ H"
show "(a ⊕⇘R⇙ b) ⊙ x = a ⊙ x ⊕ b ⊙ x"
using a b x module.smult_l_distr[OF assms] subgroup.subset[OF subgroup_axioms]
by auto
show "a ⊙ (x ⊕ y) = a ⊙ x ⊕ a ⊙ y"
using a x y module.smult_r_distr[OF assms] subgroup.subset[OF subgroup_axioms]
by auto
show "a ⊗⇘R⇙ b ⊙ x = a ⊙ (b ⊙ x)"
using a b x module.smult_assoc1[OF assms] subgroup.subset[OF subgroup_axioms]
by auto
qed

lemma (in module) module_incl_imp_submodule :
assumes "H ⊆ carrier M"
and "module R (M⦇carrier := H⦈)"
shows "submodule H R M"
apply (intro submodule.intro)
using add.group_incl_imp_subgroup[OF assms(1)] assms module.axioms(2)[OF assms(2)]
module.smult_closed[OF assms(2)]
unfolding abelian_group_def abelian_group_axioms_def comm_group_def submodule_axioms_def
by simp_all

end
```