1 (* Title: HOL/GroupTheory/Module |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
|
4 |
|
5 *) |
|
6 |
|
7 header{*Modules*} |
|
8 |
|
9 theory Module = Ring: |
|
10 |
|
11 text{*The record includes all the group components (carrier, sum, gminus, |
|
12 zero), adding the scalar product.*} |
|
13 record ('a,'b) module = "'a group" + |
|
14 sprod :: "'b \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<star>\<index>" 70) |
|
15 |
|
16 text{*The locale assumes all the properties of a ring and an Abelian group, |
|
17 adding laws relating them.*} |
|
18 locale module = ring R + abelian_group M + |
|
19 assumes sprod_funcset: "sprod M \<in> carrier R \<rightarrow> carrier M \<rightarrow> carrier M" |
|
20 and sprod_assoc: |
|
21 "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|] |
|
22 ==> (r \<cdot>\<^sub>1 s) \<star>\<^sub>2 a = r \<star>\<^sub>2 (s \<star>\<^sub>2 a)" |
|
23 and sprod_distrib_left: |
|
24 "[|r \<in> carrier R; a \<in> carrier M; b \<in> carrier M|] |
|
25 ==> r \<star>\<^sub>2 (a \<oplus>\<^sub>2 b) = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (r \<star>\<^sub>2 b)" |
|
26 and sprod_distrib_right: |
|
27 "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|] |
|
28 ==> (r \<oplus>\<^sub>1 s) \<star>\<^sub>2 a = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (s \<star>\<^sub>2 a)" |
|
29 |
|
30 lemma module_iff: |
|
31 "module R M = (ring R & abelian_group M & module_axioms R M)" |
|
32 by (simp add: module_def ring_def abelian_group_def) |
|
33 |
|
34 text{*The sum and product in @{text R} are @{text "r \<oplus>\<^sub>1 s"} and @{text |
|
35 "r \<cdot>\<^sub>1 s"}, respectively. The sum in @{text M} is @{text "a \<oplus>\<^sub>2 b"}.*} |
|
36 |
|
37 |
|
38 text{*We have to write the ring product as @{text "\<cdot>\<^sub>2"}. But if we |
|
39 refer to the scalar product as @{text "\<cdot>\<^sub>1"} then syntactic ambiguities |
|
40 arise. This presumably happens because the subscript merely determines which |
|
41 structure argument to insert, which happens after parsing. Better to use a |
|
42 different symbol such as @{text "\<star>"}*} |
|
43 |
|
44 subsection {*Trivial Example: Every Ring is an R-Module Over Itself *} |
|
45 |
|
46 constdefs |
|
47 triv_mod :: "('a,'b) ring_scheme => ('a,'a) module" |
|
48 "triv_mod R == (|carrier = carrier R, |
|
49 sum = sum R, |
|
50 gminus = gminus R, |
|
51 zero = zero R, |
|
52 sprod = prod R|)" |
|
53 |
|
54 theorem module_triv_mod: "ring R ==> module R (triv_mod R)" |
|
55 apply (simp add: triv_mod_def module_iff module_axioms_def |
|
56 ring_def ring_axioms_def abelian_group_def |
|
57 distrib_l_def distrib_r_def semigroup_def group_axioms_def) |
|
58 apply (simp add: abelian_group_axioms_def) |
|
59 --{*Combining the two simplifications causes looping!*} |
|
60 done |
|
61 |
|
62 end |
|