src/HOL/Algebra/QuotRing.thy
 author wenzelm Tue Jul 03 11:00:37 2018 +0200 (13 months ago) changeset 68582 b9b9e2985878 parent 68551 b680e74eb6f2 child 68584 ec4fe1032b6e permissions -rw-r--r--
 wenzelm@35849 ` 1` ```(* Title: HOL/Algebra/QuotRing.thy ``` wenzelm@35849 ` 2` ``` Author: Stephan Hohe ``` lp15@68551 ` 3` ``` Author: Paulo EmÃ­lio de Vilhena ``` ballarin@20318 ` 4` ```*) ``` ballarin@20318 ` 5` ballarin@20318 ` 6` ```theory QuotRing ``` ballarin@20318 ` 7` ```imports RingHom ``` ballarin@20318 ` 8` ```begin ``` ballarin@20318 ` 9` wenzelm@61382 ` 10` ```section \Quotient Rings\ ``` ballarin@27717 ` 11` wenzelm@61382 ` 12` ```subsection \Multiplication on Cosets\ ``` ballarin@20318 ` 13` wenzelm@45005 ` 14` ```definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \ 'a set" ``` wenzelm@23463 ` 15` ``` ("[mod _:] _ \\ _" [81,81,81] 80) ``` wenzelm@35848 ` 16` ``` where "rcoset_mult R I A B = (\a\A. \b\B. I +>\<^bsub>R\<^esub> (a \\<^bsub>R\<^esub> b))" ``` ballarin@20318 ` 17` ballarin@20318 ` 18` wenzelm@61382 ` 19` ```text \@{const "rcoset_mult"} fulfils the properties required by ``` wenzelm@61382 ` 20` ``` congruences\ ``` ballarin@20318 ` 21` ```lemma (in ideal) rcoset_mult_add: ``` wenzelm@45005 ` 22` ``` "x \ carrier R \ y \ carrier R \ [mod I:] (I +> x) \ (I +> y) = I +> (x \ y)" ``` wenzelm@45005 ` 23` ``` apply rule ``` wenzelm@45005 ` 24` ``` apply (rule, simp add: rcoset_mult_def, clarsimp) ``` wenzelm@45005 ` 25` ``` defer 1 ``` wenzelm@45005 ` 26` ``` apply (rule, simp add: rcoset_mult_def) ``` wenzelm@45005 ` 27` ``` defer 1 ``` ballarin@20318 ` 28` ```proof - ``` ballarin@20318 ` 29` ``` fix z x' y' ``` ballarin@20318 ` 30` ``` assume carr: "x \ carrier R" "y \ carrier R" ``` wenzelm@45005 ` 31` ``` and x'rcos: "x' \ I +> x" ``` wenzelm@45005 ` 32` ``` and y'rcos: "y' \ I +> y" ``` wenzelm@45005 ` 33` ``` and zrcos: "z \ I +> x' \ y'" ``` wenzelm@45005 ` 34` wenzelm@45005 ` 35` ``` from x'rcos have "\h\I. x' = h \ x" ``` wenzelm@45005 ` 36` ``` by (simp add: a_r_coset_def r_coset_def) ``` wenzelm@45005 ` 37` ``` then obtain hx where hxI: "hx \ I" and x': "x' = hx \ x" ``` wenzelm@45005 ` 38` ``` by fast+ ``` ballarin@20318 ` 39` wenzelm@45005 ` 40` ``` from y'rcos have "\h\I. y' = h \ y" ``` wenzelm@45005 ` 41` ``` by (simp add: a_r_coset_def r_coset_def) ``` wenzelm@45005 ` 42` ``` then obtain hy where hyI: "hy \ I" and y': "y' = hy \ y" ``` wenzelm@45005 ` 43` ``` by fast+ ``` ballarin@20318 ` 44` wenzelm@45005 ` 45` ``` from zrcos have "\h\I. z = h \ (x' \ y')" ``` wenzelm@45005 ` 46` ``` by (simp add: a_r_coset_def r_coset_def) ``` wenzelm@45005 ` 47` ``` then obtain hz where hzI: "hz \ I" and z: "z = hz \ (x' \ y')" ``` wenzelm@45005 ` 48` ``` by fast+ ``` ballarin@20318 ` 49` ballarin@20318 ` 50` ``` note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr] ``` ballarin@20318 ` 51` ballarin@20318 ` 52` ``` from z have "z = hz \ (x' \ y')" . ``` wenzelm@45005 ` 53` ``` also from x' y' have "\ = hz \ ((hx \ x) \ (hy \ y))" by simp ``` wenzelm@45005 ` 54` ``` also from carr have "\ = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" by algebra ``` wenzelm@45005 ` 55` ``` finally have z2: "z = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" . ``` ballarin@20318 ` 56` wenzelm@45005 ` 57` ``` from hxI hyI hzI carr have "hz \ (hx \ (hy \ y)) \ x \ hy \ I" ``` wenzelm@45005 ` 58` ``` by (simp add: I_l_closed I_r_closed) ``` ballarin@20318 ` 59` wenzelm@45005 ` 60` ``` with z2 have "\h\I. z = h \ x \ y" by fast ``` wenzelm@45005 ` 61` ``` then show "z \ I +> x \ y" by (simp add: a_r_coset_def r_coset_def) ``` ballarin@20318 ` 62` ```next ``` ballarin@20318 ` 63` ``` fix z ``` ballarin@20318 ` 64` ``` assume xcarr: "x \ carrier R" ``` wenzelm@45005 ` 65` ``` and ycarr: "y \ carrier R" ``` wenzelm@45005 ` 66` ``` and zrcos: "z \ I +> x \ y" ``` wenzelm@45005 ` 67` ``` from xcarr have xself: "x \ I +> x" by (intro a_rcos_self) ``` wenzelm@45005 ` 68` ``` from ycarr have yself: "y \ I +> y" by (intro a_rcos_self) ``` wenzelm@45005 ` 69` ``` show "\a\I +> x. \b\I +> y. z \ I +> a \ b" ``` wenzelm@45005 ` 70` ``` using xself and yself and zrcos by fast ``` ballarin@20318 ` 71` ```qed ``` ballarin@20318 ` 72` ballarin@20318 ` 73` wenzelm@61382 ` 74` ```subsection \Quotient Ring Definition\ ``` ballarin@20318 ` 75` wenzelm@45005 ` 76` ```definition FactRing :: "[('a,'b) ring_scheme, 'a set] \ ('a set) ring" ``` wenzelm@45005 ` 77` ``` (infixl "Quot" 65) ``` wenzelm@35848 ` 78` ``` where "FactRing R I = ``` wenzelm@45005 ` 79` ``` \carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, ``` wenzelm@45005 ` 80` ``` one = (I +>\<^bsub>R\<^esub> \\<^bsub>R\<^esub>), zero = I, add = set_add R\" ``` ballarin@20318 ` 81` ballarin@20318 ` 82` wenzelm@61382 ` 83` ```subsection \Factorization over General Ideals\ ``` ballarin@20318 ` 84` wenzelm@61382 ` 85` ```text \The quotient is a ring\ ``` wenzelm@45005 ` 86` ```lemma (in ideal) quotient_is_ring: "ring (R Quot I)" ``` ballarin@20318 ` 87` ```apply (rule ringI) ``` wenzelm@67443 ` 88` ``` \ \abelian group\ ``` ballarin@20318 ` 89` ``` apply (rule comm_group_abelian_groupI) ``` ballarin@20318 ` 90` ``` apply (simp add: FactRing_def) ``` ballarin@20318 ` 91` ``` apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def']) ``` wenzelm@67443 ` 92` ``` \ \mult monoid\ ``` ballarin@20318 ` 93` ``` apply (rule monoidI) ``` ballarin@20318 ` 94` ``` apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def ``` ballarin@20318 ` 95` ``` a_r_coset_def[symmetric]) ``` wenzelm@67443 ` 96` ``` \ \mult closed\ ``` ballarin@20318 ` 97` ``` apply (clarify) ``` ballarin@20318 ` 98` ``` apply (simp add: rcoset_mult_add, fast) ``` wenzelm@67443 ` 99` ``` \ \mult \one_closed\\ ``` wenzelm@45005 ` 100` ``` apply force ``` wenzelm@67443 ` 101` ``` \ \mult assoc\ ``` ballarin@20318 ` 102` ``` apply clarify ``` ballarin@20318 ` 103` ``` apply (simp add: rcoset_mult_add m_assoc) ``` wenzelm@67443 ` 104` ``` \ \mult one\ ``` ballarin@20318 ` 105` ``` apply clarify ``` wenzelm@45005 ` 106` ``` apply (simp add: rcoset_mult_add) ``` ballarin@20318 ` 107` ``` apply clarify ``` wenzelm@45005 ` 108` ``` apply (simp add: rcoset_mult_add) ``` wenzelm@67443 ` 109` ``` \ \distr\ ``` ballarin@20318 ` 110` ``` apply clarify ``` ballarin@20318 ` 111` ``` apply (simp add: rcoset_mult_add a_rcos_sum l_distr) ``` ballarin@20318 ` 112` ```apply clarify ``` ballarin@20318 ` 113` ```apply (simp add: rcoset_mult_add a_rcos_sum r_distr) ``` ballarin@20318 ` 114` ```done ``` ballarin@20318 ` 115` ballarin@20318 ` 116` wenzelm@61382 ` 117` ```text \This is a ring homomorphism\ ``` ballarin@20318 ` 118` nipkow@67399 ` 119` ```lemma (in ideal) rcos_ring_hom: "((+>) I) \ ring_hom R (R Quot I)" ``` ballarin@20318 ` 120` ```apply (rule ring_hom_memI) ``` ballarin@20318 ` 121` ``` apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) ``` ballarin@20318 ` 122` ``` apply (simp add: FactRing_def rcoset_mult_add) ``` ballarin@20318 ` 123` ``` apply (simp add: FactRing_def a_rcos_sum) ``` ballarin@20318 ` 124` ```apply (simp add: FactRing_def) ``` ballarin@20318 ` 125` ```done ``` ballarin@20318 ` 126` nipkow@67399 ` 127` ```lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) ((+>) I)" ``` ballarin@20318 ` 128` ```apply (rule ring_hom_ringI) ``` ballarin@20318 ` 129` ``` apply (rule is_ring, rule quotient_is_ring) ``` ballarin@20318 ` 130` ``` apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) ``` ballarin@20318 ` 131` ``` apply (simp add: FactRing_def rcoset_mult_add) ``` ballarin@20318 ` 132` ``` apply (simp add: FactRing_def a_rcos_sum) ``` ballarin@20318 ` 133` ```apply (simp add: FactRing_def) ``` ballarin@20318 ` 134` ```done ``` ballarin@20318 ` 135` wenzelm@61382 ` 136` ```text \The quotient of a cring is also commutative\ ``` ballarin@20318 ` 137` ```lemma (in ideal) quotient_is_cring: ``` ballarin@27611 ` 138` ``` assumes "cring R" ``` ballarin@20318 ` 139` ``` shows "cring (R Quot I)" ``` ballarin@27611 ` 140` ```proof - ``` ballarin@29237 ` 141` ``` interpret cring R by fact ``` wenzelm@45005 ` 142` ``` show ?thesis ``` wenzelm@45005 ` 143` ``` apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro) ``` wenzelm@45005 ` 144` ``` apply (rule quotient_is_ring) ``` wenzelm@45005 ` 145` ``` apply (rule ring.axioms[OF quotient_is_ring]) ``` wenzelm@45005 ` 146` ``` apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]) ``` wenzelm@45005 ` 147` ``` apply clarify ``` wenzelm@45005 ` 148` ``` apply (simp add: rcoset_mult_add m_comm) ``` wenzelm@45005 ` 149` ``` done ``` ballarin@27611 ` 150` ```qed ``` ballarin@20318 ` 151` wenzelm@61382 ` 152` ```text \Cosets as a ring homomorphism on crings\ ``` ballarin@20318 ` 153` ```lemma (in ideal) rcos_ring_hom_cring: ``` ballarin@27611 ` 154` ``` assumes "cring R" ``` nipkow@67399 ` 155` ``` shows "ring_hom_cring R (R Quot I) ((+>) I)" ``` ballarin@27611 ` 156` ```proof - ``` ballarin@29237 ` 157` ``` interpret cring R by fact ``` wenzelm@45005 ` 158` ``` show ?thesis ``` wenzelm@45005 ` 159` ``` apply (rule ring_hom_cringI) ``` wenzelm@45005 ` 160` ``` apply (rule rcos_ring_hom_ring) ``` wenzelm@45005 ` 161` ``` apply (rule is_cring) ``` wenzelm@45005 ` 162` ``` apply (rule quotient_is_cring) ``` wenzelm@45005 ` 163` ``` apply (rule is_cring) ``` wenzelm@45005 ` 164` ``` done ``` ballarin@27611 ` 165` ```qed ``` ballarin@20318 ` 166` wenzelm@35849 ` 167` wenzelm@61382 ` 168` ```subsection \Factorization over Prime Ideals\ ``` ballarin@20318 ` 169` wenzelm@61382 ` 170` ```text \The quotient ring generated by a prime ideal is a domain\ ``` wenzelm@45005 ` 171` ```lemma (in primeideal) quotient_is_domain: "domain (R Quot I)" ``` wenzelm@45005 ` 172` ``` apply (rule domain.intro) ``` wenzelm@45005 ` 173` ``` apply (rule quotient_is_cring, rule is_cring) ``` wenzelm@45005 ` 174` ``` apply (rule domain_axioms.intro) ``` wenzelm@45005 ` 175` ``` apply (simp add: FactRing_def) defer 1 ``` wenzelm@45005 ` 176` ``` apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify) ``` wenzelm@45005 ` 177` ``` apply (simp add: rcoset_mult_add) defer 1 ``` ballarin@20318 ` 178` ```proof (rule ccontr, clarsimp) ``` ballarin@20318 ` 179` ``` assume "I +> \ = I" ``` wenzelm@45005 ` 180` ``` then have "\ \ I" by (simp only: a_coset_join1 one_closed a_subgroup) ``` wenzelm@45005 ` 181` ``` then have "carrier R \ I" by (subst one_imp_carrier, simp, fast) ``` wenzelm@45005 ` 182` ``` with a_subset have "I = carrier R" by fast ``` wenzelm@45005 ` 183` ``` with I_notcarr show False by fast ``` ballarin@20318 ` 184` ```next ``` ballarin@20318 ` 185` ``` fix x y ``` ballarin@20318 ` 186` ``` assume carr: "x \ carrier R" "y \ carrier R" ``` wenzelm@45005 ` 187` ``` and a: "I +> x \ y = I" ``` wenzelm@45005 ` 188` ``` and b: "I +> y \ I" ``` ballarin@20318 ` 189` ballarin@20318 ` 190` ``` have ynI: "y \ I" ``` ballarin@20318 ` 191` ``` proof (rule ccontr, simp) ``` ballarin@20318 ` 192` ``` assume "y \ I" ``` wenzelm@45005 ` 193` ``` then have "I +> y = I" by (rule a_rcos_const) ``` wenzelm@45005 ` 194` ``` with b show False by simp ``` ballarin@20318 ` 195` ``` qed ``` ballarin@20318 ` 196` wenzelm@45005 ` 197` ``` from carr have "x \ y \ I +> x \ y" by (simp add: a_rcos_self) ``` wenzelm@45005 ` 198` ``` then have xyI: "x \ y \ I" by (simp add: a) ``` ballarin@20318 ` 199` wenzelm@45005 ` 200` ``` from xyI and carr have xI: "x \ I \ y \ I" by (simp add: I_prime) ``` wenzelm@45005 ` 201` ``` with ynI have "x \ I" by fast ``` wenzelm@45005 ` 202` ``` then show "I +> x = I" by (rule a_rcos_const) ``` ballarin@20318 ` 203` ```qed ``` ballarin@20318 ` 204` wenzelm@61382 ` 205` ```text \Generating right cosets of a prime ideal is a homomorphism ``` wenzelm@61382 ` 206` ``` on commutative rings\ ``` nipkow@67399 ` 207` ```lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) ((+>) I)" ``` wenzelm@45005 ` 208` ``` by (rule rcos_ring_hom_cring) (rule is_cring) ``` ballarin@20318 ` 209` ballarin@20318 ` 210` wenzelm@61382 ` 211` ```subsection \Factorization over Maximal Ideals\ ``` ballarin@20318 ` 212` wenzelm@61382 ` 213` ```text \In a commutative ring, the quotient ring over a maximal ideal ``` ballarin@20318 ` 214` ``` is a field. ``` ballarin@20318 ` 215` ``` The proof follows ``W. Adkins, S. Weintraub: Algebra -- ``` wenzelm@61382 ` 216` ``` An Approach via Module Theory''\ ``` ballarin@20318 ` 217` ```lemma (in maximalideal) quotient_is_field: ``` ballarin@27611 ` 218` ``` assumes "cring R" ``` ballarin@20318 ` 219` ``` shows "field (R Quot I)" ``` ballarin@27611 ` 220` ```proof - ``` ballarin@29237 ` 221` ``` interpret cring R by fact ``` wenzelm@45005 ` 222` ``` show ?thesis ``` wenzelm@45005 ` 223` ``` apply (intro cring.cring_fieldI2) ``` wenzelm@45005 ` 224` ``` apply (rule quotient_is_cring, rule is_cring) ``` wenzelm@45005 ` 225` ``` defer 1 ``` wenzelm@45005 ` 226` ``` apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp) ``` wenzelm@45005 ` 227` ``` apply (simp add: rcoset_mult_add) defer 1 ``` wenzelm@45005 ` 228` ``` proof (rule ccontr, simp) ``` wenzelm@67443 ` 229` ``` \ \Quotient is not empty\ ``` wenzelm@45005 ` 230` ``` assume "\\<^bsub>R Quot I\<^esub> = \\<^bsub>R Quot I\<^esub>" ``` wenzelm@45005 ` 231` ``` then have II1: "I = I +> \" by (simp add: FactRing_def) ``` wenzelm@45005 ` 232` ``` from a_rcos_self[OF one_closed] have "\ \ I" ``` wenzelm@45005 ` 233` ``` by (simp add: II1[symmetric]) ``` wenzelm@45005 ` 234` ``` then have "I = carrier R" by (rule one_imp_carrier) ``` wenzelm@45005 ` 235` ``` with I_notcarr show False by simp ``` wenzelm@45005 ` 236` ``` next ``` wenzelm@67443 ` 237` ``` \ \Existence of Inverse\ ``` wenzelm@45005 ` 238` ``` fix a ``` wenzelm@45005 ` 239` ``` assume IanI: "I +> a \ I" and acarr: "a \ carrier R" ``` ballarin@20318 ` 240` wenzelm@67443 ` 241` ``` \ \Helper ideal \J\\ ``` wenzelm@63040 ` 242` ``` define J :: "'a set" where "J = (carrier R #> a) <+> I" ``` wenzelm@45005 ` 243` ``` have idealJ: "ideal J R" ``` wenzelm@45005 ` 244` ``` apply (unfold J_def, rule add_ideals) ``` wenzelm@45005 ` 245` ``` apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr) ``` wenzelm@45005 ` 246` ``` apply (rule is_ideal) ``` wenzelm@45005 ` 247` ``` done ``` ballarin@20318 ` 248` wenzelm@67443 ` 249` ``` \ \Showing @{term "J"} not smaller than @{term "I"}\ ``` wenzelm@45005 ` 250` ``` have IinJ: "I \ J" ``` wenzelm@45005 ` 251` ``` proof (rule, simp add: J_def r_coset_def set_add_defs) ``` wenzelm@45005 ` 252` ``` fix x ``` wenzelm@45005 ` 253` ``` assume xI: "x \ I" ``` wenzelm@45005 ` 254` ``` have Zcarr: "\ \ carrier R" by fast ``` wenzelm@45005 ` 255` ``` from xI[THEN a_Hcarr] acarr ``` wenzelm@45005 ` 256` ``` have "x = \ \ a \ x" by algebra ``` wenzelm@45005 ` 257` ``` with Zcarr and xI show "\xa\carrier R. \k\I. x = xa \ a \ k" by fast ``` wenzelm@45005 ` 258` ``` qed ``` ballarin@20318 ` 259` wenzelm@67443 ` 260` ``` \ \Showing @{term "J \ I"}\ ``` wenzelm@45005 ` 261` ``` have anI: "a \ I" ``` wenzelm@45005 ` 262` ``` proof (rule ccontr, simp) ``` wenzelm@45005 ` 263` ``` assume "a \ I" ``` wenzelm@45005 ` 264` ``` then have "I +> a = I" by (rule a_rcos_const) ``` wenzelm@45005 ` 265` ``` with IanI show False by simp ``` wenzelm@45005 ` 266` ``` qed ``` ballarin@20318 ` 267` wenzelm@45005 ` 268` ``` have aJ: "a \ J" ``` wenzelm@45005 ` 269` ``` proof (simp add: J_def r_coset_def set_add_defs) ``` wenzelm@45005 ` 270` ``` from acarr ``` wenzelm@45005 ` 271` ``` have "a = \ \ a \ \" by algebra ``` wenzelm@45005 ` 272` ``` with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] ``` wenzelm@45005 ` 273` ``` show "\x\carrier R. \k\I. a = x \ a \ k" by fast ``` wenzelm@45005 ` 274` ``` qed ``` ballarin@20318 ` 275` wenzelm@45005 ` 276` ``` from aJ and anI have JnI: "J \ I" by fast ``` ballarin@20318 ` 277` wenzelm@67443 ` 278` ``` \ \Deducing @{term "J = carrier R"} because @{term "I"} is maximal\ ``` wenzelm@45005 ` 279` ``` from idealJ and IinJ have "J = I \ J = carrier R" ``` wenzelm@45005 ` 280` ``` proof (rule I_maximal, unfold J_def) ``` wenzelm@45005 ` 281` ``` have "carrier R #> a \ carrier R" ``` wenzelm@45005 ` 282` ``` using subset_refl acarr by (rule r_coset_subset_G) ``` wenzelm@45005 ` 283` ``` then show "carrier R #> a <+> I \ carrier R" ``` wenzelm@45005 ` 284` ``` using a_subset by (rule set_add_closed) ``` wenzelm@45005 ` 285` ``` qed ``` wenzelm@45005 ` 286` wenzelm@45005 ` 287` ``` with JnI have Jcarr: "J = carrier R" by simp ``` ballarin@20318 ` 288` wenzelm@67443 ` 289` ``` \ \Calculating an inverse for @{term "a"}\ ``` wenzelm@45005 ` 290` ``` from one_closed[folded Jcarr] ``` wenzelm@45005 ` 291` ``` have "\r\carrier R. \i\I. \ = r \ a \ i" ``` wenzelm@45005 ` 292` ``` by (simp add: J_def r_coset_def set_add_defs) ``` wenzelm@45005 ` 293` ``` then obtain r i where rcarr: "r \ carrier R" ``` wenzelm@45005 ` 294` ``` and iI: "i \ I" and one: "\ = r \ a \ i" by fast ``` wenzelm@45005 ` 295` ``` from one and rcarr and acarr and iI[THEN a_Hcarr] ``` wenzelm@45005 ` 296` ``` have rai1: "a \ r = \i \ \" by algebra ``` ballarin@20318 ` 297` wenzelm@67443 ` 298` ``` \ \Lifting to cosets\ ``` wenzelm@45005 ` 299` ``` from iI have "\i \ \ \ I +> \" ``` wenzelm@45005 ` 300` ``` by (intro a_rcosI, simp, intro a_subset, simp) ``` wenzelm@45005 ` 301` ``` with rai1 have "a \ r \ I +> \" by simp ``` wenzelm@45005 ` 302` ``` then have "I +> \ = I +> a \ r" ``` wenzelm@45005 ` 303` ``` by (rule a_repr_independence, simp) (rule a_subgroup) ``` wenzelm@45005 ` 304` wenzelm@45005 ` 305` ``` from rcarr and this[symmetric] ``` wenzelm@45005 ` 306` ``` show "\r\carrier R. I +> a \ r = I +> \" by fast ``` wenzelm@45005 ` 307` ``` qed ``` ballarin@27611 ` 308` ```qed ``` ballarin@20318 ` 309` lp15@68551 ` 310` lp15@68551 ` 311` ```lemma (in ring_hom_ring) trivial_hom_iff: ``` lp15@68551 ` 312` ``` "(h ` (carrier R) = { \\<^bsub>S\<^esub> }) = (a_kernel R S h = carrier R)" ``` lp15@68551 ` 313` ``` using group_hom.trivial_hom_iff[OF a_group_hom] by (simp add: a_kernel_def) ``` lp15@68551 ` 314` lp15@68551 ` 315` ```lemma (in ring_hom_ring) trivial_ker_imp_inj: ``` lp15@68551 ` 316` ``` assumes "a_kernel R S h = { \ }" ``` lp15@68551 ` 317` ``` shows "inj_on h (carrier R)" ``` lp15@68551 ` 318` ``` using group_hom.trivial_ker_imp_inj[OF a_group_hom] assms a_kernel_def[of R S h] by simp ``` lp15@68551 ` 319` lp15@68551 ` 320` ```lemma (in ring_hom_ring) non_trivial_field_hom_imp_inj: ``` lp15@68551 ` 321` ``` assumes "field R" ``` lp15@68551 ` 322` ``` shows "h ` (carrier R) \ { \\<^bsub>S\<^esub> } \ inj_on h (carrier R)" ``` lp15@68551 ` 323` ```proof - ``` lp15@68551 ` 324` ``` assume "h ` (carrier R) \ { \\<^bsub>S\<^esub> }" ``` lp15@68551 ` 325` ``` hence "a_kernel R S h \ carrier R" ``` lp15@68551 ` 326` ``` using trivial_hom_iff by linarith ``` lp15@68551 ` 327` ``` hence "a_kernel R S h = { \ }" ``` lp15@68551 ` 328` ``` using field.all_ideals[OF assms] kernel_is_ideal by blast ``` lp15@68551 ` 329` ``` thus "inj_on h (carrier R)" ``` lp15@68551 ` 330` ``` using trivial_ker_imp_inj by blast ``` lp15@68551 ` 331` ```qed ``` lp15@68551 ` 332` lp15@68551 ` 333` ```lemma (in ring_hom_ring) img_is_add_subgroup: ``` lp15@68551 ` 334` ``` assumes "subgroup H (add_monoid R)" ``` lp15@68551 ` 335` ``` shows "subgroup (h ` H) (add_monoid S)" ``` lp15@68551 ` 336` ```proof - ``` lp15@68551 ` 337` ``` have "group ((add_monoid R) \ carrier := H \)" ``` lp15@68551 ` 338` ``` using assms R.add.subgroup_imp_group by blast ``` lp15@68551 ` 339` ``` moreover have "H \ carrier R" by (simp add: R.add.subgroupE(1) assms) ``` lp15@68551 ` 340` ``` hence "h \ hom ((add_monoid R) \ carrier := H \) (add_monoid S)" ``` lp15@68551 ` 341` ``` unfolding hom_def by (auto simp add: subsetD) ``` lp15@68551 ` 342` ``` ultimately have "subgroup (h ` carrier ((add_monoid R) \ carrier := H \)) (add_monoid S)" ``` lp15@68551 ` 343` ``` using group_hom.img_is_subgroup[of "(add_monoid R) \ carrier := H \" "add_monoid S" h] ``` lp15@68551 ` 344` ``` using a_group_hom group_hom_axioms.intro group_hom_def by blast ``` lp15@68551 ` 345` ``` thus "subgroup (h ` H) (add_monoid S)" by simp ``` lp15@68551 ` 346` ```qed ``` lp15@68551 ` 347` lp15@68551 ` 348` ```lemma (in ring) ring_ideal_imp_quot_ideal: ``` lp15@68551 ` 349` ``` assumes "ideal I R" ``` lp15@68551 ` 350` ``` shows "ideal J R \ ideal ((+>) I ` J) (R Quot I)" ``` lp15@68551 ` 351` ```proof - ``` lp15@68551 ` 352` ``` assume A: "ideal J R" show "ideal (((+>) I) ` J) (R Quot I)" ``` lp15@68551 ` 353` ``` proof (rule idealI) ``` lp15@68551 ` 354` ``` show "ring (R Quot I)" ``` lp15@68551 ` 355` ``` by (simp add: assms(1) ideal.quotient_is_ring) ``` lp15@68551 ` 356` ``` next ``` lp15@68551 ` 357` ``` have "subgroup J (add_monoid R)" ``` lp15@68551 ` 358` ``` by (simp add: additive_subgroup.a_subgroup A ideal.axioms(1)) ``` lp15@68551 ` 359` ``` moreover have "((+>) I) \ ring_hom R (R Quot I)" ``` lp15@68551 ` 360` ``` by (simp add: assms(1) ideal.rcos_ring_hom) ``` lp15@68551 ` 361` ``` ultimately show "subgroup ((+>) I ` J) (add_monoid (R Quot I))" ``` lp15@68551 ` 362` ``` using assms(1) ideal.rcos_ring_hom_ring ring_hom_ring.img_is_add_subgroup by blast ``` lp15@68551 ` 363` ``` next ``` lp15@68551 ` 364` ``` fix a x assume "a \ (+>) I ` J" "x \ carrier (R Quot I)" ``` lp15@68551 ` 365` ``` then obtain i j where i: "i \ carrier R" "x = I +> i" ``` lp15@68551 ` 366` ``` and j: "j \ J" "a = I +> j" ``` lp15@68551 ` 367` ``` unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto ``` lp15@68551 ` 368` ``` hence "a \\<^bsub>R Quot I\<^esub> x = [mod I:] (I +> j) \ (I +> i)" ``` lp15@68551 ` 369` ``` unfolding FactRing_def by simp ``` lp15@68551 ` 370` ``` hence "a \\<^bsub>R Quot I\<^esub> x = I +> (j \ i)" ``` lp15@68551 ` 371` ``` using ideal.rcoset_mult_add[OF assms(1), of j i] i(1) j(1) A ideal.Icarr by force ``` lp15@68551 ` 372` ``` thus "a \\<^bsub>R Quot I\<^esub> x \ (+>) I ` J" ``` lp15@68551 ` 373` ``` using A i(1) j(1) by (simp add: ideal.I_r_closed) ``` lp15@68551 ` 374` ``` ``` lp15@68551 ` 375` ``` have "x \\<^bsub>R Quot I\<^esub> a = [mod I:] (I +> i) \ (I +> j)" ``` lp15@68551 ` 376` ``` unfolding FactRing_def i j by simp ``` lp15@68551 ` 377` ``` hence "x \\<^bsub>R Quot I\<^esub> a = I +> (i \ j)" ``` lp15@68551 ` 378` ``` using ideal.rcoset_mult_add[OF assms(1), of i j] i(1) j(1) A ideal.Icarr by force ``` lp15@68551 ` 379` ``` thus "x \\<^bsub>R Quot I\<^esub> a \ (+>) I ` J" ``` lp15@68551 ` 380` ``` using A i(1) j(1) by (simp add: ideal.I_l_closed) ``` lp15@68551 ` 381` ``` qed ``` lp15@68551 ` 382` ```qed ``` lp15@68551 ` 383` lp15@68551 ` 384` ```lemma (in ring_hom_ring) ideal_vimage: ``` lp15@68551 ` 385` ``` assumes "ideal I S" ``` lp15@68551 ` 386` ``` shows "ideal { r \ carrier R. h r \ I } R" (* or (carrier R) \ (h -` I) *) ``` lp15@68551 ` 387` ```proof ``` lp15@68551 ` 388` ``` show "{ r \ carrier R. h r \ I } \ carrier (add_monoid R)" by auto ``` lp15@68551 ` 389` ```next ``` lp15@68551 ` 390` ``` show "\\<^bsub>add_monoid R\<^esub> \ { r \ carrier R. h r \ I }" ``` lp15@68551 ` 391` ``` by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1)) ``` lp15@68551 ` 392` ```next ``` lp15@68551 ` 393` ``` fix a b ``` lp15@68551 ` 394` ``` assume "a \ { r \ carrier R. h r \ I }" ``` lp15@68551 ` 395` ``` and "b \ { r \ carrier R. h r \ I }" ``` lp15@68551 ` 396` ``` hence a: "a \ carrier R" "h a \ I" ``` lp15@68551 ` 397` ``` and b: "b \ carrier R" "h b \ I" by auto ``` lp15@68551 ` 398` ``` hence "h (a \ b) = (h a) \\<^bsub>S\<^esub> (h b)" using hom_add by blast ``` lp15@68551 ` 399` ``` moreover have "(h a) \\<^bsub>S\<^esub> (h b) \ I" using a b assms ``` lp15@68551 ` 400` ``` by (simp add: additive_subgroup.a_closed ideal.axioms(1)) ``` lp15@68551 ` 401` ``` ultimately show "a \\<^bsub>add_monoid R\<^esub> b \ { r \ carrier R. h r \ I }" ``` lp15@68551 ` 402` ``` using a(1) b (1) by auto ``` lp15@68551 ` 403` lp15@68551 ` 404` ``` have "h (\ a) = \\<^bsub>S\<^esub> (h a)" by (simp add: a) ``` lp15@68551 ` 405` ``` moreover have "\\<^bsub>S\<^esub> (h a) \ I" ``` lp15@68551 ` 406` ``` by (simp add: a(2) additive_subgroup.a_inv_closed assms ideal.axioms(1)) ``` lp15@68551 ` 407` ``` ultimately show "inv\<^bsub>add_monoid R\<^esub> a \ { r \ carrier R. h r \ I }" ``` lp15@68551 ` 408` ``` using a by (simp add: a_inv_def) ``` lp15@68551 ` 409` ```next ``` lp15@68551 ` 410` ``` fix a r ``` lp15@68551 ` 411` ``` assume "a \ { r \ carrier R. h r \ I }" and r: "r \ carrier R" ``` lp15@68551 ` 412` ``` hence a: "a \ carrier R" "h a \ I" by auto ``` lp15@68551 ` 413` lp15@68551 ` 414` ``` have "h a \\<^bsub>S\<^esub> h r \ I" ``` lp15@68551 ` 415` ``` using assms a r by (simp add: ideal.I_r_closed) ``` lp15@68551 ` 416` ``` thus "a \ r \ { r \ carrier R. h r \ I }" by (simp add: a(1) r) ``` lp15@68551 ` 417` lp15@68551 ` 418` ``` have "h r \\<^bsub>S\<^esub> h a \ I" ``` lp15@68551 ` 419` ``` using assms a r by (simp add: ideal.I_l_closed) ``` lp15@68551 ` 420` ``` thus "r \ a \ { r \ carrier R. h r \ I }" by (simp add: a(1) r) ``` lp15@68551 ` 421` ```qed ``` lp15@68551 ` 422` lp15@68551 ` 423` ```lemma (in ring) canonical_proj_vimage_in_carrier: ``` lp15@68551 ` 424` ``` assumes "ideal I R" ``` lp15@68551 ` 425` ``` shows "J \ carrier (R Quot I) \ \ J \ carrier R" ``` lp15@68551 ` 426` ```proof - ``` lp15@68551 ` 427` ``` assume A: "J \ carrier (R Quot I)" show "\ J \ carrier R" ``` lp15@68551 ` 428` ``` proof ``` lp15@68551 ` 429` ``` fix j assume j: "j \ \ J" ``` lp15@68551 ` 430` ``` then obtain j' where j': "j' \ J" "j \ j'" by blast ``` lp15@68551 ` 431` ``` then obtain r where r: "r \ carrier R" "j' = I +> r" ``` lp15@68551 ` 432` ``` using A j' unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto ``` lp15@68551 ` 433` ``` thus "j \ carrier R" using j' assms ``` lp15@68551 ` 434` ``` by (meson a_r_coset_subset_G additive_subgroup.a_subset contra_subsetD ideal.axioms(1)) ``` lp15@68551 ` 435` ``` qed ``` lp15@68551 ` 436` ```qed ``` lp15@68551 ` 437` lp15@68551 ` 438` ```lemma (in ring) canonical_proj_vimage_mem_iff: ``` lp15@68551 ` 439` ``` assumes "ideal I R" "J \ carrier (R Quot I)" ``` lp15@68551 ` 440` ``` shows "\a. a \ carrier R \ (a \ (\ J)) = (I +> a \ J)" ``` lp15@68551 ` 441` ```proof - ``` lp15@68551 ` 442` ``` fix a assume a: "a \ carrier R" show "(a \ (\ J)) = (I +> a \ J)" ``` lp15@68551 ` 443` ``` proof ``` lp15@68551 ` 444` ``` assume "a \ \ J" ``` lp15@68551 ` 445` ``` then obtain j where j: "j \ J" "a \ j" by blast ``` lp15@68551 ` 446` ``` then obtain r where r: "r \ carrier R" "j = I +> r" ``` lp15@68551 ` 447` ``` using assms j unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto ``` lp15@68551 ` 448` ``` hence "I +> r = I +> a" ``` lp15@68551 ` 449` ``` using add.repr_independence[of a I r] j r ``` lp15@68551 ` 450` ``` by (metis a_r_coset_def additive_subgroup.a_subgroup assms(1) ideal.axioms(1)) ``` lp15@68551 ` 451` ``` thus "I +> a \ J" using r j by simp ``` lp15@68551 ` 452` ``` next ``` lp15@68551 ` 453` ``` assume "I +> a \ J" ``` lp15@68551 ` 454` ``` hence "\ \ a \ I +> a" ``` lp15@68551 ` 455` ``` using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] ``` lp15@68551 ` 456` ``` a_r_coset_def'[of R I a] by blast ``` lp15@68551 ` 457` ``` thus "a \ \ J" using a \I +> a \ J\ by auto ``` lp15@68551 ` 458` ``` qed ``` lp15@68551 ` 459` ```qed ``` lp15@68551 ` 460` lp15@68551 ` 461` ```corollary (in ring) quot_ideal_imp_ring_ideal: ``` lp15@68551 ` 462` ``` assumes "ideal I R" ``` lp15@68551 ` 463` ``` shows "ideal J (R Quot I) \ ideal (\ J) R" ``` lp15@68551 ` 464` ```proof - ``` lp15@68551 ` 465` ``` assume A: "ideal J (R Quot I)" ``` lp15@68551 ` 466` ``` have "\ J = { r \ carrier R. I +> r \ J }" ``` lp15@68551 ` 467` ``` using canonical_proj_vimage_in_carrier[OF assms, of J] ``` lp15@68551 ` 468` ``` canonical_proj_vimage_mem_iff[OF assms, of J] ``` lp15@68551 ` 469` ``` additive_subgroup.a_subset[OF ideal.axioms(1)[OF A]] by blast ``` lp15@68551 ` 470` ``` thus "ideal (\ J) R" ``` lp15@68551 ` 471` ``` using ring_hom_ring.ideal_vimage[OF ideal.rcos_ring_hom_ring[OF assms] A] by simp ``` lp15@68551 ` 472` ```qed ``` lp15@68551 ` 473` lp15@68551 ` 474` ```lemma (in ring) ideal_incl_iff: ``` lp15@68551 ` 475` ``` assumes "ideal I R" "ideal J R" ``` lp15@68551 ` 476` ``` shows "(I \ J) = (J = (\ j \ J. I +> j))" ``` lp15@68551 ` 477` ```proof ``` lp15@68551 ` 478` ``` assume A: "J = (\ j \ J. I +> j)" hence "I +> \ \ J" ``` lp15@68551 ` 479` ``` using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(2)]] by blast ``` lp15@68551 ` 480` ``` thus "I \ J" using additive_subgroup.a_subset[OF ideal.axioms(1)[OF assms(1)]] by simp ``` lp15@68551 ` 481` ```next ``` lp15@68551 ` 482` ``` assume A: "I \ J" show "J = (\j\J. I +> j)" ``` lp15@68551 ` 483` ``` proof ``` lp15@68551 ` 484` ``` show "J \ (\ j \ J. I +> j)" ``` lp15@68551 ` 485` ``` proof ``` lp15@68551 ` 486` ``` fix j assume j: "j \ J" ``` lp15@68551 ` 487` ``` have "\ \ I" by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1)) ``` lp15@68551 ` 488` ``` hence "\ \ j \ I +> j" ``` lp15@68551 ` 489` ``` using a_r_coset_def'[of R I j] by blast ``` lp15@68551 ` 490` ``` thus "j \ (\j\J. I +> j)" ``` lp15@68551 ` 491` ``` using assms(2) j additive_subgroup.a_Hcarr ideal.axioms(1) by fastforce ``` lp15@68551 ` 492` ``` qed ``` lp15@68551 ` 493` ``` next ``` lp15@68551 ` 494` ``` show "(\ j \ J. I +> j) \ J" ``` lp15@68551 ` 495` ``` proof ``` lp15@68551 ` 496` ``` fix x assume "x \ (\ j \ J. I +> j)" ``` lp15@68551 ` 497` ``` then obtain j where j: "j \ J" "x \ I +> j" by blast ``` lp15@68551 ` 498` ``` then obtain i where i: "i \ I" "x = i \ j" ``` lp15@68551 ` 499` ``` using a_r_coset_def'[of R I j] by blast ``` lp15@68551 ` 500` ``` thus "x \ J" ``` lp15@68551 ` 501` ``` using assms(2) j A additive_subgroup.a_closed[OF ideal.axioms(1)[OF assms(2)]] by blast ``` lp15@68551 ` 502` ``` qed ``` lp15@68551 ` 503` ``` qed ``` lp15@68551 ` 504` ```qed ``` lp15@68551 ` 505` lp15@68551 ` 506` ```theorem (in ring) quot_ideal_correspondence: ``` lp15@68551 ` 507` ``` assumes "ideal I R" ``` lp15@68551 ` 508` ``` shows "bij_betw (\J. (+>) I ` J) { J. ideal J R \ I \ J } { J . ideal J (R Quot I) }" ``` lp15@68551 ` 509` ```proof (rule bij_betw_byWitness[where ?f' = "\X. \ X"]) ``` lp15@68551 ` 510` ``` show "\J \ { J. ideal J R \ I \ J }. (\X. \ X) ((+>) I ` J) = J" ``` lp15@68551 ` 511` ``` using assms ideal_incl_iff by blast ``` lp15@68551 ` 512` ```next ``` lp15@68551 ` 513` ``` show "(\J. (+>) I ` J) ` { J. ideal J R \ I \ J } \ { J. ideal J (R Quot I) }" ``` lp15@68551 ` 514` ``` using assms ring_ideal_imp_quot_ideal by auto ``` lp15@68551 ` 515` ```next ``` lp15@68551 ` 516` ``` show "(\X. \ X) ` { J. ideal J (R Quot I) } \ { J. ideal J R \ I \ J }" ``` lp15@68551 ` 517` ``` proof ``` lp15@68551 ` 518` ``` fix J assume "J \ ((\X. \ X) ` { J. ideal J (R Quot I) })" ``` lp15@68551 ` 519` ``` then obtain J' where J': "ideal J' (R Quot I)" "J = \ J'" by blast ``` lp15@68551 ` 520` ``` hence "ideal J R" ``` lp15@68551 ` 521` ``` using assms quot_ideal_imp_ring_ideal by auto ``` lp15@68551 ` 522` ``` moreover have "I \ J'" ``` lp15@68551 ` 523` ``` using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF J'(1)]] unfolding FactRing_def by simp ``` lp15@68551 ` 524` ``` ultimately show "J \ { J. ideal J R \ I \ J }" using J'(2) by auto ``` lp15@68551 ` 525` ``` qed ``` lp15@68551 ` 526` ```next ``` lp15@68551 ` 527` ``` show "\J' \ { J. ideal J (R Quot I) }. ((+>) I ` (\ J')) = J'" ``` lp15@68551 ` 528` ``` proof ``` lp15@68551 ` 529` ``` fix J' assume "J' \ { J. ideal J (R Quot I) }" ``` lp15@68551 ` 530` ``` hence subset: "J' \ carrier (R Quot I) \ ideal J' (R Quot I)" ``` lp15@68551 ` 531` ``` using additive_subgroup.a_subset ideal_def by blast ``` lp15@68551 ` 532` ``` hence "((+>) I ` (\ J')) \ J'" ``` lp15@68551 ` 533` ``` using canonical_proj_vimage_in_carrier canonical_proj_vimage_mem_iff ``` lp15@68551 ` 534` ``` by (meson assms contra_subsetD image_subsetI) ``` lp15@68551 ` 535` ``` moreover have "J' \ ((+>) I ` (\ J'))" ``` lp15@68551 ` 536` ``` proof ``` lp15@68551 ` 537` ``` fix x assume "x \ J'" ``` lp15@68551 ` 538` ``` then obtain r where r: "r \ carrier R" "x = I +> r" ``` lp15@68551 ` 539` ``` using subset unfolding FactRing_def A_RCOSETS_def'[of R I] by auto ``` lp15@68551 ` 540` ``` hence "r \ (\ J')" ``` lp15@68551 ` 541` ``` using \x \ J'\ assms canonical_proj_vimage_mem_iff subset by blast ``` lp15@68551 ` 542` ``` thus "x \ ((+>) I ` (\ J'))" using r(2) by blast ``` lp15@68551 ` 543` ``` qed ``` lp15@68551 ` 544` ``` ultimately show "((+>) I ` (\ J')) = J'" by blast ``` lp15@68551 ` 545` ``` qed ``` lp15@68551 ` 546` ```qed ``` lp15@68551 ` 547` lp15@68551 ` 548` ```lemma (in cring) quot_domain_imp_primeideal: ``` lp15@68551 ` 549` ``` assumes "ideal P R" ``` lp15@68551 ` 550` ``` shows "domain (R Quot P) \ primeideal P R" ``` lp15@68551 ` 551` ```proof - ``` lp15@68551 ` 552` ``` assume A: "domain (R Quot P)" show "primeideal P R" ``` lp15@68551 ` 553` ``` proof (rule primeidealI) ``` lp15@68551 ` 554` ``` show "ideal P R" using assms . ``` lp15@68551 ` 555` ``` show "cring R" using is_cring . ``` lp15@68551 ` 556` ``` next ``` lp15@68551 ` 557` ``` show "carrier R \ P" ``` lp15@68551 ` 558` ``` proof (rule ccontr) ``` lp15@68551 ` 559` ``` assume "\ carrier R \ P" hence "carrier R = P" by simp ``` lp15@68551 ` 560` ``` hence "\I. I \ carrier (R Quot P) \ I = P" ``` lp15@68551 ` 561` ``` unfolding FactRing_def A_RCOSETS_def' apply simp ``` lp15@68551 ` 562` ``` using a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1) by blast ``` lp15@68551 ` 563` ``` hence "\\<^bsub>(R Quot P)\<^esub> = \\<^bsub>(R Quot P)\<^esub>" ``` lp15@68551 ` 564` ``` by (metis assms ideal.quotient_is_ring ring.ring_simprules(2) ring.ring_simprules(6)) ``` lp15@68551 ` 565` ``` thus False using domain.one_not_zero[OF A] by simp ``` lp15@68551 ` 566` ``` qed ``` lp15@68551 ` 567` ``` next ``` lp15@68551 ` 568` ``` fix a b assume a: "a \ carrier R" and b: "b \ carrier R" and ab: "a \ b \ P" ``` lp15@68551 ` 569` ``` hence "P +> (a \ b) = \\<^bsub>(R Quot P)\<^esub>" unfolding FactRing_def ``` lp15@68551 ` 570` ``` by (simp add: a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1)) ``` lp15@68551 ` 571` ``` moreover have "(P +> a) \\<^bsub>(R Quot P)\<^esub> (P +> b) = P +> (a \ b)" unfolding FactRing_def ``` lp15@68551 ` 572` ``` using a b by (simp add: assms ideal.rcoset_mult_add) ``` lp15@68551 ` 573` ``` moreover have "P +> a \ carrier (R Quot P) \ P +> b \ carrier (R Quot P)" ``` lp15@68551 ` 574` ``` by (simp add: a b FactRing_def a_rcosetsI additive_subgroup.a_subset assms ideal.axioms(1)) ``` lp15@68551 ` 575` ``` ultimately have "P +> a = \\<^bsub>(R Quot P)\<^esub> \ P +> b = \\<^bsub>(R Quot P)\<^esub>" ``` lp15@68551 ` 576` ``` using domain.integral[OF A, of "P +> a" "P +> b"] by auto ``` lp15@68551 ` 577` ``` thus "a \ P \ b \ P" unfolding FactRing_def apply simp ``` lp15@68551 ` 578` ``` using a b assms a_coset_join1 additive_subgroup.a_subgroup ideal.axioms(1) by blast ``` lp15@68551 ` 579` ``` qed ``` lp15@68551 ` 580` ```qed ``` lp15@68551 ` 581` lp15@68551 ` 582` ```lemma (in cring) quot_domain_iff_primeideal: ``` lp15@68551 ` 583` ``` assumes "ideal P R" ``` lp15@68551 ` 584` ``` shows "domain (R Quot P) = primeideal P R" ``` lp15@68551 ` 585` ``` using quot_domain_imp_primeideal[OF assms] primeideal.quotient_is_domain[of P R] by auto ``` lp15@68551 ` 586` lp15@68551 ` 587` lp15@68551 ` 588` ```subsection \Isomorphism\ ``` lp15@68551 ` 589` lp15@68551 ` 590` ```definition ``` lp15@68551 ` 591` ``` ring_iso :: "_ \ _ \ ('a \ 'b) set" ``` lp15@68551 ` 592` ``` where "ring_iso R S = { h. h \ ring_hom R S \ bij_betw h (carrier R) (carrier S) }" ``` lp15@68551 ` 593` lp15@68551 ` 594` ```definition ``` lp15@68551 ` 595` ``` is_ring_iso :: "_ \ _ \ bool" (infixr "\" 60) ``` lp15@68551 ` 596` ``` where "R \ S = (ring_iso R S \ {})" ``` lp15@68551 ` 597` lp15@68551 ` 598` ```definition ``` lp15@68551 ` 599` ``` morphic_prop :: "_ \ ('a \ bool) \ bool" ``` lp15@68551 ` 600` ``` where "morphic_prop R P = ``` lp15@68551 ` 601` ``` ((P \\<^bsub>R\<^esub>) \ ``` lp15@68551 ` 602` ``` (\r \ carrier R. P r) \ ``` lp15@68551 ` 603` ``` (\r1 \ carrier R. \r2 \ carrier R. P (r1 \\<^bsub>R\<^esub> r2)) \ ``` lp15@68551 ` 604` ``` (\r1 \ carrier R. \r2 \ carrier R. P (r1 \\<^bsub>R\<^esub> r2)))" ``` lp15@68551 ` 605` lp15@68551 ` 606` ```lemma ring_iso_memI: ``` lp15@68551 ` 607` ``` fixes R (structure) and S (structure) ``` lp15@68551 ` 608` ``` assumes "\x. x \ carrier R \ h x \ carrier S" ``` lp15@68551 ` 609` ``` and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" ``` lp15@68551 ` 610` ``` and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" ``` lp15@68551 ` 611` ``` and "h \ = \\<^bsub>S\<^esub>" ``` lp15@68551 ` 612` ``` and "bij_betw h (carrier R) (carrier S)" ``` lp15@68551 ` 613` ``` shows "h \ ring_iso R S" ``` lp15@68551 ` 614` ``` by (auto simp add: ring_hom_memI assms ring_iso_def) ``` lp15@68551 ` 615` lp15@68551 ` 616` ```lemma ring_iso_memE: ``` lp15@68551 ` 617` ``` fixes R (structure) and S (structure) ``` lp15@68551 ` 618` ``` assumes "h \ ring_iso R S" ``` lp15@68551 ` 619` ``` shows "\x. x \ carrier R \ h x \ carrier S" ``` lp15@68551 ` 620` ``` and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" ``` lp15@68551 ` 621` ``` and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" ``` lp15@68551 ` 622` ``` and "h \ = \\<^bsub>S\<^esub>" ``` lp15@68551 ` 623` ``` and "bij_betw h (carrier R) (carrier S)" ``` lp15@68551 ` 624` ``` using assms unfolding ring_iso_def ring_hom_def by auto ``` lp15@68551 ` 625` lp15@68551 ` 626` ```lemma morphic_propI: ``` lp15@68551 ` 627` ``` fixes R (structure) ``` lp15@68551 ` 628` ``` assumes "P \" ``` lp15@68551 ` 629` ``` and "\r. r \ carrier R \ P r" ``` lp15@68551 ` 630` ``` and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)" ``` lp15@68551 ` 631` ``` and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)" ``` lp15@68551 ` 632` ``` shows "morphic_prop R P" ``` lp15@68551 ` 633` ``` unfolding morphic_prop_def using assms by auto ``` lp15@68551 ` 634` lp15@68551 ` 635` ```lemma morphic_propE: ``` lp15@68551 ` 636` ``` fixes R (structure) ``` lp15@68551 ` 637` ``` assumes "morphic_prop R P" ``` lp15@68551 ` 638` ``` shows "P \" ``` lp15@68551 ` 639` ``` and "\r. r \ carrier R \ P r" ``` lp15@68551 ` 640` ``` and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)" ``` lp15@68551 ` 641` ``` and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)" ``` lp15@68551 ` 642` ``` using assms unfolding morphic_prop_def by auto ``` lp15@68551 ` 643` lp15@68551 ` 644` ```lemma ring_iso_restrict: ``` lp15@68551 ` 645` ``` assumes "f \ ring_iso R S" ``` lp15@68551 ` 646` ``` and "\r. r \ carrier R \ f r = g r" ``` lp15@68551 ` 647` ``` and "ring R" ``` lp15@68551 ` 648` ``` shows "g \ ring_iso R S" ``` lp15@68551 ` 649` ```proof (rule ring_iso_memI) ``` lp15@68551 ` 650` ``` show "bij_betw g (carrier R) (carrier S)" ``` lp15@68551 ` 651` ``` using assms(1-2) bij_betw_cong ring_iso_memE(5) by blast ``` lp15@68551 ` 652` ``` show "g \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>" ``` lp15@68551 ` 653` ``` using assms ring.ring_simprules(6) ring_iso_memE(4) by force ``` lp15@68551 ` 654` ```next ``` lp15@68551 ` 655` ``` fix x y assume x: "x \ carrier R" and y: "y \ carrier R" ``` lp15@68551 ` 656` ``` show "g x \ carrier S" ``` lp15@68551 ` 657` ``` using assms(1-2) ring_iso_memE(1) x by fastforce ``` lp15@68551 ` 658` ``` show "g (x \\<^bsub>R\<^esub> y) = g x \\<^bsub>S\<^esub> g y" ``` lp15@68551 ` 659` ``` by (metis assms ring.ring_simprules(5) ring_iso_memE(2) x y) ``` lp15@68551 ` 660` ``` show "g (x \\<^bsub>R\<^esub> y) = g x \\<^bsub>S\<^esub> g y" ``` lp15@68551 ` 661` ``` by (metis assms ring.ring_simprules(1) ring_iso_memE(3) x y) ``` lp15@68551 ` 662` ```qed ``` lp15@68551 ` 663` lp15@68551 ` 664` ```lemma ring_iso_morphic_prop: ``` lp15@68551 ` 665` ``` assumes "f \ ring_iso R S" ``` lp15@68551 ` 666` ``` and "morphic_prop R P" ``` lp15@68551 ` 667` ``` and "\r. P r \ f r = g r" ``` lp15@68551 ` 668` ``` shows "g \ ring_iso R S" ``` lp15@68551 ` 669` ```proof - ``` lp15@68551 ` 670` ``` have eq0: "\r. r \ carrier R \ f r = g r" ``` lp15@68551 ` 671` ``` and eq1: "f \\<^bsub>R\<^esub> = g \\<^bsub>R\<^esub>" ``` lp15@68551 ` 672` ``` and eq2: "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ f (r1 \\<^bsub>R\<^esub> r2) = g (r1 \\<^bsub>R\<^esub> r2)" ``` lp15@68551 ` 673` ``` and eq3: "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ f (r1 \\<^bsub>R\<^esub> r2) = g (r1 \\<^bsub>R\<^esub> r2)" ``` lp15@68551 ` 674` ``` using assms(2-3) unfolding morphic_prop_def by auto ``` lp15@68551 ` 675` ``` show ?thesis ``` lp15@68551 ` 676` ``` apply (rule ring_iso_memI) ``` lp15@68551 ` 677` ``` using assms(1) eq0 ring_iso_memE(1) apply fastforce ``` lp15@68551 ` 678` ``` apply (metis assms(1) eq0 eq2 ring_iso_memE(2)) ``` lp15@68551 ` 679` ``` apply (metis assms(1) eq0 eq3 ring_iso_memE(3)) ``` lp15@68551 ` 680` ``` using assms(1) eq1 ring_iso_memE(4) apply fastforce ``` lp15@68551 ` 681` ``` using assms(1) bij_betw_cong eq0 ring_iso_memE(5) by blast ``` lp15@68551 ` 682` ```qed ``` lp15@68551 ` 683` lp15@68551 ` 684` ```lemma (in ring) ring_hom_imp_img_ring: ``` lp15@68551 ` 685` ``` assumes "h \ ring_hom R S" ``` lp15@68551 ` 686` ``` shows "ring (S \ carrier := h ` (carrier R), one := h \, zero := h \ \)" (is "ring ?h_img") ``` lp15@68551 ` 687` ```proof - ``` lp15@68551 ` 688` ``` have "h \ hom (add_monoid R) (add_monoid S)" ``` lp15@68551 ` 689` ``` using assms unfolding hom_def ring_hom_def by auto ``` lp15@68551 ` 690` ``` hence "comm_group ((add_monoid S) \ carrier := h ` (carrier R), one := h \ \)" ``` lp15@68551 ` 691` ``` using add.hom_imp_img_comm_group[of h "add_monoid S"] by simp ``` lp15@68551 ` 692` ``` hence comm_group: "comm_group (add_monoid ?h_img)" ``` lp15@68551 ` 693` ``` by (auto intro: comm_monoidI simp add: monoid.defs) ``` lp15@68551 ` 694` lp15@68551 ` 695` ``` moreover have "h \ hom R S" ``` lp15@68551 ` 696` ``` using assms unfolding ring_hom_def hom_def by auto ``` lp15@68551 ` 697` ``` hence "monoid (S \ carrier := h ` (carrier R), one := h \ \)" ``` lp15@68551 ` 698` ``` using hom_imp_img_monoid[of h S] by simp ``` lp15@68551 ` 699` ``` hence monoid: "monoid ?h_img" ``` lp15@68551 ` 700` ``` unfolding monoid_def by (simp add: monoid.defs) ``` lp15@68551 ` 701` lp15@68551 ` 702` ``` show ?thesis ``` lp15@68551 ` 703` ``` proof (rule ringI, simp_all add: comm_group_abelian_groupI[OF comm_group] monoid) ``` lp15@68551 ` 704` ``` fix x y z assume "x \ h ` carrier R" "y \ h ` carrier R" "z \ h ` carrier R" ``` lp15@68551 ` 705` ``` then obtain r1 r2 r3 ``` lp15@68551 ` 706` ``` where r1: "r1 \ carrier R" "x = h r1" ``` lp15@68551 ` 707` ``` and r2: "r2 \ carrier R" "y = h r2" ``` lp15@68551 ` 708` ``` and r3: "r3 \ carrier R" "z = h r3" by blast ``` lp15@68551 ` 709` ``` hence "(x \\<^bsub>S\<^esub> y) \\<^bsub>S\<^esub> z = h ((r1 \ r2) \ r3)" ``` lp15@68551 ` 710` ``` using ring_hom_memE[OF assms] by auto ``` lp15@68551 ` 711` ``` also have " ... = h ((r1 \ r3) \ (r2 \ r3))" ``` lp15@68551 ` 712` ``` using l_distr[OF r1(1) r2(1) r3(1)] by simp ``` lp15@68551 ` 713` ``` also have " ... = (x \\<^bsub>S\<^esub> z) \\<^bsub>S\<^esub> (y \\<^bsub>S\<^esub> z)" ``` lp15@68551 ` 714` ``` using ring_hom_memE[OF assms] r1 r2 r3 by auto ``` lp15@68551 ` 715` ``` finally show "(x \\<^bsub>S\<^esub> y) \\<^bsub>S\<^esub> z = (x \\<^bsub>S\<^esub> z) \\<^bsub>S\<^esub> (y \\<^bsub>S\<^esub> z)" . ``` lp15@68551 ` 716` lp15@68551 ` 717` ``` have "z \\<^bsub>S\<^esub> (x \\<^bsub>S\<^esub> y) = h (r3 \ (r1 \ r2))" ``` lp15@68551 ` 718` ``` using ring_hom_memE[OF assms] r1 r2 r3 by auto ``` lp15@68551 ` 719` ``` also have " ... = h ((r3 \ r1) \ (r3 \ r2))" ``` lp15@68551 ` 720` ``` using r_distr[OF r1(1) r2(1) r3(1)] by simp ``` lp15@68551 ` 721` ``` also have " ... = (z \\<^bsub>S\<^esub> x) \\<^bsub>S\<^esub> (z \\<^bsub>S\<^esub> y)" ``` lp15@68551 ` 722` ``` using ring_hom_memE[OF assms] r1 r2 r3 by auto ``` lp15@68551 ` 723` ``` finally show "z \\<^bsub>S\<^esub> (x \\<^bsub>S\<^esub> y) = (z \\<^bsub>S\<^esub> x) \\<^bsub>S\<^esub> (z \\<^bsub>S\<^esub> y)" . ``` lp15@68551 ` 724` ``` qed ``` lp15@68551 ` 725` ```qed ``` lp15@68551 ` 726` lp15@68551 ` 727` ```lemma (in ring) ring_iso_imp_img_ring: ``` lp15@68551 ` 728` ``` assumes "h \ ring_iso R S" ``` lp15@68551 ` 729` ``` shows "ring (S \ one := h \, zero := h \ \)" ``` lp15@68551 ` 730` ```proof - ``` lp15@68551 ` 731` ``` have "ring (S \ carrier := h ` (carrier R), one := h \, zero := h \ \)" ``` lp15@68551 ` 732` ``` using ring_hom_imp_img_ring[of h S] assms unfolding ring_iso_def by auto ``` lp15@68551 ` 733` ``` moreover have "h ` (carrier R) = carrier S" ``` lp15@68551 ` 734` ``` using assms unfolding ring_iso_def bij_betw_def by auto ``` lp15@68551 ` 735` ``` ultimately show ?thesis by simp ``` lp15@68551 ` 736` ```qed ``` lp15@68551 ` 737` lp15@68551 ` 738` ```lemma (in cring) ring_iso_imp_img_cring: ``` lp15@68551 ` 739` ``` assumes "h \ ring_iso R S" ``` lp15@68551 ` 740` ``` shows "cring (S \ one := h \, zero := h \ \)" (is "cring ?h_img") ``` lp15@68551 ` 741` ```proof - ``` lp15@68551 ` 742` ``` note m_comm ``` lp15@68551 ` 743` ``` interpret h_img?: ring ?h_img ``` lp15@68551 ` 744` ``` using ring_iso_imp_img_ring[OF assms] . ``` lp15@68551 ` 745` ``` show ?thesis ``` lp15@68551 ` 746` ``` proof (unfold_locales) ``` lp15@68551 ` 747` ``` fix x y assume "x \ carrier ?h_img" "y \ carrier ?h_img" ``` lp15@68551 ` 748` ``` then obtain r1 r2 ``` lp15@68551 ` 749` ``` where r1: "r1 \ carrier R" "x = h r1" ``` lp15@68551 ` 750` ``` and r2: "r2 \ carrier R" "y = h r2" ``` lp15@68551 ` 751` ``` using assms image_iff[where ?f = h and ?A = "carrier R"] ``` lp15@68551 ` 752` ``` unfolding ring_iso_def bij_betw_def by auto ``` lp15@68551 ` 753` ``` have "x \\<^bsub>(?h_img)\<^esub> y = h (r1 \ r2)" ``` lp15@68551 ` 754` ``` using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto ``` lp15@68551 ` 755` ``` also have " ... = h (r2 \ r1)" ``` lp15@68551 ` 756` ``` using m_comm[OF r1(1) r2(1)] by simp ``` lp15@68551 ` 757` ``` also have " ... = y \\<^bsub>(?h_img)\<^esub> x" ``` lp15@68551 ` 758` ``` using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto ``` lp15@68551 ` 759` ``` finally show "x \\<^bsub>(?h_img)\<^esub> y = y \\<^bsub>(?h_img)\<^esub> x" . ``` lp15@68551 ` 760` ``` qed ``` lp15@68551 ` 761` ```qed ``` lp15@68551 ` 762` lp15@68551 ` 763` ```lemma (in domain) ring_iso_imp_img_domain: ``` lp15@68551 ` 764` ``` assumes "h \ ring_iso R S" ``` lp15@68551 ` 765` ``` shows "domain (S \ one := h \, zero := h \ \)" (is "domain ?h_img") ``` lp15@68551 ` 766` ```proof - ``` lp15@68551 ` 767` ``` note aux = m_closed integral one_not_zero one_closed zero_closed ``` lp15@68551 ` 768` ``` interpret h_img?: cring ?h_img ``` lp15@68551 ` 769` ``` using ring_iso_imp_img_cring[OF assms] . ``` lp15@68551 ` 770` ``` show ?thesis ``` lp15@68551 ` 771` ``` proof (unfold_locales) ``` lp15@68551 ` 772` ``` show "\\<^bsub>?h_img\<^esub> \ \\<^bsub>?h_img\<^esub>" ``` lp15@68551 ` 773` ``` using ring_iso_memE(5)[OF assms] aux(3-4) ``` lp15@68551 ` 774` ``` unfolding bij_betw_def inj_on_def by force ``` lp15@68551 ` 775` ``` next ``` lp15@68551 ` 776` ``` fix a b ``` lp15@68551 ` 777` ``` assume A: "a \\<^bsub>?h_img\<^esub> b = \\<^bsub>?h_img\<^esub>" "a \ carrier ?h_img" "b \ carrier ?h_img" ``` lp15@68551 ` 778` ``` then obtain r1 r2 ``` lp15@68551 ` 779` ``` where r1: "r1 \ carrier R" "a = h r1" ``` lp15@68551 ` 780` ``` and r2: "r2 \ carrier R" "b = h r2" ``` lp15@68551 ` 781` ``` using assms image_iff[where ?f = h and ?A = "carrier R"] ``` lp15@68551 ` 782` ``` unfolding ring_iso_def bij_betw_def by auto ``` lp15@68551 ` 783` ``` hence "a \\<^bsub>?h_img\<^esub> b = h (r1 \ r2)" ``` lp15@68551 ` 784` ``` using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto ``` lp15@68551 ` 785` ``` hence "h (r1 \ r2) = h \" ``` lp15@68551 ` 786` ``` using A(1) by simp ``` lp15@68551 ` 787` ``` hence "r1 \ r2 = \" ``` lp15@68551 ` 788` ``` using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5) ``` lp15@68551 ` 789` ``` unfolding bij_betw_def inj_on_def by force ``` lp15@68551 ` 790` ``` hence "r1 = \ \ r2 = \" ``` lp15@68551 ` 791` ``` using aux(2)[OF _ r1(1) r2(1)] by simp ``` lp15@68551 ` 792` ``` thus "a = \\<^bsub>?h_img\<^esub> \ b = \\<^bsub>?h_img\<^esub>" ``` lp15@68551 ` 793` ``` unfolding r1 r2 by auto ``` lp15@68551 ` 794` ``` qed ``` lp15@68551 ` 795` ```qed ``` lp15@68551 ` 796` lp15@68551 ` 797` ```lemma (in field) ring_iso_imp_img_field: ``` lp15@68551 ` 798` ``` assumes "h \ ring_iso R S" ``` lp15@68551 ` 799` ``` shows "field (S \ one := h \, zero := h \ \)" (is "field ?h_img") ``` lp15@68551 ` 800` ```proof - ``` lp15@68551 ` 801` ``` interpret h_img?: domain ?h_img ``` lp15@68551 ` 802` ``` using ring_iso_imp_img_domain[OF assms] . ``` lp15@68551 ` 803` ``` show ?thesis ``` lp15@68551 ` 804` ``` proof (unfold_locales, auto simp add: Units_def) ``` lp15@68551 ` 805` ``` interpret field R using field_axioms . ``` lp15@68551 ` 806` ``` fix a assume a: "a \ carrier S" "a \\<^bsub>S\<^esub> h \ = h \" ``` lp15@68551 ` 807` ``` then obtain r where r: "r \ carrier R" "a = h r" ``` lp15@68551 ` 808` ``` using assms image_iff[where ?f = h and ?A = "carrier R"] ``` lp15@68551 ` 809` ``` unfolding ring_iso_def bij_betw_def by auto ``` lp15@68551 ` 810` ``` have "a \\<^bsub>S\<^esub> h \ = h (r \ \)" unfolding r(2) ``` lp15@68551 ` 811` ``` using ring_iso_memE(2)[OF assms r(1)] by simp ``` lp15@68551 ` 812` ``` hence "h \ = h \" ``` lp15@68551 ` 813` ``` using r(1) a(2) by simp ``` lp15@68551 ` 814` ``` thus False ``` lp15@68551 ` 815` ``` using ring_iso_memE(5)[OF assms] ``` lp15@68551 ` 816` ``` unfolding bij_betw_def inj_on_def by force ``` lp15@68551 ` 817` ``` next ``` lp15@68551 ` 818` ``` interpret field R using field_axioms . ``` lp15@68551 ` 819` ``` fix s assume s: "s \ carrier S" "s \ h \" ``` lp15@68551 ` 820` ``` then obtain r where r: "r \ carrier R" "s = h r" ``` lp15@68551 ` 821` ``` using assms image_iff[where ?f = h and ?A = "carrier R"] ``` lp15@68551 ` 822` ``` unfolding ring_iso_def bij_betw_def by auto ``` lp15@68551 ` 823` ``` hence "r \ \" using s(2) by auto ``` lp15@68551 ` 824` ``` hence inv_r: "inv r \ carrier R" "inv r \ \" "r \ inv r = \" "inv r \ r = \" ``` lp15@68551 ` 825` ``` using field_Units r(1) by auto ``` lp15@68551 ` 826` ``` have "h (inv r) \\<^bsub>S\<^esub> h r = h \" and "h r \\<^bsub>S\<^esub> h (inv r) = h \" ``` lp15@68551 ` 827` ``` using ring_iso_memE(2)[OF assms inv_r(1) r(1)] inv_r(3-4) ``` lp15@68551 ` 828` ``` ring_iso_memE(2)[OF assms r(1) inv_r(1)] by auto ``` lp15@68551 ` 829` ``` thus "\s' \ carrier S. s' \\<^bsub>S\<^esub> s = h \ \ s \\<^bsub>S\<^esub> s' = h \" ``` lp15@68551 ` 830` ``` using ring_iso_memE(1)[OF assms inv_r(1)] r(2) by auto ``` lp15@68551 ` 831` ``` qed ``` lp15@68551 ` 832` ```qed ``` lp15@68551 ` 833` lp15@68551 ` 834` ```lemma ring_iso_same_card: "R \ S \ card (carrier R) = card (carrier S)" ``` lp15@68551 ` 835` ```proof - ``` lp15@68551 ` 836` ``` assume "R \ S" ``` lp15@68551 ` 837` ``` then obtain h where "bij_betw h (carrier R) (carrier S)" ``` lp15@68551 ` 838` ``` unfolding is_ring_iso_def ring_iso_def by auto ``` lp15@68551 ` 839` ``` thus "card (carrier R) = card (carrier S)" ``` lp15@68551 ` 840` ``` using bij_betw_same_card[of h "carrier R" "carrier S"] by simp ``` lp15@68551 ` 841` ```qed ``` lp15@68551 ` 842` lp15@68551 ` 843` ```lemma ring_iso_set_refl: "id \ ring_iso R R" ``` lp15@68551 ` 844` ``` by (rule ring_iso_memI) (auto) ``` lp15@68551 ` 845` lp15@68551 ` 846` ```corollary ring_iso_refl: "R \ R" ``` lp15@68551 ` 847` ``` using is_ring_iso_def ring_iso_set_refl by auto ``` lp15@68551 ` 848` lp15@68551 ` 849` ```lemma ring_iso_set_trans: ``` lp15@68551 ` 850` ``` "\ f \ ring_iso R S; g \ ring_iso S Q \ \ (g \ f) \ ring_iso R Q" ``` lp15@68551 ` 851` ``` unfolding ring_iso_def using bij_betw_trans ring_hom_trans by fastforce ``` lp15@68551 ` 852` lp15@68551 ` 853` ```corollary ring_iso_trans: "\ R \ S; S \ Q \ \ R \ Q" ``` lp15@68551 ` 854` ``` using ring_iso_set_trans unfolding is_ring_iso_def by blast ``` lp15@68551 ` 855` lp15@68551 ` 856` ```lemma ring_iso_set_sym: ``` lp15@68551 ` 857` ``` assumes "ring R" ``` lp15@68551 ` 858` ``` shows "h \ ring_iso R S \ (inv_into (carrier R) h) \ ring_iso S R" ``` lp15@68551 ` 859` ```proof - ``` lp15@68551 ` 860` ``` assume h: "h \ ring_iso R S" ``` lp15@68551 ` 861` ``` hence h_hom: "h \ ring_hom R S" ``` lp15@68551 ` 862` ``` and h_surj: "h ` (carrier R) = (carrier S)" ``` lp15@68551 ` 863` ``` and h_inj: "\ x1 x2. \ x1 \ carrier R; x2 \ carrier R \ \ h x1 = h x2 \ x1 = x2" ``` lp15@68551 ` 864` ``` unfolding ring_iso_def bij_betw_def inj_on_def by auto ``` lp15@68551 ` 865` lp15@68551 ` 866` ``` have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)" ``` lp15@68551 ` 867` ``` using bij_betw_inv_into h ring_iso_def by fastforce ``` lp15@68551 ` 868` lp15@68551 ` 869` ``` show "inv_into (carrier R) h \ ring_iso S R" ``` lp15@68551 ` 870` ``` apply (rule ring_iso_memI) ``` lp15@68551 ` 871` ``` apply (simp add: h_surj inv_into_into) ``` lp15@68551 ` 872` ``` apply (auto simp add: h_inv_bij) ``` lp15@68551 ` 873` ``` apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into ``` lp15@68551 ` 874` ``` ring.ring_simprules(5) ring_hom_closed ring_hom_mult) ``` lp15@68551 ` 875` ``` apply (smt assms f_inv_into_f h_hom h_inj h_surj inv_into_into ``` lp15@68551 ` 876` ``` ring.ring_simprules(1) ring_hom_add ring_hom_closed) ``` lp15@68551 ` 877` ``` by (metis (no_types, hide_lams) assms f_inv_into_f h_hom h_inj ``` lp15@68551 ` 878` ``` imageI inv_into_into ring.ring_simprules(6) ring_hom_one) ``` lp15@68551 ` 879` ```qed ``` lp15@68551 ` 880` lp15@68551 ` 881` ```corollary ring_iso_sym: ``` lp15@68551 ` 882` ``` assumes "ring R" ``` lp15@68551 ` 883` ``` shows "R \ S \ S \ R" ``` lp15@68551 ` 884` ``` using assms ring_iso_set_sym unfolding is_ring_iso_def by auto ``` lp15@68551 ` 885` lp15@68551 ` 886` ```lemma (in ring_hom_ring) the_elem_simp [simp]: ``` lp15@68551 ` 887` ``` "\x. x \ carrier R \ the_elem (h ` ((a_kernel R S h) +> x)) = h x" ``` lp15@68551 ` 888` ```proof - ``` lp15@68551 ` 889` ``` fix x assume x: "x \ carrier R" ``` lp15@68551 ` 890` ``` hence "h x \ h ` ((a_kernel R S h) +> x)" ``` lp15@68551 ` 891` ``` using homeq_imp_rcos by blast ``` lp15@68551 ` 892` ``` thus "the_elem (h ` ((a_kernel R S h) +> x)) = h x" ``` lp15@68551 ` 893` ``` by (metis (no_types, lifting) x empty_iff homeq_imp_rcos rcos_imp_homeq the_elem_image_unique) ``` lp15@68551 ` 894` ```qed ``` lp15@68551 ` 895` lp15@68551 ` 896` ```lemma (in ring_hom_ring) the_elem_inj: ``` lp15@68551 ` 897` ``` "\X Y. \ X \ carrier (R Quot (a_kernel R S h)); Y \ carrier (R Quot (a_kernel R S h)) \ \ ``` lp15@68551 ` 898` ``` the_elem (h ` X) = the_elem (h ` Y) \ X = Y" ``` lp15@68551 ` 899` ```proof - ``` lp15@68551 ` 900` ``` fix X Y ``` lp15@68551 ` 901` ``` assume "X \ carrier (R Quot (a_kernel R S h))" ``` lp15@68551 ` 902` ``` and "Y \ carrier (R Quot (a_kernel R S h))" ``` lp15@68551 ` 903` ``` and Eq: "the_elem (h ` X) = the_elem (h ` Y)" ``` lp15@68551 ` 904` ``` then obtain x y where x: "x \ carrier R" "X = (a_kernel R S h) +> x" ``` lp15@68551 ` 905` ``` and y: "y \ carrier R" "Y = (a_kernel R S h) +> y" ``` lp15@68551 ` 906` ``` unfolding FactRing_def A_RCOSETS_def' by auto ``` lp15@68551 ` 907` ``` hence "h x = h y" using Eq by simp ``` lp15@68551 ` 908` ``` hence "x \ y \ (a_kernel R S h)" ``` lp15@68551 ` 909` ``` by (simp add: a_minus_def abelian_subgroup.a_rcos_module_imp ``` lp15@68551 ` 910` ``` abelian_subgroup_a_kernel homeq_imp_rcos x(1) y(1)) ``` lp15@68551 ` 911` ``` thus "X = Y" ``` lp15@68551 ` 912` ``` by (metis R.a_coset_add_inv1 R.minus_eq abelian_subgroup.a_rcos_const ``` lp15@68551 ` 913` ``` abelian_subgroup_a_kernel additive_subgroup.a_subset additive_subgroup_a_kernel x y) ``` lp15@68551 ` 914` ```qed ``` lp15@68551 ` 915` lp15@68551 ` 916` ```lemma (in ring_hom_ring) quot_mem: ``` lp15@68551 ` 917` ``` "\X. X \ carrier (R Quot (a_kernel R S h)) \ \x \ carrier R. X = (a_kernel R S h) +> x" ``` lp15@68551 ` 918` ```proof - ``` lp15@68551 ` 919` ``` fix X assume "X \ carrier (R Quot (a_kernel R S h))" ``` lp15@68551 ` 920` ``` thus "\x \ carrier R. X = (a_kernel R S h) +> x" ``` lp15@68551 ` 921` ``` unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (simp add: a_r_coset_def) ``` lp15@68551 ` 922` ```qed ``` lp15@68551 ` 923` lp15@68551 ` 924` ```lemma (in ring_hom_ring) the_elem_wf: ``` lp15@68551 ` 925` ``` "\X. X \ carrier (R Quot (a_kernel R S h)) \ \y \ carrier S. (h ` X) = { y }" ``` lp15@68551 ` 926` ```proof - ``` lp15@68551 ` 927` ``` fix X assume "X \ carrier (R Quot (a_kernel R S h))" ``` lp15@68551 ` 928` ``` then obtain x where x: "x \ carrier R" and X: "X = (a_kernel R S h) +> x" ``` lp15@68551 ` 929` ``` using quot_mem by blast ``` lp15@68551 ` 930` ``` hence "\x'. x' \ X \ h x' = h x" ``` lp15@68551 ` 931` ``` proof - ``` lp15@68551 ` 932` ``` fix x' assume "x' \ X" hence "x' \ (a_kernel R S h) +> x" using X by simp ``` lp15@68551 ` 933` ``` then obtain k where k: "k \ a_kernel R S h" "x' = k \ x" ``` lp15@68551 ` 934` ``` by (metis R.add.inv_closed R.add.m_assoc R.l_neg R.r_zero ``` lp15@68551 ` 935` ``` abelian_subgroup.a_elemrcos_carrier ``` lp15@68551 ` 936` ``` abelian_subgroup.a_rcos_module_imp abelian_subgroup_a_kernel x) ``` lp15@68551 ` 937` ``` hence "h x' = h k \\<^bsub>S\<^esub> h x" ``` lp15@68551 ` 938` ``` by (meson additive_subgroup.a_Hcarr additive_subgroup_a_kernel hom_add x) ``` lp15@68551 ` 939` ``` also have " ... = h x" ``` lp15@68551 ` 940` ``` using k by (auto simp add: x) ``` lp15@68551 ` 941` ``` finally show "h x' = h x" . ``` lp15@68551 ` 942` ``` qed ``` lp15@68551 ` 943` ``` moreover have "h x \ h ` X" ``` lp15@68551 ` 944` ``` by (simp add: X homeq_imp_rcos x) ``` lp15@68551 ` 945` ``` ultimately have "(h ` X) = { h x }" ``` lp15@68551 ` 946` ``` by blast ``` lp15@68551 ` 947` ``` thus "\y \ carrier S. (h ` X) = { y }" using x by simp ``` lp15@68551 ` 948` ```qed ``` lp15@68551 ` 949` lp15@68551 ` 950` ```corollary (in ring_hom_ring) the_elem_wf': ``` lp15@68551 ` 951` ``` "\X. X \ carrier (R Quot (a_kernel R S h)) \ \r \ carrier R. (h ` X) = { h r }" ``` lp15@68551 ` 952` ``` using the_elem_wf by (metis quot_mem the_elem_eq the_elem_simp) ``` lp15@68551 ` 953` lp15@68551 ` 954` ```lemma (in ring_hom_ring) the_elem_hom: ``` lp15@68551 ` 955` ``` "(\X. the_elem (h ` X)) \ ring_hom (R Quot (a_kernel R S h)) S" ``` lp15@68551 ` 956` ```proof (rule ring_hom_memI) ``` lp15@68551 ` 957` ``` show "\x. x \ carrier (R Quot a_kernel R S h) \ the_elem (h ` x) \ carrier S" ``` lp15@68551 ` 958` ``` using the_elem_wf by fastforce ``` lp15@68551 ` 959` ``` ``` lp15@68551 ` 960` ``` show "the_elem (h ` \\<^bsub>R Quot a_kernel R S h\<^esub>) = \\<^bsub>S\<^esub>" ``` lp15@68551 ` 961` ``` unfolding FactRing_def using the_elem_simp[of "\\<^bsub>R\<^esub>"] by simp ``` lp15@68551 ` 962` lp15@68551 ` 963` ``` fix X Y ``` lp15@68551 ` 964` ``` assume "X \ carrier (R Quot a_kernel R S h)" ``` lp15@68551 ` 965` ``` and "Y \ carrier (R Quot a_kernel R S h)" ``` lp15@68551 ` 966` ``` then obtain x y where x: "x \ carrier R" "X = (a_kernel R S h) +> x" ``` lp15@68551 ` 967` ``` and y: "y \ carrier R" "Y = (a_kernel R S h) +> y" ``` lp15@68551 ` 968` ``` using quot_mem by blast ``` lp15@68551 ` 969` lp15@68551 ` 970` ``` have "X \\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \ y)" ``` lp15@68551 ` 971` ``` by (simp add: FactRing_def ideal.rcoset_mult_add kernel_is_ideal x y) ``` lp15@68551 ` 972` ``` thus "the_elem (h ` (X \\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \\<^bsub>S\<^esub> the_elem (h ` Y)" ``` lp15@68551 ` 973` ``` by (simp add: x y) ``` lp15@68551 ` 974` lp15@68551 ` 975` ``` have "X \\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \ y)" ``` lp15@68551 ` 976` ``` using ideal.rcos_ring_hom kernel_is_ideal ring_hom_add x y by fastforce ``` lp15@68551 ` 977` ``` thus "the_elem (h ` (X \\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \\<^bsub>S\<^esub> the_elem (h ` Y)" ``` lp15@68551 ` 978` ``` by (simp add: x y) ``` lp15@68551 ` 979` ```qed ``` lp15@68551 ` 980` lp15@68551 ` 981` ```lemma (in ring_hom_ring) the_elem_surj: ``` lp15@68551 ` 982` ``` "(\X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h)) = (h ` (carrier R))" ``` lp15@68551 ` 983` ```proof ``` lp15@68551 ` 984` ``` show "(\X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h) \ h ` carrier R" ``` lp15@68551 ` 985` ``` using the_elem_wf' by fastforce ``` lp15@68551 ` 986` ```next ``` lp15@68551 ` 987` ``` show "h ` carrier R \ (\X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h)" ``` lp15@68551 ` 988` ``` proof ``` lp15@68551 ` 989` ``` fix y assume "y \ h ` carrier R" ``` lp15@68551 ` 990` ``` then obtain x where x: "x \ carrier R" "h x = y" ``` lp15@68551 ` 991` ``` by (metis image_iff) ``` lp15@68551 ` 992` ``` hence "the_elem (h ` ((a_kernel R S h) +> x)) = y" by simp ``` lp15@68551 ` 993` ``` moreover have "(a_kernel R S h) +> x \ carrier (R Quot (a_kernel R S h))" ``` lp15@68551 ` 994` ``` unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (auto simp add: x a_r_coset_def) ``` lp15@68551 ` 995` ``` ultimately show "y \ (\X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h))" by blast ``` lp15@68551 ` 996` ``` qed ``` lp15@68551 ` 997` ```qed ``` lp15@68551 ` 998` lp15@68551 ` 999` ```proposition (in ring_hom_ring) FactRing_iso_set_aux: ``` lp15@68551 ` 1000` ``` "(\X. the_elem (h ` X)) \ ring_iso (R Quot (a_kernel R S h)) (S \ carrier := h ` (carrier R) \)" ``` lp15@68551 ` 1001` ```proof - ``` lp15@68551 ` 1002` ``` have "bij_betw (\X. the_elem (h ` X)) (carrier (R Quot a_kernel R S h)) (h ` (carrier R))" ``` lp15@68551 ` 1003` ``` unfolding bij_betw_def inj_on_def using the_elem_surj the_elem_inj by simp ``` lp15@68551 ` 1004` lp15@68551 ` 1005` ``` moreover ``` lp15@68551 ` 1006` ``` have "(\X. the_elem (h ` X)): carrier (R Quot (a_kernel R S h)) \ h ` (carrier R)" ``` lp15@68551 ` 1007` ``` using the_elem_wf' by fastforce ``` lp15@68551 ` 1008` ``` hence "(\X. the_elem (h ` X)) \ ring_hom (R Quot (a_kernel R S h)) (S \ carrier := h ` (carrier R) \)" ``` lp15@68551 ` 1009` ``` using the_elem_hom the_elem_wf' unfolding ring_hom_def by simp ``` lp15@68551 ` 1010` lp15@68551 ` 1011` ``` ultimately show ?thesis unfolding ring_iso_def using the_elem_hom by simp ``` lp15@68551 ` 1012` ```qed ``` lp15@68551 ` 1013` lp15@68551 ` 1014` ```theorem (in ring_hom_ring) FactRing_iso_set: ``` lp15@68551 ` 1015` ``` assumes "h ` carrier R = carrier S" ``` lp15@68551 ` 1016` ``` shows "(\X. the_elem (h ` X)) \ ring_iso (R Quot (a_kernel R S h)) S" ``` lp15@68551 ` 1017` ``` using FactRing_iso_set_aux assms by auto ``` lp15@68551 ` 1018` lp15@68551 ` 1019` ```corollary (in ring_hom_ring) FactRing_iso: ``` lp15@68551 ` 1020` ``` assumes "h ` carrier R = carrier S" ``` lp15@68551 ` 1021` ``` shows "R Quot (a_kernel R S h) \ S" ``` lp15@68551 ` 1022` ``` using FactRing_iso_set assms is_ring_iso_def by auto ``` lp15@68551 ` 1023` lp15@68551 ` 1024` ```lemma (in ring_hom_ring) img_is_ring: "ring (S \ carrier := h ` (carrier R) \)" ``` lp15@68551 ` 1025` ```proof - ``` lp15@68551 ` 1026` ``` let ?the_elem = "\X. the_elem (h ` X)" ``` lp15@68551 ` 1027` ``` have FactRing_is_ring: "ring (R Quot (a_kernel R S h))" ``` lp15@68551 ` 1028` ``` by (simp add: ideal.quotient_is_ring kernel_is_ideal) ``` lp15@68551 ` 1029` ``` have "ring ((S \ carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \) ``` lp15@68551 ` 1030` ``` \ one := ?the_elem \\<^bsub>(R Quot (a_kernel R S h))\<^esub>, ``` lp15@68551 ` 1031` ``` zero := ?the_elem \\<^bsub>(R Quot (a_kernel R S h))\<^esub> \)" ``` lp15@68551 ` 1032` ``` using ring.ring_iso_imp_img_ring[OF FactRing_is_ring, of ?the_elem ``` lp15@68551 ` 1033` ``` "S \ carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \"] ``` lp15@68551 ` 1034` ``` FactRing_iso_set_aux the_elem_surj by auto ``` lp15@68551 ` 1035` lp15@68551 ` 1036` ``` moreover ``` lp15@68551 ` 1037` ``` have "\ \ (a_kernel R S h)" ``` lp15@68551 ` 1038` ``` using a_kernel_def'[of R S h] by auto ``` lp15@68551 ` 1039` ``` hence "\ \ (a_kernel R S h) +> \" ``` lp15@68551 ` 1040` ``` using a_r_coset_def'[of R "a_kernel R S h" \] by force ``` lp15@68551 ` 1041` ``` hence "\\<^bsub>S\<^esub> \ (h ` ((a_kernel R S h) +> \))" ``` lp15@68551 ` 1042` ``` using hom_one by force ``` lp15@68551 ` 1043` ``` hence "?the_elem \\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \\<^bsub>S\<^esub>" ``` lp15@68551 ` 1044` ``` using the_elem_wf[of "(a_kernel R S h) +> \"] by (simp add: FactRing_def) ``` lp15@68551 ` 1045` ``` ``` lp15@68551 ` 1046` ``` moreover ``` lp15@68551 ` 1047` ``` have "\\<^bsub>S\<^esub> \ (h ` (a_kernel R S h))" ``` lp15@68551 ` 1048` ``` using a_kernel_def'[of R S h] hom_zero by force ``` lp15@68551 ` 1049` ``` hence "\\<^bsub>S\<^esub> \ (h ` \\<^bsub>(R Quot (a_kernel R S h))\<^esub>)" ``` lp15@68551 ` 1050` ``` by (simp add: FactRing_def) ``` lp15@68551 ` 1051` ``` hence "?the_elem \\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \\<^bsub>S\<^esub>" ``` lp15@68551 ` 1052` ``` using the_elem_wf[OF ring.ring_simprules(2)[OF FactRing_is_ring]] ``` lp15@68551 ` 1053` ``` by (metis singletonD the_elem_eq) ``` lp15@68551 ` 1054` lp15@68551 ` 1055` ``` ultimately ``` lp15@68551 ` 1056` ``` have "ring ((S \ carrier := h ` (carrier R) \) \ one := \\<^bsub>S\<^esub>, zero := \\<^bsub>S\<^esub> \)" ``` lp15@68551 ` 1057` ``` using the_elem_surj by simp ``` lp15@68551 ` 1058` ``` thus ?thesis ``` lp15@68551 ` 1059` ``` by auto ``` lp15@68551 ` 1060` ```qed ``` lp15@68551 ` 1061` lp15@68551 ` 1062` ```lemma (in ring_hom_ring) img_is_cring: ``` lp15@68551 ` 1063` ``` assumes "cring S" ``` lp15@68551 ` 1064` ``` shows "cring (S \ carrier := h ` (carrier R) \)" ``` lp15@68551 ` 1065` ```proof - ``` lp15@68551 ` 1066` ``` interpret ring "S \ carrier := h ` (carrier R) \" ``` lp15@68551 ` 1067` ``` using img_is_ring . ``` lp15@68551 ` 1068` ``` show ?thesis ``` lp15@68551 ` 1069` ``` apply unfold_locales ``` lp15@68551 ` 1070` ``` using assms unfolding cring_def comm_monoid_def comm_monoid_axioms_def by auto ``` lp15@68551 ` 1071` ```qed ``` lp15@68551 ` 1072` lp15@68551 ` 1073` ```lemma (in ring_hom_ring) img_is_domain: ``` lp15@68551 ` 1074` ``` assumes "domain S" ``` lp15@68551 ` 1075` ``` shows "domain (S \ carrier := h ` (carrier R) \)" ``` lp15@68551 ` 1076` ```proof - ``` lp15@68551 ` 1077` ``` interpret cring "S \ carrier := h ` (carrier R) \" ``` lp15@68551 ` 1078` ``` using img_is_cring assms unfolding domain_def by simp ``` lp15@68551 ` 1079` ``` show ?thesis ``` lp15@68551 ` 1080` ``` apply unfold_locales ``` lp15@68551 ` 1081` ``` using assms unfolding domain_def domain_axioms_def apply auto ``` lp15@68551 ` 1082` ``` using hom_closed by blast ``` lp15@68551 ` 1083` ```qed ``` lp15@68551 ` 1084` lp15@68551 ` 1085` ```proposition (in ring_hom_ring) primeideal_vimage: ``` lp15@68551 ` 1086` ``` assumes "cring R" ``` lp15@68551 ` 1087` ``` shows "primeideal P S \ primeideal { r \ carrier R. h r \ P } R" ``` lp15@68551 ` 1088` ```proof - ``` lp15@68551 ` 1089` ``` assume A: "primeideal P S" ``` lp15@68551 ` 1090` ``` hence is_ideal: "ideal P S" unfolding primeideal_def by simp ``` lp15@68551 ` 1091` ``` have "ring_hom_ring R (S Quot P) (((+>\<^bsub>S\<^esub>) P) \ h)" (is "ring_hom_ring ?A ?B ?h") ``` lp15@68551 ` 1092` ``` using ring_hom_trans[OF homh, of "(+>\<^bsub>S\<^esub>) P" "S Quot P"] ``` lp15@68551 ` 1093` ``` ideal.rcos_ring_hom_ring[OF is_ideal] assms ``` lp15@68551 ` 1094` ``` unfolding ring_hom_ring_def ring_hom_ring_axioms_def cring_def by simp ``` lp15@68551 ` 1095` ``` then interpret hom: ring_hom_ring R "S Quot P" "((+>\<^bsub>S\<^esub>) P) \ h" by simp ``` lp15@68551 ` 1096` ``` ``` lp15@68551 ` 1097` ``` have "inj_on (\X. the_elem (?h ` X)) (carrier (R Quot (a_kernel R (S Quot P) ?h)))" ``` lp15@68551 ` 1098` ``` using hom.the_elem_inj unfolding inj_on_def by simp ``` lp15@68551 ` 1099` ``` moreover ``` lp15@68551 ` 1100` ``` have "ideal (a_kernel R (S Quot P) ?h) R" ``` lp15@68551 ` 1101` ``` using hom.kernel_is_ideal by auto ``` lp15@68551 ` 1102` ``` have hom': "ring_hom_ring (R Quot (a_kernel R (S Quot P) ?h)) (S Quot P) (\X. the_elem (?h ` X))" ``` lp15@68551 ` 1103` ``` using hom.the_elem_hom hom.kernel_is_ideal ``` lp15@68551 ` 1104` ``` by (meson hom.ring_hom_ring_axioms ideal.rcos_ring_hom_ring ring_hom_ring_axioms_def ring_hom_ring_def) ``` lp15@68551 ` 1105` ``` ``` lp15@68551 ` 1106` ``` ultimately ``` lp15@68551 ` 1107` ``` have "primeideal (a_kernel R (S Quot P) ?h) R" ``` lp15@68551 ` 1108` ``` using ring_hom_ring.inj_on_domain[OF hom'] primeideal.quotient_is_domain[OF A] ``` lp15@68551 ` 1109` ``` cring.quot_domain_imp_primeideal[OF assms hom.kernel_is_ideal] by simp ``` lp15@68551 ` 1110` ``` ``` lp15@68551 ` 1111` ``` moreover have "a_kernel R (S Quot P) ?h = { r \ carrier R. h r \ P }" ``` lp15@68551 ` 1112` ``` proof ``` lp15@68551 ` 1113` ``` show "a_kernel R (S Quot P) ?h \ { r \ carrier R. h r \ P }" ``` lp15@68551 ` 1114` ``` proof ``` lp15@68551 ` 1115` ``` fix r assume "r \ a_kernel R (S Quot P) ?h" ``` lp15@68551 ` 1116` ``` hence r: "r \ carrier R" "P +>\<^bsub>S\<^esub> (h r) = P" ``` lp15@68551 ` 1117` ``` unfolding a_kernel_def kernel_def FactRing_def by auto ``` lp15@68551 ` 1118` ``` hence "h r \ P" ``` lp15@68551 ` 1119` ``` using S.a_rcosI R.l_zero S.l_zero additive_subgroup.a_subset[OF ideal.axioms(1)[OF is_ideal]] ``` lp15@68551 ` 1120` ``` additive_subgroup.zero_closed[OF ideal.axioms(1)[OF is_ideal]] hom_closed by metis ``` lp15@68551 ` 1121` ``` thus "r \ { r \ carrier R. h r \ P }" using r by simp ``` lp15@68551 ` 1122` ``` qed ``` lp15@68551 ` 1123` ``` next ``` lp15@68551 ` 1124` ``` show "{ r \ carrier R. h r \ P } \ a_kernel R (S Quot P) ?h" ``` lp15@68551 ` 1125` ``` proof ``` lp15@68551 ` 1126` ``` fix r assume "r \ { r \ carrier R. h r \ P }" ``` lp15@68551 ` 1127` ``` hence r: "r \ carrier R" "h r \ P" by simp_all ``` lp15@68551 ` 1128` ``` hence "?h r = P" ``` lp15@68551 ` 1129` ``` by (simp add: S.a_coset_join2 additive_subgroup.a_subgroup ideal.axioms(1) is_ideal) ``` lp15@68551 ` 1130` ``` thus "r \ a_kernel R (S Quot P) ?h" ``` lp15@68551 ` 1131` ``` unfolding a_kernel_def kernel_def FactRing_def using r(1) by auto ``` lp15@68551 ` 1132` ``` qed ``` lp15@68551 ` 1133` ``` qed ``` lp15@68551 ` 1134` ``` ultimately show "primeideal { r \ carrier R. h r \ P } R" by simp ``` lp15@68551 ` 1135` ```qed ``` lp15@68551 ` 1136` ballarin@20318 ` 1137` ```end ```