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