Theory Module

(*  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