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