Theory Module

theory Module
imports Ring
(*  Title:      HOL/Algebra/Module.thy
Author: Clemens Ballarin, started 15 April 2003
Copyright: Clemens Ballarin
*)


theory Module
imports Ring
begin

section {* Modules over an Abelian Group *}

subsection {* Definitions *}

record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)

locale module = R: cring + M: abelian_group M for M (structure) +
assumes smult_closed [simp, intro]:
"[| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M x ∈ carrier M"
and smult_l_distr:
"[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊕ b) \<odot>M x = a \<odot>M x ⊕M b \<odot>M x"

and smult_r_distr:
"[| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
a \<odot>M (x ⊕M y) = a \<odot>M x ⊕M a \<odot>M y"

and smult_assoc1:
"[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊗ b) \<odot>M x = a \<odot>M (b \<odot>M x)"

and smult_one [simp]:
"x ∈ carrier M ==> \<one> \<odot>M x = x"

locale algebra = module + cring M +
assumes smult_assoc2:
"[| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
(a \<odot>M x) ⊗M y = a \<odot>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 \<odot>M x ∈ carrier M"
and smult_l_distr:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊕ b) \<odot>M x = (a \<odot>M x) ⊕M (b \<odot>M x)"

and smult_r_distr:
"!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
a \<odot>M (x ⊕M y) = (a \<odot>M x) ⊕M (a \<odot>M y)"

and smult_assoc1:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊗ b) \<odot>M x = a \<odot>M (b \<odot>M x)"

and smult_one:
"!!x. x ∈ carrier M ==> \<one> \<odot>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 \<odot>M x ∈ carrier M"
and smult_l_distr:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊕ b) \<odot>M x = (a \<odot>M x) ⊕M (b \<odot>M x)"

and smult_r_distr:
"!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
a \<odot>M (x ⊕M y) = (a \<odot>M x) ⊕M (a \<odot>M y)"

and smult_assoc1:
"!!a b x. [| a ∈ carrier R; b ∈ carrier R; x ∈ carrier M |] ==>
(a ⊗ b) \<odot>M x = a \<odot>M (b \<odot>M x)"

and smult_one:
"!!x. x ∈ carrier M ==> (one R) \<odot>M x = x"
and smult_assoc2:
"!!a x y. [| a ∈ carrier R; x ∈ carrier M; y ∈ carrier M |] ==>
(a \<odot>M x) ⊗M y = a \<odot>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 (simp add: smult_closed)
apply (simp add: smult_l_distr)
apply (simp add: smult_r_distr)
apply (simp add: smult_assoc1)
apply (simp add: smult_one)
apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
apply (rule algebra_axioms.intro)
apply (simp add: smult_assoc2)
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 Algebras *}

lemma (in algebra) smult_l_null [simp]:
"x ∈ carrier M ==> \<zero> \<odot>M x = \<zero>M"
proof -
assume M: "x ∈ carrier M"
note facts = M smult_closed [OF R.zero_closed]
from facts have "\<zero> \<odot>M x = (\<zero> \<odot>M x ⊕M \<zero> \<odot>M x) ⊕M \<ominus>M (\<zero> \<odot>M x)" by algebra
also from M have "... = (\<zero> ⊕ \<zero>) \<odot>M x ⊕M \<ominus>M (\<zero> \<odot>M x)"
by (simp add: smult_l_distr del: R.l_zero R.r_zero)
also from facts have "... = \<zero>M" apply algebra apply algebra done
finally show ?thesis .
qed

lemma (in algebra) smult_r_null [simp]:
"a ∈ carrier R ==> a \<odot>M \<zero>M = \<zero>M";
proof -
assume R: "a ∈ carrier R"
note facts = R smult_closed
from facts have "a \<odot>M \<zero>M = (a \<odot>M \<zero>MM a \<odot>M \<zero>M) ⊕M \<ominus>M (a \<odot>M \<zero>M)"
by algebra
also from R have "... = a \<odot>M (\<zero>MM \<zero>M) ⊕M \<ominus>M (a \<odot>M \<zero>M)"
by (simp add: smult_r_distr del: M.l_zero M.r_zero)
also from facts have "... = \<zero>M" by algebra
finally show ?thesis .
qed

lemma (in algebra) smult_l_minus:
"[| a ∈ carrier R; x ∈ carrier M |] ==> (\<ominus>a) \<odot>M x = \<ominus>M (a \<odot>M x)"
proof -
assume RM: "a ∈ carrier R" "x ∈ carrier M"
from RM have a_smult: "a \<odot>M x ∈ carrier M" by simp
from RM have ma_smult: "\<ominus>a \<odot>M x ∈ carrier M" by simp
note facts = RM a_smult ma_smult
from facts have "(\<ominus>a) \<odot>M x = (\<ominus>a \<odot>M x ⊕M a \<odot>M x) ⊕M \<ominus>M(a \<odot>M x)"
by algebra
also from RM have "... = (\<ominus>a ⊕ a) \<odot>M x ⊕M \<ominus>M(a \<odot>M x)"
by (simp add: smult_l_distr)
also from facts smult_l_null have "... = \<ominus>M(a \<odot>M x)"
apply algebra apply algebra done
finally show ?thesis .
qed

lemma (in algebra) smult_r_minus:
"[| a ∈ carrier R; x ∈ carrier M |] ==> a \<odot>M (\<ominus>Mx) = \<ominus>M (a \<odot>M x)"
proof -
assume RM: "a ∈ carrier R" "x ∈ carrier M"
note facts = RM smult_closed
from facts have "a \<odot>M (\<ominus>Mx) = (a \<odot>M \<ominus>Mx ⊕M a \<odot>M x) ⊕M \<ominus>M(a \<odot>M x)"
by algebra
also from RM have "... = a \<odot>M (\<ominus>Mx ⊕M x) ⊕M \<ominus>M(a \<odot>M x)"
by (simp add: smult_r_distr)
also from facts smult_r_null have "... = \<ominus>M(a \<odot>M x)" by algebra
finally show ?thesis .
qed

end