author | wenzelm |
Wed, 13 Jun 2007 00:01:41 +0200 | |
changeset 23350 | 50c5b0912a0c |
parent 21502 | 7f3ea2b3bab6 |
child 23463 | 9953ff53cc64 |
permissions | -rw-r--r-- |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
1 |
(* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
2 |
Title: HOL/Algebra/QuotRing.thy |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
3 |
Id: $Id$ |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
4 |
Author: Stephan Hohe |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
5 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
6 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
7 |
theory QuotRing |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
8 |
imports RingHom |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
9 |
begin |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
10 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
11 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
12 |
section {* Quotient Rings *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
13 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
14 |
subsection {* Multiplication on Cosets *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
15 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
16 |
constdefs (structure R) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
17 |
rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set" ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
18 |
"rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
19 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
20 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
21 |
text {* @{const "rcoset_mult"} fulfils the properties required by |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
22 |
congruences *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
23 |
lemma (in ideal) rcoset_mult_add: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
24 |
"\<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
25 |
apply rule |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
26 |
apply (rule, simp add: rcoset_mult_def, clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
28 |
apply (rule, simp add: rcoset_mult_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
29 |
defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
30 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
31 |
fix z x' y' |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
32 |
assume carr: "x \<in> carrier R" "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
33 |
and x'rcos: "x' \<in> I +> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
34 |
and y'rcos: "y' \<in> I +> y" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
35 |
and zrcos: "z \<in> I +> x' \<otimes> y'" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
36 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
37 |
from x'rcos |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
38 |
have "\<exists>h\<in>I. x' = h \<oplus> x" by (simp add: a_r_coset_def r_coset_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
39 |
from this obtain hx |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
40 |
where hxI: "hx \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
41 |
and x': "x' = hx \<oplus> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
42 |
by fast+ |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
43 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
44 |
from y'rcos |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
45 |
have "\<exists>h\<in>I. y' = h \<oplus> y" by (simp add: a_r_coset_def r_coset_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
46 |
from this |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
47 |
obtain hy |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
48 |
where hyI: "hy \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
49 |
and y': "y' = hy \<oplus> y" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
50 |
by fast+ |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
51 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
52 |
from zrcos |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
53 |
have "\<exists>h\<in>I. z = h \<oplus> (x' \<otimes> y')" by (simp add: a_r_coset_def r_coset_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
54 |
from this |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
55 |
obtain hz |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
56 |
where hzI: "hz \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
57 |
and z: "z = hz \<oplus> (x' \<otimes> y')" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
58 |
by fast+ |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
59 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
60 |
note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
61 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
62 |
from z have "z = hz \<oplus> (x' \<otimes> y')" . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
63 |
also from x' y' |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
64 |
have "\<dots> = hz \<oplus> ((hx \<oplus> x) \<otimes> (hy \<oplus> y))" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
65 |
also from carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
66 |
have "\<dots> = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" by algebra |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
67 |
finally |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
68 |
have z2: "z = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
69 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
70 |
from hxI hyI hzI carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
71 |
have "hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy \<in> I" by (simp add: I_l_closed I_r_closed) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
72 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
73 |
from this and z2 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
74 |
have "\<exists>h\<in>I. z = h \<oplus> x \<otimes> y" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
75 |
thus "z \<in> I +> x \<otimes> y" by (simp add: a_r_coset_def r_coset_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
76 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
77 |
fix z |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
78 |
assume xcarr: "x \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
79 |
and ycarr: "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
80 |
and zrcos: "z \<in> I +> x \<otimes> y" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
81 |
from xcarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
82 |
have xself: "x \<in> I +> x" by (intro a_rcos_self) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
83 |
from ycarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
84 |
have yself: "y \<in> I +> y" by (intro a_rcos_self) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
85 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
86 |
from xself and yself and zrcos |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
87 |
show "\<exists>a\<in>I +> x. \<exists>b\<in>I +> y. z \<in> I +> a \<otimes> b" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
88 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
89 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
90 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
91 |
subsection {* Quotient Ring Definition *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
92 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
93 |
constdefs (structure R) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
94 |
FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
95 |
(infixl "Quot" 65) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
96 |
"FactRing R I \<equiv> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
97 |
\<lparr>carrier = a_rcosets I, mult = rcoset_mult R I, one = (I +> \<one>), zero = I, add = set_add R\<rparr>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
98 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
99 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
100 |
subsection {* Factorization over General Ideals *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
101 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
102 |
text {* The quotient is a ring *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
103 |
lemma (in ideal) quotient_is_ring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
104 |
shows "ring (R Quot I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
105 |
apply (rule ringI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
106 |
--{* abelian group *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
107 |
apply (rule comm_group_abelian_groupI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
108 |
apply (simp add: FactRing_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
109 |
apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def']) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
110 |
--{* mult monoid *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
111 |
apply (rule monoidI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
112 |
apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
113 |
a_r_coset_def[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
114 |
--{* mult closed *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
115 |
apply (clarify) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
116 |
apply (simp add: rcoset_mult_add, fast) |
21502 | 117 |
--{* mult @{text one_closed} *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
118 |
apply (force intro: one_closed) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
119 |
--{* mult assoc *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
120 |
apply clarify |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
121 |
apply (simp add: rcoset_mult_add m_assoc) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
122 |
--{* mult one *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
123 |
apply clarify |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
124 |
apply (simp add: rcoset_mult_add l_one) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
125 |
apply clarify |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
126 |
apply (simp add: rcoset_mult_add r_one) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
127 |
--{* distr *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
128 |
apply clarify |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
129 |
apply (simp add: rcoset_mult_add a_rcos_sum l_distr) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
130 |
apply clarify |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
131 |
apply (simp add: rcoset_mult_add a_rcos_sum r_distr) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
132 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
133 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
134 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
135 |
text {* This is a ring homomorphism *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
136 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
137 |
lemma (in ideal) rcos_ring_hom: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
138 |
"(op +> I) \<in> ring_hom R (R Quot I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
139 |
apply (rule ring_hom_memI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
140 |
apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
141 |
apply (simp add: FactRing_def rcoset_mult_add) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
142 |
apply (simp add: FactRing_def a_rcos_sum) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
143 |
apply (simp add: FactRing_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
144 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
145 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
146 |
lemma (in ideal) rcos_ring_hom_ring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
147 |
"ring_hom_ring R (R Quot I) (op +> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
148 |
apply (rule ring_hom_ringI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
149 |
apply (rule is_ring, rule quotient_is_ring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
150 |
apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
151 |
apply (simp add: FactRing_def rcoset_mult_add) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
152 |
apply (simp add: FactRing_def a_rcos_sum) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
153 |
apply (simp add: FactRing_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
154 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
155 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
156 |
text {* The quotient of a cring is also commutative *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
157 |
lemma (in ideal) quotient_is_cring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
158 |
includes cring |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
159 |
shows "cring (R Quot I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
160 |
apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
161 |
apply (rule quotient_is_ring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
162 |
apply (rule ring.axioms[OF quotient_is_ring]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
163 |
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
164 |
apply clarify |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
165 |
apply (simp add: rcoset_mult_add m_comm) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
166 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
167 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
168 |
text {* Cosets as a ring homomorphism on crings *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
169 |
lemma (in ideal) rcos_ring_hom_cring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
170 |
includes cring |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
171 |
shows "ring_hom_cring R (R Quot I) (op +> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
172 |
apply (rule ring_hom_cringI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
173 |
apply (rule rcos_ring_hom_ring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
174 |
apply assumption |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
175 |
apply (rule quotient_is_cring, assumption) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
176 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
177 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
178 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
179 |
subsection {* Factorization over Prime Ideals *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
180 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
181 |
text {* The quotient ring generated by a prime ideal is a domain *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
182 |
lemma (in primeideal) quotient_is_domain: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
183 |
shows "domain (R Quot I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
184 |
apply (rule domain.intro) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
185 |
apply (rule quotient_is_cring, rule is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
186 |
apply (rule domain_axioms.intro) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
187 |
apply (simp add: FactRing_def) defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
188 |
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
189 |
apply (simp add: rcoset_mult_add) defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
190 |
proof (rule ccontr, clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
191 |
assume "I +> \<one> = I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
192 |
hence "\<one> \<in> I" by (simp only: a_coset_join1 one_closed a_subgroup) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
193 |
hence "carrier R \<subseteq> I" by (subst one_imp_carrier, simp, fast) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
194 |
from this and a_subset |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
195 |
have "I = carrier R" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
196 |
from this and I_notcarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
197 |
show "False" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
198 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
199 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
200 |
assume carr: "x \<in> carrier R" "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
201 |
and a: "I +> x \<otimes> y = I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
202 |
and b: "I +> y \<noteq> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
203 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
204 |
have ynI: "y \<notin> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
205 |
proof (rule ccontr, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
206 |
assume "y \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
207 |
hence "I +> y = I" by (rule a_rcos_const) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
208 |
from this and b |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
209 |
show "False" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
210 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
211 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
212 |
from carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
213 |
have "x \<otimes> y \<in> I +> x \<otimes> y" by (simp add: a_rcos_self) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
214 |
from this |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
215 |
have xyI: "x \<otimes> y \<in> I" by (simp add: a) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
216 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
217 |
from xyI and carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
218 |
have xI: "x \<in> I \<or> y \<in> I" by (simp add: I_prime) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
219 |
from this and ynI |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
220 |
have "x \<in> I" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
221 |
thus "I +> x = I" by (rule a_rcos_const) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
222 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
223 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
224 |
text {* Generating right cosets of a prime ideal is a homomorphism |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
225 |
on commutative rings *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
226 |
lemma (in primeideal) rcos_ring_hom_cring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
227 |
shows "ring_hom_cring R (R Quot I) (op +> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
228 |
by (rule rcos_ring_hom_cring, rule is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
229 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
230 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
subsection {* Factorization over Maximal Ideals *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
232 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
233 |
text {* In a commutative ring, the quotient ring over a maximal ideal |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
is a field. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
235 |
The proof follows ``W. Adkins, S. Weintraub: Algebra -- |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
236 |
An Approach via Module Theory'' *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
237 |
lemma (in maximalideal) quotient_is_field: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
238 |
includes cring |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
239 |
shows "field (R Quot I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
240 |
apply (intro cring.cring_fieldI2) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
241 |
apply (rule quotient_is_cring, rule is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
242 |
defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
243 |
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
244 |
apply (simp add: rcoset_mult_add) defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
245 |
proof (rule ccontr, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
246 |
--{* Quotient is not empty *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
247 |
assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
248 |
hence II1: "I = I +> \<one>" by (simp add: FactRing_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
249 |
from a_rcos_self[OF one_closed] |
23350 | 250 |
have "\<one> \<in> I" by (simp add: II1[symmetric]) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
251 |
hence "I = carrier R" by (rule one_imp_carrier) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
252 |
from this and I_notcarr |
23350 | 253 |
show "False" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
254 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
255 |
--{* Existence of Inverse *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
256 |
fix a |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
assume IanI: "I +> a \<noteq> I" |
23350 | 258 |
and acarr: "a \<in> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
259 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
260 |
--{* Helper ideal @{text "J"} *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
261 |
def J \<equiv> "(carrier R #> a) <+> I :: 'a set" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
have idealJ: "ideal J R" |
23350 | 263 |
apply (unfold J_def, rule add_ideals) |
264 |
apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr) |
|
265 |
apply (rule is_ideal) |
|
266 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
267 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
268 |
--{* Showing @{term "J"} not smaller than @{term "I"} *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
269 |
have IinJ: "I \<subseteq> J" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
270 |
proof (rule, simp add: J_def r_coset_def set_add_defs) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
271 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
272 |
assume xI: "x \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
273 |
have Zcarr: "\<zero> \<in> carrier R" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
274 |
from xI[THEN a_Hcarr] acarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
275 |
have "x = \<zero> \<otimes> a \<oplus> x" by algebra |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
276 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
277 |
from Zcarr and xI and this |
23350 | 278 |
show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
279 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
280 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
281 |
--{* Showing @{term "J \<noteq> I"} *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
282 |
have anI: "a \<notin> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
283 |
proof (rule ccontr, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
284 |
assume "a \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
285 |
hence "I +> a = I" by (rule a_rcos_const) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
286 |
from this and IanI |
23350 | 287 |
show "False" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
288 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
289 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
290 |
have aJ: "a \<in> J" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
291 |
proof (simp add: J_def r_coset_def set_add_defs) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
292 |
from acarr |
23350 | 293 |
have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
from one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] and this |
23350 | 295 |
show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
297 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
298 |
from aJ and anI |
23350 | 299 |
have JnI: "J \<noteq> I" by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
301 |
--{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
302 |
from idealJ and IinJ |
23350 | 303 |
have "J = I \<or> J = carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
304 |
proof (rule I_maximal, unfold J_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
305 |
have "carrier R #> a \<subseteq> carrier R" |
23350 | 306 |
using subset_refl acarr |
307 |
by (rule r_coset_subset_G) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
308 |
from this and a_subset |
23350 | 309 |
show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
310 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
311 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
312 |
from this and JnI |
23350 | 313 |
have Jcarr: "J = carrier R" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
315 |
--{* Calculating an inverse for @{term "a"} *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
316 |
from one_closed[folded Jcarr] |
23350 | 317 |
have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i" |
318 |
by (simp add: J_def r_coset_def set_add_defs) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
319 |
from this |
23350 | 320 |
obtain r i |
321 |
where rcarr: "r \<in> carrier R" |
|
322 |
and iI: "i \<in> I" |
|
323 |
and one: "\<one> = r \<otimes> a \<oplus> i" |
|
324 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
from one and rcarr and acarr and iI[THEN a_Hcarr] |
23350 | 326 |
have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
327 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
328 |
--{* Lifting to cosets *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
329 |
from iI |
23350 | 330 |
have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>" |
331 |
by (intro a_rcosI, simp, intro a_subset, simp) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
332 |
from this and rai1 |
23350 | 333 |
have "a \<otimes> r \<in> I +> \<one>" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
from this have "I +> \<one> = I +> a \<otimes> r" |
23350 | 335 |
by (rule a_repr_independence, simp) (rule a_subgroup) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
336 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
337 |
from rcarr and this[symmetric] |
23350 | 338 |
show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
340 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
341 |
end |