(* 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 "⊙ı" 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 (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 ==> 𝟬 ⊙⇘_{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 ⊕⇘_{M⇙}𝟬 ⊙⇘_{M⇙}x) ⊕⇘_{M⇙}⊖⇘_{M⇙}(𝟬 ⊙⇘_{M⇙}x)" by algebra also from M have "... = (𝟬 ⊕ 𝟬) ⊙⇘_{M⇙}x ⊕⇘_{M⇙}⊖⇘_{M⇙}(𝟬 ⊙⇘_{M⇙}x)" by (simp add: smult_l_distr del: R.l_zero R.r_zero) also from facts have "... = 𝟬⇘_{M⇙}" apply algebra apply algebra done finally show ?thesis . qed lemma (in algebra) 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⇙})" by algebra 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⇙}" by algebra finally show ?thesis . qed lemma (in algebra) 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)" by algebra also from RM have "... = (⊖a ⊕ a) ⊙⇘_{M⇙}x ⊕⇘_{M⇙}⊖⇘_{M⇙}(a ⊙⇘_{M⇙}x)" by (simp add: smult_l_distr) also from facts smult_l_null have "... = ⊖⇘_{M⇙}(a ⊙⇘_{M⇙}x)" apply algebra apply algebra done finally show ?thesis . qed lemma (in algebra) 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)" by algebra also from RM have "... = a ⊙⇘_{M⇙}(⊖⇘_{M⇙}x ⊕⇘_{M⇙}x) ⊕⇘_{M⇙}⊖⇘_{M⇙}(a ⊙⇘_{M⇙}x)" by (simp add: smult_r_distr) also from facts smult_r_null have "... = ⊖⇘_{M⇙}(a ⊙⇘_{M⇙}x)" by algebra finally show ?thesis . qed end