(* Title: HOL/Algebra/Module.thy
Author: Clemens Ballarin, started 15 April 2003
with contributions by Martin Baillon
*)
theory Module
imports Ring
begin
section \<open>Modules over an Abelian Group\<close>
subsection \<open>Definitions\<close>
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 \\<^bsub>M\<^esub> x \ carrier M"
and smult_l_distr:
"[| a \ carrier R; b \ carrier R; x \ carrier M |] ==>
(a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"
and smult_r_distr:
"[| a \ carrier R; x \ carrier M; y \ carrier M |] ==>
a \<odot>\<^bsub>M\<^esub> (x \<oplus>\<^bsub>M\<^esub> y) = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> y"
and smult_assoc1:
"[| a \ carrier R; b \ carrier R; x \ carrier M |] ==>
(a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
and smult_one [simp]:
"x \ carrier M ==> \ \\<^bsub>M\<^esub> x = x"
locale algebra = module + cring M +
assumes smult_assoc2:
"[| a \ carrier R; x \ carrier M; y \ carrier M |] ==>
(a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> 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 \\<^bsub>M\<^esub> x \ carrier M"
and smult_l_distr:
"!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==>
(a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
and smult_r_distr:
"!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==>
a \<odot>\<^bsub>M\<^esub> (x \<oplus>\<^bsub>M\<^esub> y) = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> y)"
and smult_assoc1:
"!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==>
(a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
and smult_one:
"!!x. x \ carrier M ==> \ \\<^bsub>M\<^esub> 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 \\<^bsub>M\<^esub> x \ carrier M"
and smult_l_distr:
"!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==>
(a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
and smult_r_distr:
"!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==>
a \<odot>\<^bsub>M\<^esub> (x \<oplus>\<^bsub>M\<^esub> y) = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> y)"
and smult_assoc1:
"!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==>
(a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
and smult_one:
"!!x. x \ carrier M ==> (one R) \\<^bsub>M\<^esub> x = x"
and smult_assoc2:
"!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==>
(a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> 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 \<open>Basic Properties of Modules\<close>
lemma (in module) smult_l_null [simp]:
"x \ carrier M ==> \ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>"
proof-
assume M : "x \ carrier M"
note facts = M smult_closed [OF R.zero_closed]
from facts have "\ \\<^bsub>M\<^esub> x = (\ \ \) \\<^bsub>M\<^esub> x "
using smult_l_distr by auto
also have "... = \ \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \ \\<^bsub>M\<^esub> x"
using smult_l_distr[of \<zero> \<zero> x] facts by auto
finally show "\ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>" using facts
by (metis M.add.r_cancel_one')
qed
lemma (in module) smult_r_null [simp]:
"a \ carrier R ==> a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> = \\<^bsub>M\<^esub>"
proof -
assume R: "a \ carrier R"
note facts = R smult_closed
from facts have "a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> = (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>)"
by (simp add: M.add.inv_solve_right)
also from R have "... = a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub> \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>)"
by (simp add: smult_r_distr del: M.l_zero M.r_zero)
also from facts have "... = \\<^bsub>M\<^esub>"
by (simp add: M.r_neg)
finally show ?thesis .
qed
lemma (in module) smult_l_minus:
"\ a \ carrier R; x \ carrier M \ \ (\a) \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)"
proof-
assume RM: "a \ carrier R" "x \ carrier M"
from RM have a_smult: "a \\<^bsub>M\<^esub> x \ carrier M" by simp
from RM have ma_smult: "\a \\<^bsub>M\<^esub> x \ carrier M" by simp
note facts = RM a_smult ma_smult
from facts have "(\a) \\<^bsub>M\<^esub> x = (\a \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)"
by (simp add: M.add.inv_solve_right)
also from RM have "... = (\a \ a) \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)"
by (simp add: smult_l_distr)
also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)"
by (simp add: R.l_neg)
finally show ?thesis .
qed
lemma (in module) smult_r_minus:
"[| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x) = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)"
proof -
assume RM: "a \ carrier R" "x \ carrier M"
note facts = RM smult_closed
from facts have "a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x) = (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>x \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)"
by (simp add: M.add.inv_solve_right)
also from RM have "... = a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)"
by (simp add: smult_r_distr)
also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)"
by (metis M.add.inv_closed M.add.inv_solve_right M.l_neg R.zero_closed r_null smult_assoc1)
finally show ?thesis .
qed
lemma (in module) finsum_smult_ldistr:
"\ finite A; a \ carrier R; f: A \ carrier M \ \
a \<odot>\<^bsub>M\<^esub> (\<Oplus>\<^bsub>M\<^esub> i \<in> A. (f i)) = (\<Oplus>\<^bsub>M\<^esub> i \<in> A. ( a \<odot>\<^bsub>M\<^esub> (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
by (simp add: Pi_def smult_r_distr)
qed
subsection \<open>Submodules\<close>
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 \\<^bsub>M\<^esub> x \ H"
lemma (in module) submoduleI :
assumes subset: "H \ carrier M"
and zero: "\\<^bsub>M\<^esub> \ H"
and a_inv: "!!a. a \ H \ \\<^bsub>M\<^esub> a \ H"
and add : "\ a b. \a \ H ; b \ H\ \ a \\<^bsub>M\<^esub> b \ H"
and smult_closed : "\ a x. \a \ carrier R; x \ H\ \ a \\<^bsub>M\<^esub> x \ H"
shows "submodule H R M"
apply (intro submodule.intro subgroup.intro)
using assms unfolding submodule_axioms_def
by (simp_all add : a_inv_def)
lemma (in module) submoduleE :
assumes "submodule H R M"
shows "H \ carrier M"
and "H \ {}"
and "\a. a \ H \ \\<^bsub>M\<^esub> a \ H"
and "\a b. \a \ carrier R; b \ H\ \ a \\<^bsub>M\<^esub> b \ H"
and "\ a b. \a \ H ; b \ H\ \ a \\<^bsub>M\<^esub> 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 \ \\<^bsub>R\<^esub> \ 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 \\<^bsub>R\<^esub> 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 \\<^bsub>R\<^esub> 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
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
