src/HOL/Algebra/Module.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 61565 352c73a689da
child 68552 391e89e03eef
permissions -rw-r--r--
More on Algebra by Paulo and Martin
wenzelm@14706
     1
(*  Title:      HOL/Algebra/Module.thy
ballarin@13936
     2
    Author:     Clemens Ballarin, started 15 April 2003
ballarin@13936
     3
    Copyright:  Clemens Ballarin
ballarin@13936
     4
*)
ballarin@13936
     5
wenzelm@35849
     6
theory Module
wenzelm@35849
     7
imports Ring
wenzelm@35849
     8
begin
ballarin@13936
     9
wenzelm@61382
    10
section \<open>Modules over an Abelian Group\<close>
ballarin@20318
    11
wenzelm@61382
    12
subsection \<open>Definitions\<close>
ballarin@13936
    13
ballarin@13936
    14
record ('a, 'b) module = "'b ring" +
ballarin@13936
    15
  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
ballarin@13936
    16
ballarin@61565
    17
locale module = R?: cring + M?: abelian_group M for M (structure) +
ballarin@13936
    18
  assumes smult_closed [simp, intro]:
ballarin@15095
    19
      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
ballarin@13936
    20
    and smult_l_distr:
ballarin@13936
    21
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    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"
ballarin@13936
    23
    and smult_r_distr:
ballarin@13936
    24
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    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"
ballarin@13936
    26
    and smult_assoc1:
ballarin@13936
    27
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    28
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    29
    and smult_one [simp]:
ballarin@15095
    30
      "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
ballarin@13936
    31
ballarin@29237
    32
locale algebra = module + cring M +
ballarin@13936
    33
  assumes smult_assoc2:
ballarin@13936
    34
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    35
      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
ballarin@13936
    36
ballarin@13936
    37
lemma moduleI:
ballarin@19783
    38
  fixes R (structure) and M (structure)
ballarin@13936
    39
  assumes cring: "cring R"
ballarin@13936
    40
    and abelian_group: "abelian_group M"
ballarin@13936
    41
    and smult_closed:
ballarin@15095
    42
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
ballarin@13936
    43
    and smult_l_distr:
ballarin@13936
    44
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    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)"
ballarin@13936
    46
    and smult_r_distr:
ballarin@13936
    47
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    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)"
ballarin@13936
    49
    and smult_assoc1:
ballarin@13936
    50
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    51
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    52
    and smult_one:
ballarin@15095
    53
      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
ballarin@13936
    54
  shows "module R M"
ballarin@13936
    55
  by (auto intro: module.intro cring.axioms abelian_group.axioms
ballarin@27714
    56
    module_axioms.intro assms)
ballarin@13936
    57
ballarin@13936
    58
lemma algebraI:
ballarin@19783
    59
  fixes R (structure) and M (structure)
ballarin@13936
    60
  assumes R_cring: "cring R"
ballarin@13936
    61
    and M_cring: "cring M"
ballarin@13936
    62
    and smult_closed:
ballarin@15095
    63
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
ballarin@13936
    64
    and smult_l_distr:
ballarin@13936
    65
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    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)"
ballarin@13936
    67
    and smult_r_distr:
ballarin@13936
    68
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    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)"
ballarin@13936
    70
    and smult_assoc1:
ballarin@13936
    71
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
ballarin@15095
    72
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
ballarin@13936
    73
    and smult_one:
ballarin@15095
    74
      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
ballarin@13936
    75
    and smult_assoc2:
ballarin@13936
    76
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
ballarin@15095
    77
      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
ballarin@13936
    78
  shows "algebra R M"
lp15@68551
    79
  apply intro_locales
lp15@68551
    80
             apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
lp15@68551
    81
      apply (rule module_axioms.intro)
lp15@68551
    82
          apply (simp add: smult_closed)
lp15@68551
    83
         apply (simp add: smult_l_distr)
lp15@68551
    84
        apply (simp add: smult_r_distr)
lp15@68551
    85
       apply (simp add: smult_assoc1)
lp15@68551
    86
      apply (simp add: smult_one)
lp15@68551
    87
     apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
lp15@68551
    88
  apply (rule algebra_axioms.intro)
lp15@68551
    89
  apply (simp add: smult_assoc2)
lp15@68551
    90
  done
ballarin@13936
    91
lp15@68551
    92
lemma (in algebra) R_cring: "cring R" ..
ballarin@13936
    93
lp15@68551
    94
lemma (in algebra) M_cring: "cring M" ..
ballarin@13936
    95
lp15@68551
    96
lemma (in algebra) module: "module R M"
lp15@68551
    97
  by (auto intro: moduleI R_cring is_abelian_group smult_l_distr smult_r_distr smult_assoc1)
ballarin@13936
    98
wenzelm@14651
    99
lp15@68551
   100
subsection \<open>Basic Properties of Modules\<close>
ballarin@13936
   101
lp15@68551
   102
lemma (in module) smult_l_null [simp]:
lp15@68551
   103
 "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
lp15@68551
   104
proof-
lp15@68551
   105
  assume M : "x \<in> carrier M"
ballarin@20168
   106
  note facts = M smult_closed [OF R.zero_closed]
lp15@68551
   107
  from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x "
lp15@68551
   108
    using smult_l_distr by auto
lp15@68551
   109
  also have "... = \<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x"
lp15@68551
   110
    using smult_l_distr[of \<zero> \<zero> x] facts by auto
lp15@68551
   111
  finally show "\<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>" using facts
lp15@68551
   112
    by (metis M.add.r_cancel_one')
ballarin@13936
   113
qed
ballarin@13936
   114
lp15@68551
   115
lemma (in module) smult_r_null [simp]:
wenzelm@58860
   116
  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
ballarin@13936
   117
proof -
ballarin@13936
   118
  assume R: "a \<in> carrier R"
ballarin@13936
   119
  note facts = R smult_closed
ballarin@15095
   120
  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>)"
lp15@68551
   121
    by (simp add: M.add.inv_solve_right)
ballarin@15095
   122
  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
   123
    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
lp15@68551
   124
  also from facts have "... = \<zero>\<^bsub>M\<^esub>"
lp15@68551
   125
    by (simp add: M.r_neg)
ballarin@13936
   126
  finally show ?thesis .
ballarin@13936
   127
qed
ballarin@13936
   128
lp15@68551
   129
lemma (in module) smult_l_minus:
lp15@68551
   130
"\<lbrakk> a \<in> carrier R; x \<in> carrier M \<rbrakk> \<Longrightarrow> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
lp15@68551
   131
proof-
ballarin@13936
   132
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
ballarin@20168
   133
  from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
ballarin@20168
   134
  from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
ballarin@20168
   135
  note facts = RM a_smult ma_smult
ballarin@15095
   136
  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)"
lp15@68551
   137
    by (simp add: M.add.inv_solve_right)
ballarin@15095
   138
  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
   139
    by (simp add: smult_l_distr)
ballarin@20168
   140
  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
lp15@68551
   141
    by (simp add: R.l_neg)
ballarin@13936
   142
  finally show ?thesis .
ballarin@13936
   143
qed
ballarin@13936
   144
lp15@68551
   145
lemma (in module) smult_r_minus:
ballarin@15095
   146
  "[| 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
   147
proof -
ballarin@13936
   148
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
ballarin@13936
   149
  note facts = RM smult_closed
ballarin@15095
   150
  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)"
lp15@68551
   151
    by (simp add: M.add.inv_solve_right)
ballarin@15095
   152
  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
   153
    by (simp add: smult_r_distr)
lp15@68551
   154
  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
lp15@68551
   155
    by (metis M.add.inv_closed M.add.inv_solve_right M.l_neg R.zero_closed r_null smult_assoc1)
ballarin@13936
   156
  finally show ?thesis .
ballarin@13936
   157
qed
ballarin@13936
   158
lp15@68551
   159
lemma (in module) finsum_smult_ldistr:
lp15@68551
   160
  "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier M \<rbrakk> \<Longrightarrow>
lp15@68551
   161
     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)))"
lp15@68551
   162
proof (induct set: finite)
lp15@68551
   163
  case empty then show ?case
lp15@68551
   164
    by (metis M.finsum_empty M.zero_closed R.zero_closed r_null smult_assoc1 smult_l_null)
lp15@68551
   165
next
lp15@68551
   166
  case (insert x F) then show ?case
lp15@68551
   167
    by (simp add: Pi_def smult_r_distr)
lp15@68551
   168
qed
lp15@68551
   169
ballarin@13936
   170
end