src/HOL/Algebra/Module.thy
author ballarin
Mon May 05 10:53:27 2003 +0200 (2003-05-05)
changeset 13952 6206d3e7672a
parent 13949 0ce528cd6f19
child 13975 c8e9a89883ce
permissions -rw-r--r--
Fixed but with old versions of pdflatex (fancy symbols not allowed in bookmarks).
ballarin@13936
     1
(*  Title:      HOL/Algebra/Module
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
ballarin@13936
     7
theory Module = CRing:
ballarin@13936
     8
ballarin@13936
     9
section {* Modules over an Abelian Group *}
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@13936
    16
      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 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@13936
    19
      (a \<oplus> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
ballarin@13936
    20
    and smult_r_distr:
ballarin@13936
    21
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@13936
    22
      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
ballarin@13936
    23
    and smult_assoc1:
ballarin@13936
    24
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@13936
    25
      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
ballarin@13936
    26
    and smult_one [simp]:
ballarin@13936
    27
      "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 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@13936
    32
      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
ballarin@13936
    33
ballarin@13936
    34
lemma moduleI:
ballarin@13936
    35
  assumes cring: "cring R"
ballarin@13936
    36
    and abelian_group: "abelian_group M"
ballarin@13936
    37
    and smult_closed:
ballarin@13936
    38
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
ballarin@13936
    39
    and smult_l_distr:
ballarin@13936
    40
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@13936
    41
      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
ballarin@13936
    42
    and smult_r_distr:
ballarin@13936
    43
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@13936
    44
      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
ballarin@13936
    45
    and smult_assoc1:
ballarin@13936
    46
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@13936
    47
      smult M (mult R a b) x = smult M a (smult M b x)"
ballarin@13936
    48
    and smult_one:
ballarin@13936
    49
      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
ballarin@13936
    50
  shows "module R M"
ballarin@13936
    51
  by (auto intro: module.intro cring.axioms abelian_group.axioms
ballarin@13936
    52
    module_axioms.intro prems)
ballarin@13936
    53
ballarin@13936
    54
lemma algebraI:
ballarin@13936
    55
  assumes R_cring: "cring R"
ballarin@13936
    56
    and M_cring: "cring M"
ballarin@13936
    57
    and smult_closed:
ballarin@13936
    58
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
ballarin@13936
    59
    and smult_l_distr:
ballarin@13936
    60
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@13936
    61
      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
ballarin@13936
    62
    and smult_r_distr:
ballarin@13936
    63
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@13936
    64
      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
ballarin@13936
    65
    and smult_assoc1:
ballarin@13936
    66
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@13936
    67
      smult M (mult R a b) x = smult M a (smult M b x)"
ballarin@13936
    68
    and smult_one:
ballarin@13936
    69
      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
ballarin@13936
    70
    and smult_assoc2:
ballarin@13936
    71
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@13936
    72
      mult M (smult M a x) y = smult M a (mult M x y)"
ballarin@13936
    73
  shows "algebra R M"
ballarin@13936
    74
  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
ballarin@13936
    75
    module_axioms.intro prems)
ballarin@13936
    76
ballarin@13936
    77
lemma (in algebra) R_cring:
ballarin@13936
    78
  "cring R"
ballarin@13936
    79
  by (rule cring.intro) assumption+
ballarin@13936
    80
ballarin@13936
    81
lemma (in algebra) M_cring:
ballarin@13936
    82
  "cring M"
ballarin@13936
    83
  by (rule cring.intro) assumption+
ballarin@13936
    84
ballarin@13936
    85
lemma (in algebra) module:
ballarin@13936
    86
  "module R M"
ballarin@13936
    87
  by (auto intro: moduleI R_cring is_abelian_group
ballarin@13936
    88
    smult_l_distr smult_r_distr smult_assoc1)
ballarin@13936
    89
ballarin@13936
    90
subsection {* Basic Properties of Algebras *}
ballarin@13936
    91
ballarin@13936
    92
lemma (in algebra) smult_l_null [simp]:
ballarin@13936
    93
  "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
ballarin@13936
    94
proof -
ballarin@13936
    95
  assume M: "x \<in> carrier M"
ballarin@13936
    96
  note facts = M smult_closed
ballarin@13936
    97
  from facts have "\<zero> \<odot>\<^sub>2 x = (\<zero> \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<zero> \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)" by algebra
ballarin@13936
    98
  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
ballarin@13936
    99
    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
ballarin@13936
   100
  also from facts have "... = \<zero>\<^sub>2" by algebra
ballarin@13936
   101
  finally show ?thesis .
ballarin@13936
   102
qed
ballarin@13936
   103
ballarin@13936
   104
lemma (in algebra) smult_r_null [simp]:
ballarin@13936
   105
  "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
ballarin@13936
   106
proof -
ballarin@13936
   107
  assume R: "a \<in> carrier R"
ballarin@13936
   108
  note facts = R smult_closed
ballarin@13936
   109
  from facts have "a \<odot>\<^sub>2 \<zero>\<^sub>2 = (a \<odot>\<^sub>2 \<zero>\<^sub>2 \<oplus>\<^sub>2 a \<odot>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
ballarin@13936
   110
    by algebra
ballarin@13936
   111
  also from R have "... = a \<odot>\<^sub>2 (\<zero>\<^sub>2 \<oplus>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
ballarin@13936
   112
    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
ballarin@13936
   113
  also from facts have "... = \<zero>\<^sub>2" by algebra
ballarin@13936
   114
  finally show ?thesis .
ballarin@13936
   115
qed
ballarin@13936
   116
ballarin@13936
   117
lemma (in algebra) smult_l_minus:
ballarin@13936
   118
  "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^sub>2 x = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
ballarin@13936
   119
proof -
ballarin@13936
   120
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
ballarin@13936
   121
  note facts = RM smult_closed
ballarin@13936
   122
  from facts have "(\<ominus>a) \<odot>\<^sub>2 x = (\<ominus>a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
ballarin@13936
   123
  also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
ballarin@13936
   124
    by (simp add: smult_l_distr)
ballarin@13936
   125
  also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
ballarin@13936
   126
  finally show ?thesis .
ballarin@13936
   127
qed
ballarin@13936
   128
ballarin@13936
   129
lemma (in algebra) smult_r_minus:
ballarin@13936
   130
  "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
ballarin@13936
   131
proof -
ballarin@13936
   132
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
ballarin@13936
   133
  note facts = RM smult_closed
ballarin@13936
   134
  from facts have "a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = (a \<odot>\<^sub>2 \<ominus>\<^sub>2x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
ballarin@13936
   135
    by algebra
ballarin@13936
   136
  also from RM have "... = a \<odot>\<^sub>2 (\<ominus>\<^sub>2x \<oplus>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
ballarin@13936
   137
    by (simp add: smult_r_distr)
ballarin@13936
   138
  also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
ballarin@13936
   139
  finally show ?thesis .
ballarin@13936
   140
qed
ballarin@13936
   141
ballarin@13952
   142
subsection {* Every Abelian Group is a Z-module *}
ballarin@13952
   143
ballarin@13952
   144
(* Not all versions of pdflatex permit $\mathbb{Z}$ in bookmarks. *)
ballarin@13936
   145
ballarin@13936
   146
text {* Not finished. *}
ballarin@13936
   147
ballarin@13936
   148
constdefs
ballarin@13936
   149
  INTEG :: "int ring"
ballarin@13936
   150
  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
ballarin@13936
   151
ballarin@13936
   152
(*
ballarin@13936
   153
  INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
ballarin@13936
   154
  "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
ballarin@13936
   155
    zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
ballarin@13936
   156
*)
ballarin@13936
   157
ballarin@13936
   158
lemma cring_INTEG:
ballarin@13936
   159
  "cring INTEG"
ballarin@13936
   160
  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
ballarin@13936
   161
    zadd_zminus_inverse2 zadd_zmult_distrib)
ballarin@13936
   162
ballarin@13936
   163
end