src/HOL/Algebra/Module.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 15095 63f5f4c265dd
child 19783 82f365a14960
permissions -rw-r--r--
migrated theory headers to new format
wenzelm@14706
     1
(*  Title:      HOL/Algebra/Module.thy
ballarin@13936
     2
    ID:         $Id$
ballarin@13936
     3
    Author:     Clemens Ballarin, started 15 April 2003
ballarin@13936
     4
    Copyright:  Clemens Ballarin
ballarin@13936
     5
*)
ballarin@13936
     6
wenzelm@14577
     7
header {* Modules over an Abelian Group *}
ballarin@13936
     8
haftmann@16417
     9
theory Module imports CRing begin
ballarin@13936
    10
ballarin@13936
    11
record ('a, 'b) module = "'b ring" +
ballarin@13936
    12
  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
ballarin@13936
    13
ballarin@13936
    14
locale module = cring R + abelian_group M +
ballarin@13936
    15
  assumes smult_closed [simp, intro]:
ballarin@15095
    16
      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
ballarin@13936
    17
    and smult_l_distr:
ballarin@13936
    18
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    19
      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"
ballarin@13936
    20
    and smult_r_distr:
ballarin@13936
    21
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    22
      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"
ballarin@13936
    23
    and smult_assoc1:
ballarin@13936
    24
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    25
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    26
    and smult_one [simp]:
ballarin@15095
    27
      "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
ballarin@13936
    28
ballarin@13936
    29
locale algebra = module R M + cring M +
ballarin@13936
    30
  assumes smult_assoc2:
ballarin@13936
    31
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    32
      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
ballarin@13936
    33
ballarin@13936
    34
lemma moduleI:
wenzelm@14651
    35
  includes struct R + struct M
ballarin@13936
    36
  assumes cring: "cring R"
ballarin@13936
    37
    and abelian_group: "abelian_group M"
ballarin@13936
    38
    and smult_closed:
ballarin@15095
    39
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
ballarin@13936
    40
    and smult_l_distr:
ballarin@13936
    41
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    42
      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    43
    and smult_r_distr:
ballarin@13936
    44
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    45
      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)"
ballarin@13936
    46
    and smult_assoc1:
ballarin@13936
    47
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    48
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    49
    and smult_one:
ballarin@15095
    50
      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
ballarin@13936
    51
  shows "module R M"
ballarin@13936
    52
  by (auto intro: module.intro cring.axioms abelian_group.axioms
ballarin@13936
    53
    module_axioms.intro prems)
ballarin@13936
    54
ballarin@13936
    55
lemma algebraI:
wenzelm@14651
    56
  includes struct R + struct M
ballarin@13936
    57
  assumes R_cring: "cring R"
ballarin@13936
    58
    and M_cring: "cring M"
ballarin@13936
    59
    and smult_closed:
ballarin@15095
    60
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
ballarin@13936
    61
    and smult_l_distr:
ballarin@13936
    62
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    63
      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    64
    and smult_r_distr:
ballarin@13936
    65
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    66
      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)"
ballarin@13936
    67
    and smult_assoc1:
ballarin@13936
    68
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    69
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    70
    and smult_one:
ballarin@15095
    71
      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
ballarin@13936
    72
    and smult_assoc2:
ballarin@13936
    73
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    74
      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
ballarin@13936
    75
  shows "algebra R M"
ballarin@13936
    76
  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
ballarin@13936
    77
    module_axioms.intro prems)
ballarin@13936
    78
ballarin@13936
    79
lemma (in algebra) R_cring:
ballarin@13936
    80
  "cring R"
wenzelm@14651
    81
  by (rule cring.intro)
ballarin@13936
    82
ballarin@13936
    83
lemma (in algebra) M_cring:
ballarin@13936
    84
  "cring M"
wenzelm@14651
    85
  by (rule cring.intro)
ballarin@13936
    86
ballarin@13936
    87
lemma (in algebra) module:
ballarin@13936
    88
  "module R M"
ballarin@13936
    89
  by (auto intro: moduleI R_cring is_abelian_group
ballarin@13936
    90
    smult_l_distr smult_r_distr smult_assoc1)
ballarin@13936
    91
wenzelm@14651
    92
ballarin@13936
    93
subsection {* Basic Properties of Algebras *}
ballarin@13936
    94
ballarin@13936
    95
lemma (in algebra) smult_l_null [simp]:
ballarin@15095
    96
  "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
ballarin@13936
    97
proof -
ballarin@13936
    98
  assume M: "x \<in> carrier M"
ballarin@13936
    99
  note facts = M smult_closed
ballarin@15095
   100
  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
ballarin@15095
   101
  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)"
ballarin@13936
   102
    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
ballarin@15095
   103
  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
ballarin@13936
   104
  finally show ?thesis .
ballarin@13936
   105
qed
ballarin@13936
   106
ballarin@13936
   107
lemma (in algebra) smult_r_null [simp]:
ballarin@15095
   108
  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
ballarin@13936
   109
proof -
ballarin@13936
   110
  assume R: "a \<in> carrier R"
ballarin@13936
   111
  note facts = R smult_closed
ballarin@15095
   112
  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>)"
ballarin@13936
   113
    by algebra
ballarin@15095
   114
  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>)"
ballarin@13936
   115
    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
ballarin@15095
   116
  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
ballarin@13936
   117
  finally show ?thesis .
ballarin@13936
   118
qed
ballarin@13936
   119
ballarin@13936
   120
lemma (in algebra) smult_l_minus:
ballarin@15095
   121
  "[| 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)"
ballarin@13936
   122
proof -
ballarin@13936
   123
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
ballarin@13936
   124
  note facts = RM smult_closed
ballarin@15095
   125
  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)"
ballarin@15095
   126
    by algebra
ballarin@15095
   127
  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)"
ballarin@13936
   128
    by (simp add: smult_l_distr)
ballarin@15095
   129
  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
ballarin@13936
   130
  finally show ?thesis .
ballarin@13936
   131
qed
ballarin@13936
   132
ballarin@13936
   133
lemma (in algebra) smult_r_minus:
ballarin@15095
   134
  "[| 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)"
ballarin@13936
   135
proof -
ballarin@13936
   136
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
ballarin@13936
   137
  note facts = RM smult_closed
ballarin@15095
   138
  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)"
ballarin@13936
   139
    by algebra
ballarin@15095
   140
  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)"
ballarin@13936
   141
    by (simp add: smult_r_distr)
ballarin@15095
   142
  also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
ballarin@13936
   143
  finally show ?thesis .
ballarin@13936
   144
qed
ballarin@13936
   145
ballarin@13936
   146
end