Quelle  Module.thy

(*  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 ==> 1 ⊙🪙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 ==> 1 ⊙🪙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 Modules›

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

lemma (in module) smult_r_null [simp]:
  "a ∈ carrier R ==> a ⊙🪙M🪙 0🪙M🪙 = 0🪙M🪙"
proof -
  assume R: "a ∈ carrier R"
  note facts = R smult_closed
  from facts have "a ⊙🪙M🪙 0🪙M🪙 = (a ⊙🪙M🪙 0🪙M🪙 ⊕🪙M🪙 a ⊙🪙M🪙 0🪙M🪙) ⊕🪙M🪙 ⊖🪙M🪙 (a ⊙🪙M🪙 0🪙M🪙)"
    by (simp add: M.add.inv_solve_right)
  also from R have "... = a ⊙🪙M🪙 (0🪙M🪙 ⊕🪙M🪙 0🪙M🪙) ⊕🪙M🪙 ⊖🪙M🪙 (a ⊙🪙M🪙 0🪙M🪙)"
    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
  also from facts have "... = 0🪙M🪙"
    by (simp add: M.r_neg)
  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)"
    by (simp add: M.add.inv_solve_right)
  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)"
    by (simp add: R.l_neg)
  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)"
    by (simp add: M.add.inv_solve_right)
  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_l_null have "... = ⊖🪙M🪙(a ⊙🪙M🪙 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 ⊙🪙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
    by (simp add: Pi_def smult_r_distr)
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: "0🪙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
  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 ==> ⊖🪙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 ==> 1🪙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