Quelle Module.thy Sprache: Isabelle

(*  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 \<open>\<odot>\<index>\<close> 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

quality97%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.