src/HOL/Algebra/Module.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 29237 e90d9d51106b
child 35849 b5522b51cb1e
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/Algebra/Module.thy
     2     Author:     Clemens Ballarin, started 15 April 2003
     3     Copyright:  Clemens Ballarin
     4 *)
     5 
     6 theory Module imports Ring begin
     7 
     8 
     9 section {* Modules over an Abelian Group *}
    10 
    11 subsection {* Definitions *}
    12 
    13 record ('a, 'b) module = "'b ring" +
    14   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
    15 
    16 locale module = R: cring + M: abelian_group M for M (structure) +
    17   assumes smult_closed [simp, intro]:
    18       "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    19     and smult_l_distr:
    20       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    21       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"
    22     and smult_r_distr:
    23       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    24       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"
    25     and smult_assoc1:
    26       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    27       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    28     and smult_one [simp]:
    29       "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
    30 
    31 locale algebra = module + cring M +
    32   assumes smult_assoc2:
    33       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    34       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    35 
    36 lemma moduleI:
    37   fixes R (structure) and M (structure)
    38   assumes cring: "cring R"
    39     and abelian_group: "abelian_group M"
    40     and smult_closed:
    41       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    42     and smult_l_distr:
    43       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    44       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    45     and smult_r_distr:
    46       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    47       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)"
    48     and smult_assoc1:
    49       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    50       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    51     and smult_one:
    52       "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
    53   shows "module R M"
    54   by (auto intro: module.intro cring.axioms abelian_group.axioms
    55     module_axioms.intro assms)
    56 
    57 lemma algebraI:
    58   fixes R (structure) and M (structure)
    59   assumes R_cring: "cring R"
    60     and M_cring: "cring M"
    61     and smult_closed:
    62       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    63     and smult_l_distr:
    64       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    65       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    66     and smult_r_distr:
    67       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    68       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)"
    69     and smult_assoc1:
    70       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    71       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    72     and smult_one:
    73       "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
    74     and smult_assoc2:
    75       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    76       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    77   shows "algebra R M"
    78 apply intro_locales
    79 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
    80 apply (rule module_axioms.intro)
    81  apply (simp add: smult_closed)
    82  apply (simp add: smult_l_distr)
    83  apply (simp add: smult_r_distr)
    84  apply (simp add: smult_assoc1)
    85  apply (simp add: smult_one)
    86 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
    87 apply (rule algebra_axioms.intro)
    88  apply (simp add: smult_assoc2)
    89 done
    90 
    91 lemma (in algebra) R_cring:
    92   "cring R"
    93   ..
    94 
    95 lemma (in algebra) M_cring:
    96   "cring M"
    97   ..
    98 
    99 lemma (in algebra) module:
   100   "module R M"
   101   by (auto intro: moduleI R_cring is_abelian_group
   102     smult_l_distr smult_r_distr smult_assoc1)
   103 
   104 
   105 subsection {* Basic Properties of Algebras *}
   106 
   107 lemma (in algebra) smult_l_null [simp]:
   108   "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
   109 proof -
   110   assume M: "x \<in> carrier M"
   111   note facts = M smult_closed [OF R.zero_closed]
   112   from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)" by algebra
   113   also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)"
   114     by (simp add: smult_l_distr del: R.l_zero R.r_zero)
   115   also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done
   116   finally show ?thesis .
   117 qed
   118 
   119 lemma (in algebra) smult_r_null [simp]:
   120   "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
   121 proof -
   122   assume R: "a \<in> carrier R"
   123   note facts = R smult_closed
   124   from facts have "a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
   125     by algebra
   126   also from R have "... = a \<odot>\<^bsub>M\<^esub> (\<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
   127     by (simp add: smult_r_distr del: M.l_zero M.r_zero)
   128   also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
   129   finally show ?thesis .
   130 qed
   131 
   132 lemma (in algebra) smult_l_minus:
   133   "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
   134 proof -
   135   assume RM: "a \<in> carrier R" "x \<in> carrier M"
   136   from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
   137   from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
   138   note facts = RM a_smult ma_smult
   139   from facts have "(\<ominus>a) \<odot>\<^bsub>M\<^esub> x = (\<ominus>a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   140     by algebra
   141   also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   142     by (simp add: smult_l_distr)
   143   also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   144     apply algebra apply algebra done
   145   finally show ?thesis .
   146 qed
   147 
   148 lemma (in algebra) smult_r_minus:
   149   "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
   150 proof -
   151   assume RM: "a \<in> carrier R" "x \<in> carrier M"
   152   note facts = RM smult_closed
   153   from facts have "a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = (a \<odot>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   154     by algebra
   155   also from RM have "... = a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   156     by (simp add: smult_r_distr)
   157   also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
   158   finally show ?thesis .
   159 qed
   160 
   161 end