(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2022 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Rings - Ideals of quotient rings› theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_5 begin text‹This section studies the ideals of quotient rings, and defines ring homomorphisms.› subsection‹Ring homomorphisms› text‹Morphisms in general are structure preserving functions between algebraic structures. In this section we study ring homomorphisms.› text‹A ring homomorphism is a function between rings which has the morphism property with respect to both addition and multiplication operation, and maps one (the neutral element of multiplication) in the first ring to one in the second ring. › definition "ringHomomor(f,R,A,M,S,U,V) ≡ f:R→S ∧ IsMorphism(R,A,U,f) ∧ IsMorphism(R,M,V,f) ∧ f`(TheNeutralElement(R,M)) = TheNeutralElement(S,V)" text‹The next locale defines notation which we will use in this theory. We assume that we have two rings, one (which we will call the origin ring) defined by the triple $(R,A,M)$ and the second one (which we will call the target ring) by the triple $(S,U,V)$, and a homomorphism $f:R\rightarrow S$. › locale ring_homo = fixes R A M S U V f assumes origin: "IsAring(R,A,M)" and target: "IsAring(S,U,V)" and homomorphism: "ringHomomor(f,R,A,M,S,U,V)" fixes ringa (infixl "\<ra>⇩_{R}" 90) defines ringa_def [simp]: "x\<ra>⇩_{R}y ≡ A`⟨x,y⟩" fixes ringminus ("\<rm>⇩_{R}_" 89) defines ringminus_def [simp]: "(\<rm>⇩_{R}x) ≡ GroupInv(R,A)`(x)" fixes ringsub (infixl "\<rs>⇩_{R}" 90) defines ringsub_def [simp]: "x\<rs>⇩_{R}y ≡ x\<ra>⇩_{R}(\<rm>⇩_{R}y)" fixes ringm (infixl "⋅⇩_{R}" 95) defines ringm_def [simp]: "x⋅⇩_{R}y ≡ M`⟨x,y⟩" fixes ringzero ("𝟬⇩_{R}") defines ringzero_def [simp]: "𝟬⇩_{R}≡ TheNeutralElement(R,A)" fixes ringone ("𝟭⇩_{R}") defines ringone_def [simp]: "𝟭⇩_{R}≡ TheNeutralElement(R,M)" fixes ringtwo ("𝟮⇩_{R}") defines ringtwo_def [simp]: "𝟮⇩_{R}≡ 𝟭⇩_{R}\<ra>⇩_{R}𝟭⇩_{R}" fixes ringsq ("_⇧^{2}⇧^{R}" [96] 97) defines ringsq_def [simp]: "x⇧^{2}⇧^{R}≡ x⋅⇩_{R}x" fixes ringas (infixl "\<ra>⇩_{S}" 90) defines ringas_def [simp]: "x\<ra>⇩_{S}b ≡ U`⟨x,b⟩" fixes ringminuss ("\<rm>⇩_{S}_" 89) defines ringminuss_def [simp]: "(\<rm>⇩_{S}x) ≡ GroupInv(S,U)`(x)" fixes ringsubs (infixl "\<rs>⇩_{S}" 90) defines ringsubs_def [simp]: "x\<rs>⇩_{S}b ≡ x\<ra>⇩_{S}(\<rm>⇩_{S}b)" fixes ringms (infixl "⋅⇩_{S}" 95) defines ringms_def [simp]: "x⋅⇩_{S}b ≡ V`⟨ x,b⟩" fixes ringzeros ("𝟬⇩_{S}") defines ringzeros_def [simp]: "𝟬⇩_{S}≡ TheNeutralElement(S,U)" fixes ringones ("𝟭⇩_{S}") defines ringones_def [simp]: "𝟭⇩_{S}≡ TheNeutralElement(S,V)" fixes ringtwos ("𝟮⇩_{S}") defines ringtwos_def [simp]: "𝟮⇩_{S}≡ 𝟭⇩_{S}\<ra>⇩_{S}𝟭⇩_{S}" fixes ringsqs ("_⇧^{2}⇧^{S}" [96] 97) defines ringsqs_def [simp]: "x⇧^{2}⇧^{S}≡ x⋅⇩_{S}x" text‹We will write ‹I◃R⇩_{o}› to denote that $I$ is an ideal of the ring $R$. Note that in this notation the ‹R⇩_{o}› part by itself has no meaning, only the whole ‹◃R⇩_{o}› serves as postfix operator. › abbreviation (in ring_homo) ideal_origin ("_◃R⇩_{o}") where "I◃R⇩_{o}≡ ring0.Ideal(R,A,M,I)" text‹‹I◃R⇩_{t}› means that $I$ is an ideal of $S$.› abbreviation (in ring_homo) ideal_target ("_◃R⇩_{t}") where "I◃R⇩_{t}≡ ring0.Ideal(S,U,V,I)" text‹ ‹I◃⇩_{p}R⇩_{o}› means that $I$ is a prime ideal of $R$.› abbreviation (in ring_homo) prime_ideal_origin ("_◃⇩_{p}R⇩_{o}") where "I◃⇩_{p}R⇩_{o}≡ ring0.primeIdeal(R,A,M,I)" text‹We will write ‹I◃⇩_{p}R⇩_{t}› to denote that $I$ is a prime ideal of the ring $S$. › abbreviation (in ring_homo) prime_ideal_target ("_◃⇩_{p}R⇩_{t}") where "I◃⇩_{p}R⇩_{t}≡ ring0.primeIdeal(S,U,V,I)" text‹ ‹ker› denotes the kernel of $f$ (which is assumed to be a homomorphism between $R$ and $S$.› abbreviation (in ring_homo) kernel ("ker" 90) where "ker ≡ f-``{𝟬⇩_{S}}" text‹The theorems proven in the ‹ring0› context are valid in the ‹ring_homo› context when applied to the ring $R$.› sublocale ring_homo < origin_ring:ring0 using origin unfolding ring0_def by auto text‹The theorems proven in the ‹ring0› context are valid in the ‹ring_homo› context when applied to the ring $S$.› sublocale ring_homo < target_ring:ring0 S U V ringas ringminuss ringsubs ringms ringzeros ringones ringtwos ringsqs using target unfolding ring0_def by auto text‹A ring homomorphism is a homomorphism both with respect to addition and multiplication.› lemma ringHomHom: assumes "ringHomomor(f,R,A,M,S,U,V)" shows "Homomor(f,R,A,S,U)" and "Homomor(f,R,M,S,V)" using assms unfolding ringHomomor_def Homomor_def by simp_all text‹Since in the ‹ring_homo› locale $f$ is a ring homomorphism it implies that $f$ is a function from $R$ to $S$. › lemma (in ring_homo) f_is_fun: shows "f:R→S" using homomorphism unfolding ringHomomor_def by simp text‹In the ‹ring_homo› context $A$ is the addition in the first (source) ring $M$ is the multiplication there and $U,V$ are the addition and multiplication resp. in the second (target) ring. The next lemma states the all these are binary operations, a trivial, but frequently used fact.› lemma (in ring_homo) AMUV_are_ops: shows "A:R×R→R" "M:R×R→R" "U:S×S→S" "V:S×S→S" using origin target unfolding IsAring_def IsAgroup_def IsAmonoid_def IsAssociative_def by auto text‹The kernel is a subset of $R$ on which the value of $f$ is zero (of the target ring)› lemma (in ring_homo) kernel_def_alt: shows "ker = {r∈R. f`(r) = 𝟬⇩_{S}}" using f_is_fun func1_1_L14 by simp text‹ the homomorphism $f$ maps each element of the kernel to zero of the target ring. › lemma (in ring_homo) image_kernel: assumes "x∈ker" shows "f`(x) = 𝟬⇩_{S}" using assms func1_1_L15 f_is_fun by simp text‹ As a ring homomorphism $f$ preserves multiplication.› lemma (in ring_homo) homomor_dest_mult: assumes "x∈R" "y∈R" shows "f`(x⋅⇩_{R}y) = (f`(x))⋅⇩_{S}(f`(y))" using assms origin target homomorphism unfolding ringHomomor_def IsMorphism_def by simp text‹ As a ring homomorphism $f$ preserves addition. › lemma (in ring_homo) homomor_dest_add: assumes "x∈R" "y∈R" shows "f`(x\<ra>⇩_{R}y) = (f`(x))\<ra>⇩_{S}(f`(y))" using homomor_eq origin target homomorphism assms unfolding IsAring_def ringHomomor_def IsMorphism_def by simp text‹For $x\in R$ the value of $f$ is in $S$.› lemma (in ring_homo) homomor_val: assumes "x∈R" shows "f`(x) ∈ S" using homomorphism assms apply_funtype unfolding ringHomomor_def by blast text‹A ring homomorphism preserves taking negative of an element.› lemma (in ring_homo) homomor_dest_minus: assumes "x∈R" shows "f`(\<rm>⇩_{R}x) = \<rm>⇩_{S}(f`(x))" using origin target homomorphism assms ringHomHom image_inv unfolding IsAring_def by auto text‹A ring homomorphism preserves substraction.› lemma (in ring_homo) homomor_dest_subs: assumes "x∈R" "y∈R" shows "f`(x\<rs>⇩_{R}y) = (f`(x))\<rs>⇩_{S}(f`(y))" using assms homomor_dest_add homomor_dest_minus using origin_ring.Ring_ZF_1_L3(1) by auto text‹A ring homomorphism maps zero to zero.› lemma (in ring_homo) homomor_dest_zero: shows "f`(𝟬⇩_{R}) = 𝟬⇩_{S}" using origin target homomorphism ringHomHom(1) image_neutral unfolding IsAring_def by auto text‹The kernel of a homomorphism is never empty.› lemma (in ring_homo) kernel_non_empty: shows "𝟬⇩_{R}∈ker" and "ker≠0" using homomor_dest_zero origin_ring.Ring_ZF_1_L2(1) func1_1_L15 f_is_fun by auto text‹The image of the kernel by $f$ is the singleton $\{ 0_R\}$.› corollary (in ring_homo) image_kernel_2: shows "f``(ker) = {𝟬⇩_{S}}" proof - have "f:R→S" "ker⊆R" "ker≠0" "∀x∈ker. f`(x) = 𝟬⇩_{S}" using f_is_fun kernel_def_alt kernel_non_empty by auto then show "f``(ker) = {𝟬⇩_{S}}" using image_constant_singleton by simp qed text‹The inverse image of an ideal (in the target ring) is a normal subgroup of the addition group and an ideal in the origin ring. The kernel of the homomorphism is a subset of the inverse of image of every ideal. › lemma (in ring_homo) preimage_ideal: assumes "J◃R⇩_{t}" shows "IsAnormalSubgroup(R,A,f-``(J))" "(f-``(J))◃R⇩_{o}" "ker ⊆ f-``(J)" proof - from origin target homomorphism assms show "IsAnormalSubgroup(R,A,f-``(J))" using ringHomHom(1) preimage_normal_subgroup target_ring.ideal_normal_add_subgroup unfolding IsAring_def by blast then have "IsAsubgroup(f-``(J),A)" unfolding IsAnormalSubgroup_def by auto moreover { fix x y assume "x ∈ f-``(J)" "y∈R" from homomorphism have "f:R→S" unfolding ringHomomor_def by simp with ‹x ∈ f-``(J)› have "x∈R" and "f`(x) ∈ J" using func1_1_L15 unfolding ringHomomor_def by simp_all with assms ‹y∈R› ‹f:R→S› have "V`⟨f`(x),f`(y)⟩ ∈ J" and "V`⟨f`(y),f`(x)⟩∈J" using apply_funtype target_ring.ideal_dest_mult by simp_all with ‹x∈R› ‹y∈R› have "f`(M`⟨x,y⟩) ∈ J" and "f`(M`⟨y,x⟩) ∈ J" using homomor_dest_mult by auto with ‹x∈R› ‹y∈R› ‹f:R→S› have "M`⟨x,y⟩ ∈ f-``(J)" and "M`⟨y,x⟩ ∈ f-``(J)" using origin_ring.Ring_ZF_1_L4(3) func1_1_L15 by auto } ultimately show "(f-``(J))◃R⇩_{o}" using origin_ring.Ideal_def by auto from assms show "ker ⊆ f-``(J)" using target_ring.ideal_dest_zero by auto qed text‹Kernel of the homomorphism in an ideal.› lemma (in ring_homo) kernel_ideal: shows "ker ◃R⇩_{o}" using target_ring.zero_ideal preimage_ideal(2) by simp text‹The inverse image of a prime ideal by a homomorphism is not the whole ring. Proof by contradiction.› lemma (in ring_homo) vimage_prime_ideal_not_all: assumes "J◃⇩_{p}R⇩_{t}" shows "f-``(J) ≠ R" proof - { assume "R = f-``(J)" then have "R = {x∈R. f`(x)∈J}" using f_is_fun func1_1_L15 by simp then have "𝟭⇩_{R}∈ {x∈R. f`(x)∈J}" using origin_ring.Ring_ZF_1_L2(2) by simp with origin_ring.ringAssum target_ring.ringAssum homomorphism assms have False using target_ring.ideal_with_one unfolding target_ring.primeIdeal_def ringHomomor_def by auto } thus "f-``(J) ≠ R" by blast qed text‹Even more, if the target ring of the homomorphism is commutative and the ideal is prime then its preimage is also. Note that this is not true in general.› lemma (in ring_homo) preimage_prime_ideal_comm: assumes "J◃⇩_{p}R⇩_{t}" "V {is commutative on} S" shows "(f-``(J))◃⇩_{p}R⇩_{o}" proof - have "∀x∈R. ∀y∈R. (∀z∈R. x⋅⇩_{R}z⋅⇩_{R}y ∈ f-``(J)) ⟶ x∈f-``(J) ∨ y∈f-``( J)" proof - { fix x y assume "x∈R" "y∈R" and as: "∀z∈R. x⋅⇩_{R}z⋅⇩_{R}y ∈ f-``(J)" and "y ∉ f-``(J)" { fix s assume "s∈S" with assms(2) ‹x∈R› ‹y∈R› have "(f`(x))⋅⇩_{S}s⋅⇩_{S}(f`(y)) = s⋅⇩_{S}((f`(x))⋅⇩_{S}(f`(y)))" using f_is_fun apply_funtype target_ring.Ring_ZF_1_L11(2) unfolding IsCommutative_def by auto with ‹x∈R› ‹y∈R› have "(f`x)⋅⇩_{S}s⋅⇩_{S}(f`y) = s⋅⇩_{S}(f`(x⋅⇩_{R}y))" using homomor_dest_mult by simp with assms(1) ‹s∈S› ‹x∈R› as have "(f`(x))⋅⇩_{S}s⋅⇩_{S}(f`(y)) ∈ J" using origin_ring.Ring_ZF_1_L2(2) origin_ring.Ring_ZF_1_L3(5) func1_1_L15 f_is_fun target_ring.ideal_dest_mult(2) unfolding target_ring.primeIdeal_def by auto } hence "∀z∈S. (f`x) ⋅⇩_{S}z ⋅⇩_{S}(f`y) ∈ J" by simp with assms(1) ‹x∈R› ‹y∈R› have "f`(x)∈ J ∨ f`(y)∈J" using target_ring.equivalent_prime_ideal f_is_fun apply_funtype by simp with ‹x∈R› ‹y∈R› ‹y ∉ f-``(J)› have "x∈f-``(J)" using func1_1_L15 f_is_fun by simp } thus ?thesis by blast qed moreover from assms have "(f-``J)◃R⇩_{o}" using preimage_ideal unfolding target_ring.primeIdeal_def by auto moreover from assms(1) have "f-``(J) ≠ R" using vimage_prime_ideal_not_all by simp ultimately show "(f-``(J))◃⇩_{p}R⇩_{o}" by (rule origin_ring.equivalent_prime_ideal_2) qed text‹We can replace the assumption that the target ring of the homomorphism is commutative with the assumption that homomorphism is surjective in ‹preimage_prime_ideal_comm› above and we can show the same assertion that the preimage of a prime ideal prime. › lemma (in ring_homo) preimage_prime_ideal_surj: assumes "J◃⇩_{p}R⇩_{t}" "f ∈ surj(R,S)" shows "(f-``(J))◃⇩_{p}R⇩_{o}" proof - have "∀x∈R. ∀y∈R. (∀z∈R. x⋅⇩_{R}z⋅⇩_{R}y ∈ f-``(J)) ⟶ x∈f-``(J) ∨ y∈f-``(J)" proof - { fix x y assume "x∈R" "y∈R" and as: "∀z∈R. x⋅⇩_{R}z⋅⇩_{R}y ∈ f-``(J)" and "y ∉ f-``(J)" { fix s assume s: "s∈S" with assms(2) obtain t where "s=f`(t)" "t∈R" unfolding surj_def by auto with ‹x∈R› ‹y∈R› as have "(f`x)⋅⇩_{S}s⋅⇩_{S}(f`y)∈J" using homomor_dest_mult origin_ring.Ring_ZF_1_L4(3) func1_1_L15 f_is_fun by simp } hence "∀z∈S. (f`(x)) ⋅⇩_{S}z ⋅⇩_{S}(f`(y)) ∈ J" by simp with target_ring.equivalent_prime_ideal assms(1) ‹x∈R› ‹y∈R› have "f`(x)∈J∨f`(y)∈J" using f_is_fun apply_funtype by auto with ‹x∈R› ‹y∈R› ‹y ∉ f-``(J)› have "x∈f-``(J)" using func1_1_L15 f_is_fun by auto } thus ?thesis by blast qed moreover from assms have "(f-``(J))◃R⇩_{o}" using preimage_ideal unfolding target_ring.primeIdeal_def by auto moreover from assms(1) have "f-``(J) ≠ R" using vimage_prime_ideal_not_all by simp ultimately show "(f-``(J))◃⇩_{p}R⇩_{o}" by (rule origin_ring.equivalent_prime_ideal_2) qed subsection‹Quotient ring with quotient map› text‹The notion of a quotient ring (a.k.a factor ring, difference ring or residue class) is analogous to the notion of quotient group from the group theory. › text‹The next locale ‹ring2› extends the ‹ring0› locale (defined in the ‹Ring_ZF› theory) with the assumption that some fixed set $I$ is an ideal. It also defines some notation related to quotient rings, in particular we define the function (projection) $f_I$ that maps each element $r$ of the ring $R$ to its class $r_I(\{ r\}$ where $r_I$ is the quotient group relation defined by $I$ as a (normal) subgroup of $R$ with addition. › locale ring2 = ring0 + fixes I assumes idealAssum: "I◃R" fixes quot ("R⇩_{I}") defines quot_def [simp]: "R⇩_{I}≡ QuotientBy(I)" fixes qrel ("r⇩_{I}") defines qrel_def [simp]: "r⇩_{I}≡ QuotientGroupRel(R,A,I)" fixes qfun ("f⇩_{I}") defines qfun_def [simp]: "f⇩_{I}≡ λr∈R. r⇩_{I}``{r}" fixes qadd ("A⇩_{I}") defines qadd_def [simp]: "A⇩_{I}≡ QuotientGroupOp(R, A, I)" fixes qmul ("M⇩_{I}") defines qmul_def [simp]: "M⇩_{I}≡ ProjFun2(R, qrel, M)" text‹The expression ‹J◃R⇩_{I}› will mean that $J$ is an ideal of the quotient ring $R_I$ (with the quotient addition and multiplication).› abbreviation (in ring2) qideal ("_◃R⇩_{I}") where "J◃R⇩_{I}≡ ring0.Ideal(R⇩_{I},A⇩_{I},M⇩_{I},J)" text‹In the ‹ring2› The expression ‹J◃⇩_{p}R⇩_{I}› means that $J$ is a prime ideal of the quotient ring $R_I$. › abbreviation (in ring2) qprimeIdeal ("_◃⇩_{p}R⇩_{I}") where "J◃⇩_{p}R⇩_{I}≡ ring0.primeIdeal(R⇩_{I},A⇩_{I},M⇩_{I},J)" text‹Theorems proven in the ‹ring0› context can be applied to the quotient ring in the ‹ring2› context. › sublocale ring2 < quotient_ring: ring0 quot qadd qmul "λx y. ideal_radd(x,I,y)" "λy. ideal_rmin(I,y)" "λx y. ideal_rsub(x,I,y)" "λx y. ideal_rmult(x,I,y)" "𝟬⇩I" "𝟭⇩I" "𝟮⇩I" "λx. (x⇧^{2}⇧I)" using quotientBy_is_ring idealAssum neutral_quotient one_quotient two_quotient unfolding ring0_def ideal_radd_def ideal_rmin_def ideal_rsub_def ideal_rmult_def ideal_rzero_def ideal_rone_def ideal_rtwo_def ideal_rsqr_def by auto text‹The quotient map is a homomorphism of rings. This is probably one of the most sophisticated facts in IsarMathlib that Isabelle's simp method proves from 10 facts and 5 definitions. › theorem (in ring2) quotient_fun_homomor: shows "ringHomomor(f⇩_{I},R,A,M,R⇩_{I},A⇩_{I},M⇩_{I})" using ringAssum idealAssum ideal_normal_add_subgroup add_group.quotient_map Ring_ZF_1_L4(3) EquivClass_1_L10 Ring_ZF_1_L2(2) Group_ZF_2_2_L1 ideal_equiv_rel quotientBy_mul_monoid(1) QuotientBy_def unfolding IsAring_def Homomor_def IsMorphism_def ringHomomor_def by simp text‹The quotient map is surjective› lemma (in ring2) quot_fun: shows "f⇩_{I}∈surj(R,R⇩_{I})" using lam_funtype idealAssum QuotientBy_def unfolding quotient_def surj_def by auto text‹The theorems proven in the ‹ring_homo› context are valid in the ‹ring_homo› context when applied to the quotient ring as the second (target) ring and the quotient map as the ring homomorphism.› sublocale ring2 < quot_homomorphism: ring_homo R A M quot qadd qmul qfun _ _ _ _ _ _ _ _ "λx y. ideal_radd(x,I,y)" "λy. ideal_rmin(I,y)" "λx y. ideal_rsub(x,I,y)" "λx y. ideal_rmult(x,I,y)" "𝟬⇩I" "𝟭⇩I" "𝟮⇩I" "λx. (x⇧^{2}⇧I)" using ringAssum quotient_ring.ringAssum quotient_fun_homomor unfolding ring_homo_def by simp_all text‹The ideal we divide by is the kernel of the quotient map.› lemma (in ring2) quotient_kernel: shows "quot_homomorphism.kernel = I" proof from idealAssum show "quot_homomorphism.kernel ⊆ I" using add_group.Group_ZF_2_4_L5E ideal_normal_add_subgroup neutral_quotient QuotientBy_def quot_homomorphism.image_kernel func1_1_L15 unfolding ideal_rzero_def QuotientBy_def by auto { fix t assume "t∈I" then have "t∈R" using ideal_dest_subset idealAssum by auto with idealAssum ‹t∈I› have "t ∈ f⇩_{I}-``{𝟬⇩I}" using add_group.Group_ZF_2_4_L5E ideal_normal_add_subgroup neutral_quotient QuotientBy_def func1_1_L15 surj_is_fun unfolding ideal_rzero_def by auto } thus "I ⊆ quot_homomorphism.kernel" by blast qed text‹The theorems proven in the ‹ring0› context are valid in the ‹ring 2› context when applied to the quotient ring.› sublocale ring2 < quotient_ring: ring0 quot qadd qmul "λx y. ideal_radd(x,I,y)" "λy. ideal_rmin(I,y)" "λx y. ideal_rsub(x,I,y)" "λx y. ideal_rmult(x,I,y)" "𝟬⇩I" "𝟭⇩I" "𝟮⇩I" "λx. (x⇧^{2}⇧I)" using idealAssum quotientBy_is_ring neutral_quotient one_quotient two_quotient unfolding ring0_def by simp_all text‹If an ideal $I$ is a subset of the kernel of the homomorphism then the image of the ideal generated by $I\cup J$, where $J$ is another ideal, is the same as the image of $J$. Note that ‹J+⇩_{I}I› notation means the ideal generated by the union of ideals $J$ and $J$, see the definitions of ‹sumIdeal› and ‹generatedIdeal› in the ‹Ring_ZF_2› theory, and also corollary ‹sum_ideals_is_sum_elements› for an alternative definition. › theorem (in ring_homo) kernel_empty_image: assumes "J◃R" "I ⊆ ker" "I◃R" shows "f``(J+⇩_{I}I) = f``(J)" "f``(I+⇩_{I}J) = f``(J)" proof- from assms(1,3) have "J+⇩_{I}I ⊆ R" using origin_ring.sum_ideals_is_ideal origin_ring.ideal_dest_subset by auto show "f``(J+⇩_{I}I) = f``(J)" proof { fix t assume "t∈f``(J+⇩_{I}I)" with ‹J+⇩_{I}I ⊆ R› obtain q where q: "q ∈ J+⇩_{I}I" "t=f`(q)" using func_imagedef f_is_fun by auto with assms(1,3) ‹q ∈ J+⇩_{I}I› have "q∈A``(J×I)" "J×I ⊆ R×R" using origin_ring.sum_ideals_is_sum_elements assms(1,3) origin_ring.ideal_dest_subset by auto from origin_ring.add_group.groupAssum ‹J×I ⊆ R×R› have "A``(J×I) = {A`(p). p∈J×I}" unfolding IsAgroup_def IsAmonoid_def IsAssociative_def using func_imagedef by auto with ‹q∈A``(J×I)› obtain q⇩_{j}q⇩_{i}where "q⇩_{j}∈J" "q⇩_{i}∈I" "q=q⇩_{j}\<ra>⇩_{R}q⇩_{i}" by auto with assms have "f`(q) = (f`(q⇩_{j})) \<ra>⇩_{S}𝟬⇩_{S}" using homomor_dest_add origin_ring.ideal_dest_subset image_kernel by blast moreover from assms(1) ‹q⇩_{j}∈J› have "f`(q⇩_{j}) ∈ S" using origin_ring.ideal_dest_subset f_is_fun apply_funtype by blast ultimately have "f`(q) = f`(q⇩_{j})" using target_ring.Ring_ZF_1_L3(3) by auto with assms ‹t=f`(q)› ‹q⇩_{j}∈J› have "t ∈ f``(J)" using func_imagedef f_is_fun origin_ring.ideal_dest_subset by auto } thus "f``(J+⇩_{I}I) ⊆ f``(J)" by blast { fix t assume "t∈f``(J)" with assms(1) obtain q where q:"q∈J" "t=f`(q)" using func_imagedef f_is_fun origin_ring.ideal_dest_subset by auto from ‹q∈J› have "q∈J∪I" by auto moreover from assms(1,3) have "J∪I ⊆ R" using origin_ring.ideal_dest_subset by auto ultimately have "q∈⟨J∪I⟩⇩_{I}" using origin_ring.generated_ideal_contains_set by auto with assms(1,3) ‹J+⇩_{I}I ⊆ R› ‹t=f`(q)› have "t∈f``(J+⇩_{I}I)" using origin_ring.sumIdeal_def f_is_fun func_imagedef by auto } thus "f``(J) ⊆ f``(J+⇩_{I}I)" by auto qed with assms(1,3) show "f ``(I+⇩_{I}J) = f``(J)" using origin_ring.sum_ideals_commute by auto qed subsection‹Quotient ideals› text‹If we have an ideal $J$ in a ring $R$, and another ideal $I$ contained in J, then we can form the quotient ideal J/I whose elements are of the form $a + I$ where $a$ is an element of $J$.› text‹The preimage of an ideal is an ideal, so it applies to the quotient map; but the preimage ideal contains the quotient ideal.› lemma (in ring2) ideal_quot_preimage: assumes "J◃R⇩_{I}" shows "(f⇩_{I}-``(J)) ◃R" "I ⊆ f⇩_{I}-``(J)" proof - from assms quot_homomorphism.preimage_ideal show "(f⇩_{I}-``(J)) ◃R" by simp { fix x assume x: "x∈I" with idealAssum have "x∈R" using ideal_dest_subset by auto from assms ‹x∈I› have "f⇩_{I}`(x) ∈ J" using quotient_kernel quot_homomorphism.image_kernel quotient_ring.ideal_dest_zero by simp with ‹x∈R› have "x∈f⇩_{I}-``(J)" using quot_homomorphism.f_is_fun func1_1_L15 by simp } thus "I ⊆ f⇩_{I}-``(J)" by auto qed text‹Since the map is surjective, the image is also an ideal› lemma (in ring_homo) image_ideal_surj: assumes "J◃R⇩_{o}" "f∈surj(R,S)" shows "(f``(J)) ◃R⇩_{t}" proof - from assms homomorphism target_ring.ringAssum origin_ring.ringAssum have "IsAsubgroup(f``(J),U)" using ringHomHom(1) image_subgroup f_is_fun unfolding IsAring_def origin_ring.Ideal_def by blast moreover { fix x y assume "x∈f``(J)" "y∈S" from assms(1) ‹x∈f``(J)› obtain j where "x=f`(j)" "j∈J" using func_imagedef f_is_fun origin_ring.ideal_dest_subset by auto from assms ‹y∈S› ‹j∈J› have "j∈R" and "y∈f``(R)" using origin_ring.ideal_dest_subset surj_range_image_domain by auto with assms(1) obtain s where "y=f`(s)" "s∈R" using func_imagedef origin_ring.ideal_dest_subset f_is_fun by auto with assms(1) ‹j∈R› ‹x=f`(j)› ‹x∈f``(J)› have "V`⟨x,y⟩ = f`(M`⟨j,s⟩)" and "V`⟨y,x⟩ = f`(M`⟨s,j⟩)" using homomor_dest_mult origin_ring.ideal_dest_subset by auto with assms(1) ‹j∈J› ‹s∈R› have "(x⋅⇩_{S}y)∈f``(J)" and "(y⋅⇩_{S}x)∈f``J" using origin_ring.ideal_dest_mult func_imagedef f_is_fun origin_ring.ideal_dest_subset by auto } hence "∀x∈f``(J). ∀y∈S. (y⋅⇩_{S}x) ∈ f``(J) ∧ (x⋅⇩_{S}y) ∈ f``(J)" by auto ultimately show ?thesis unfolding target_ring.Ideal_def by simp qed text‹If the homomorphism is a surjection and given two ideals in the target ring the inverse image of their product ideal is the sum ideal of the product ideal of their inverse images and the kernel of the homomorphism.› corollary (in ring_homo) prime_ideal_quot: assumes "J◃R⇩_{t}" "K◃R⇩_{t}" "f∈surj(R,S)" shows "f-``(target_ring.productIdeal(J, K)) = origin_ring.sumIdeal(origin_ring.productIdeal((f-``(J)),(f-``(K))), ker)" proof let ?P = "origin_ring.sumIdeal(origin_ring.productIdeal((f-``(J)),(f-``(K))), f-``{𝟬⇩_{S}})" let ?Q = "target_ring.productIdeal(J, K)" from assms(1,2) have ideals: "(f-``(J)) ◃R⇩_{o}" "(f-``(K)) ◃R⇩_{o}" using preimage_ideal by auto then have idealJK: "((f-``(J))⋅⇩_{I}(f-``(K))) ◃R⇩_{o}" using origin_ring.product_in_intersection(2) by auto then have "?P ◃R⇩_{o}" and "?P⊆R" using kernel_ideal origin_ring.sum_ideals_is_ideal origin_ring.ideal_dest_subset by simp_all with assms(3) have "(f``(?P)) ◃R⇩_{t}" using image_ideal_surj by simp let ?X = "((f-``(J)) ⋅⇩_{I}(f-``(K)))∪(f-``{𝟬⇩_{S}})" from assms(3) idealJK have "?X ⊆ R" using func1_1_L6A surj_is_fun origin_ring.ideal_dest_subset by blast with idealJK have "?X ⊆ ?P" using kernel_ideal origin_ring.sumIdeal_def origin_ring.generated_ideal_contains_set by simp { fix t assume "t∈V ``(J×K)" moreover from assms have "J×K ⊆ S×S" using target_ring.ideal_dest_subset by blast ultimately obtain j k where "j∈J" "k∈K" "t=V`⟨j,k⟩" using func_imagedef AMUV_are_ops(4) by auto from assms(1) ‹j∈J› have "j∈S" using target_ring.ideal_dest_subset by blast with assms(3) obtain j⇩_{0}where "j⇩_{0}∈R" "f`(j⇩_{0}) = j" unfolding surj_def by auto with assms(2,3) ‹k∈K› obtain k⇩_{0}where "k⇩_{0}∈R" "f`(k⇩_{0}) = k" using target_ring.ideal_dest_subset unfolding surj_def by blast with ‹t=V`⟨j,k⟩› ‹f`(j⇩_{0}) = j› ‹j⇩_{0}∈R› have "t=f`(M`⟨j⇩_{0},k⇩_{0}⟩)" using homomor_dest_mult by simp from assms(3) have "(f-``(J))×(f-``(K)) ⊆ R×R" using func1_1_L6A f_is_fun by blast moreover from assms(3) ‹j⇩_{0}∈R› ‹f`(j⇩_{0}) = j› ‹j∈J› ‹k∈K› ‹k⇩_{0}∈R› ‹f`(k⇩_{0}) = k› have "⟨j⇩_{0},k⇩_{0}⟩ ∈ (f-``J)×(f-``K)" using func1_1_L15 unfolding surj_def by auto ultimately have "M`⟨j⇩_{0},k⇩_{0}⟩ ∈ M``((f-``(J))×(f-``(K)))" using AMUV_are_ops func_imagedef by auto with ideals ‹?X ⊆ ?P› have "M`⟨j⇩_{0},k⇩_{0}⟩ ∈ ?P" using origin_ring.product_in_intersection(3) by blast with ‹?P⊆R› ‹t=f`(M`⟨j⇩_{0},k⇩_{0}⟩)› have "t∈(f``(?P))" using f_is_fun func1_1_L15D by simp } hence "V``(J × K) ⊆ f``(?P)" by blast with assms(1,2) ‹(f``(?P)) ◃R⇩_{t}› have "?Q⊆f``(?P)" using target_ring.generated_ideal_small target_ring.productIdeal_def by simp then have R: "f-``(?Q) ⊆ f-``(f``?P)" unfolding vimage_def by blast from ‹?X ⊆ ?P› ‹?P ◃R⇩_{o}› ‹?P⊆R› have P_ideal: "?P ∈ {N∈ℐ. f-``{𝟬⇩_{S}} ⊆ N}" by auto { fix t assume "t∈f-``(f``(?P))" then have "f`(t) ∈ f``(?P)" and "t∈R" using func1_1_L15 f_is_fun by simp_all with P_ideal obtain s where "f`(t) = f`(s)" "s∈?P" using func_imagedef f_is_fun by auto from P_ideal ‹s∈?P› have "s∈R" by blast from ‹t∈R› ‹s∈R› ‹f`(t) = f`(s)› have "f`(t\<rs>⇩_{R}s) = 𝟬⇩_{S}" using f_is_fun apply_funtype target_ring.Ring_ZF_1_L3(7) homomor_dest_subs by simp with ‹t∈R› ‹s∈R› ‹?X⊆?P› have "t\<rs>⇩_{R}s ∈ ?P" using origin_ring.Ring_ZF_1_L4(2) func1_1_L15 f_is_fun by auto with P_ideal ‹s∈?P› have "s\<ra>⇩_{R}(t\<rs>⇩_{R}s) ∈ ?P" using origin_ring.ideal_dest_sum by auto with ‹t∈R› ‹s∈R› have "t∈?P" using origin_ring.Ring_ZF_2_L1A(5) by auto } with R show "f-``(?Q) ⊆ ?P" by auto { fix t assume as: "t ∈ M``((f-``(J))×(f-``(K)))" have "(f-``(J))×(f-``(K)) ⊆ R×R" using func1_1_L15 f_is_fun by auto with as obtain t⇩_{j}t⇩_{k}where jk: "t=t⇩_{j}⋅⇩_{R}t⇩_{k}" "t⇩_{j}∈f-``(J)" "t⇩_{k}∈f-``(K)" using AMUV_are_ops(2) func_imagedef IsAssociative_def by auto from as have "t∈R" using AMUV_are_ops(2) func1_1_L6(2) by blast from jk(2,3) have "t⇩_{j}∈R" "f`(t⇩_{j})∈J" and "t⇩_{k}∈R" "f`(t⇩_{k})∈K" using func1_1_L15 f_is_fun by simp_all from jk(1) ‹t⇩_{j}∈R› ‹t⇩_{k}∈R› have ft: "f`(t) = ((f`(t⇩_{j}))⋅⇩_{S}(f`(t⇩_{k})))" using homomor_dest_mult by simp from ‹f`(t⇩_{j})∈J› ‹f`(t⇩_{k}) ∈K› have "⟨f`(t⇩_{j}),f`(t⇩_{k})⟩ ∈ J×K" by simp moreover from assms have "V:S×S→S" and "J×K ⊆ S×S" using AMUV_are_ops(4) target_ring.ideal_dest_subset by auto ultimately have "V`⟨f`(t⇩_{j}), f`(t⇩_{k})⟩ ∈V``(J×K)" using func_imagedef by force with assms ft ‹t∈R› have "t ∈ f-``(?Q)" using target_ring.product_in_intersection(3) func1_1_L15 f_is_fun by auto } hence "M``(f-``(J)×f-``(K))⊆f-``(?Q)" by auto moreover from assms(1,2) have id: "(f-``(?Q)) ◃R⇩_{o}" using preimage_ideal target_ring.product_in_intersection(2) by simp ultimately have "(f -`` J) ⋅⇩_{I}(f -`` K)⊆f-``(?Q)" using ideals origin_ring.generated_ideal_small origin_ring.productIdeal_def by auto with assms(1,2) have "?X ⊆ f-``(?Q)" using target_ring.product_in_intersection(2) target_ring.ideal_dest_zero by auto with idealJK id show "((f-``(J))⋅⇩_{I}(f-``(K)))+⇩_{I}(f-``{𝟬⇩_{S}}) ⊆ f-``(?Q)" using origin_ring.generated_ideal_small kernel_ideal origin_ring.sumIdeal_def by simp qed text‹If the homomorphism is surjective then the product ideal of ideals $J,K$ in the target ring is the image of the product ideal (in the source ring) of the inverse images of $J,K$. › corollary (in ring_homo) prime_ideal_quot_2: assumes "J◃R⇩_{t}" "K◃R⇩_{t}" "f∈surj(R,S)" shows "target_ring.productIdeal(J, K) = f``(origin_ring.productIdeal((f-``(J)), (f-``(K))))" proof - from assms have "f``(f-``(target_ring.productIdeal(J, K))) = f``(((f-``(J)) ⋅⇩_{I}(f-``(K))) +⇩_{I}(ker))" using prime_ideal_quot by simp with assms show ?thesis using target_ring.product_in_intersection(2) target_ring.ideal_dest_subset surj_image_vimage origin_ring.product_in_intersection(2) preimage_ideal kernel_empty_image(1) target_ring.zero_ideal by simp qed text‹If the homomorphism is surjective and an ideal in the source ring contains the kernel, then the image of that ideal is a prime ideal in the target ring.› lemma (in ring_homo) preimage_ideal_prime: assumes "J◃⇩_{p}R⇩_{o}" "ker ⊆ J" "f∈surj(R,S)" shows "(f``(J))◃⇩_{p}R⇩_{t}" proof - from assms(1) have "J ⊆ R" "J ≠ R" unfolding origin_ring.primeIdeal_def using origin_ring.ideal_dest_subset by auto from assms(1,3) have "(f``(J))◃R⇩_{t}" using image_ideal_surj unfolding origin_ring.primeIdeal_def by auto moreover { assume "f``(J) = S" from ‹J ⊆ R› ‹J ≠ R› obtain t where "t∈R-J" by auto with assms(3) have "f`(t)∈S" using apply_funtype f_is_fun by auto with assms(3) ‹J ⊆ R› ‹f``(J) = S› obtain j where j: "j∈J" "f`(t)= f`(j)" using func_imagedef f_is_fun by auto from ‹j∈J› ‹J ⊆ R› have "j∈R" by auto with assms(3) ‹f`(t)= f`(j)› ‹t∈R-J› have "t\<rs>⇩_{R}j∈f-``{𝟬⇩_{S}}" using apply_type target_ring.Ring_ZF_1_L3(7) f_is_fun homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15 by auto with assms(1,2) j(1) have "j\<ra>⇩_{R}(t\<rs>⇩_{R}j) ∈J" unfolding origin_ring.primeIdeal_def using origin_ring.ideal_dest_sum by auto with ‹j∈R› ‹t∈R-J› have False using origin_ring.Ring_ZF_2_L1A(5) by auto } hence "f``(J) ≠ S" by auto moreover { fix I K assume as: "I∈target_ring.ideals" "K∈target_ring.ideals" "target_ring.productIdeal(I, K) ⊆ f``(J)" let ?A = "(f-``(I)) ⋅⇩_{I}(f-``(K))" from as(1,2) have "?A ⊆ f-``(f``(?A))" using origin_ring.product_in_intersection(2) preimage_ideal(2) origin_ring.ideal_dest_subset func1_1_L9 f_is_fun by auto with assms(3) as have "?A ⊆ f-``(f``(J))" using prime_ideal_quot_2 vimage_mono by force moreover from assms(1) have "J ⊆ f-``(f``(J))" using func1_1_L9 f_is_fun origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def by auto moreover { fix t assume "t ∈ f-``(f``(J))" then have "f`(t)∈f``(J)" "t∈R" using func1_1_L15 f_is_fun by auto from assms(1) ‹f`(t)∈f``(J)› obtain s where "f`(t)=f`(s)" "s∈J" using func_imagedef f_is_fun origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def by auto from assms(1) ‹s∈J› have "s∈R" unfolding origin_ring.primeIdeal_def using origin_ring.ideal_dest_subset by auto with assms(2) ‹f`(t)=f`(s)› ‹t∈R› have "t\<rs>⇩_{R}s ∈ J" using target_ring.Ring_ZF_1_L3(7) apply_funtype f_is_fun homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15 by auto with assms(1) ‹s∈J› have "s\<ra>⇩_{R}(t\<rs>⇩_{R}s)∈J" using origin_ring.ideal_dest_sum unfolding origin_ring.primeIdeal_def by auto with ‹s∈R› ‹t∈R› have "t∈J" using origin_ring.Ring_ZF_2_L1A(5) by auto } hence "f-``(f``J) ⊆ J" by auto ultimately have "?A ⊆ J" by auto with assms(1) as(1,2) have "(f-``(I)) ⊆ J ∨ (f-``(K)) ⊆ J" using preimage_ideal origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def by auto hence "f``(f-``(I)) ⊆ f``J ∨ f``(f-``(K)) ⊆ f``(J)" by auto with assms(3) as(1,2) have "I ⊆ f``(J) ∨ K ⊆ f``(J)" using surj_image_vimage by auto } ultimately show ?thesis unfolding target_ring.primeIdeal_def by auto qed text‹The ideals of the quotient ring are in bijection with the ideals of the original ring that contain the ideal by which we made the quotient.› theorem (in ring_homo) ideal_quot_bijection: assumes "f∈surj(R,S)" defines "idealFun ≡ λJ∈target_ring.ideals. f-``(J)" shows "idealFun ∈ bij(target_ring.ideals,{K∈ℐ. ker ⊆ K})" proof - let ?ℐ⇩_{t}= "target_ring.ideals" have "idealFun : ?ℐ⇩_{t}→ {f-``(J). J∈?ℐ⇩_{t}}" unfolding idealFun_def using lam_funtype by simp moreover { fix t assume "t ∈ {f-``(J). J∈?ℐ⇩_{t}}" then obtain K where "K ∈ ?ℐ⇩_{t}" "f-``(K) = t" by auto then have "K◃R⇩_{t}" by simp then have "(f-``(K))◃R" "ker ⊆ f-``(K)" using preimage_ideal(2,3) by simp_all with ‹f-``(K) = t› have "ker ⊆ t" "t◃R" by simp_all with ‹f-``(K) = t› have "t∈{K∈ℐ. ker ⊆ K}" using func1_1_L3 f_is_fun by blast } hence "{f-``(J). J∈?ℐ⇩_{t}} ⊆ {K∈ℐ. ker ⊆ K}" by blast ultimately have I: "idealFun : ?ℐ⇩_{t}→ {K∈ℐ. ker ⊆ K}" using func1_1_L1B by auto { fix w x assume as: "w◃R⇩_{t}" "x◃R⇩_{t}" "w⊆S" "x⊆S" "idealFun`(w) = idealFun`(x)" then have "f``(f-``(w)) = f``(f-``(x))" unfolding idealFun_def by simp with assms(1) as have "w = x" using surj_image_vimage by simp } with I have "idealFun ∈ inj(?ℐ⇩_{t},{K∈ℐ. ker ⊆ K})" unfolding inj_def by auto moreover { fix y assume "y◃R" "y⊆R" "ker ⊆ y" from ‹y⊆R› have "y ⊆ f-``(f``y)" using func1_1_L9 f_is_fun by auto moreover { fix t assume "t∈f-``(f``(y))" then have "f`(t) ∈ f``(y)" "t∈R" using func1_1_L15 f_is_fun by auto from ‹f`(t) ∈ f``(y)› ‹y⊆R› obtain s where "s∈y" "f`(t) = f`(s)" using func_imagedef f_is_fun by auto from ‹s∈y› ‹y⊆R› have "s∈R" by auto with ‹t∈R› ‹f`(t) = f`(s)› ‹ker ⊆ y› have "t\<rs>⇩_{R}s ∈ y" using target_ring.Ring_ZF_1_L3(7) homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15 f_is_fun by auto with ‹s∈y› ‹y◃R› ‹s∈R› ‹t∈R› have "t∈y" using origin_ring.ideal_dest_sum origin_ring.Ring_ZF_2_L1A(5) by force } ultimately have "f-``(f``(y)) = y" by blast moreover have "f``(y) ⊆ S" using func1_1_L6(2) f_is_fun unfolding surj_def by auto moreover from assms(1) ‹y◃R› have "(f``(y))◃R⇩_{t}" using image_ideal_surj by auto ultimately have "∃x∈?ℐ⇩_{t}. idealFun`(x) = y" unfolding idealFun_def by auto } with I have "idealFun ∈ surj(?ℐ⇩_{t},{K∈ℐ. ker ⊆ K})" unfolding surj_def by auto ultimately show ?thesis unfolding bij_def by blast qed text‹Assume the homomorphism $f$ is surjective and consider the function that maps an ideal $J$ in the target ring to its inverse image $f^{-1}(J)$ (in the source ring). Then the value of the converse of that function on any ideal containing the kernel of $f$ is the image of that ideal under the homomorphism $f$. › theorem (in ring_homo) quot_converse: defines "F ≡ λJ∈target_ring.ideals. f-``(J)" assumes "J◃R" "ker⊆J" "f∈surj(R,S)" shows "converse(F)`(J) = f``(J)" proof- let ?g = "λJ∈{K∈ℐ. ker⊆K}. f``(J)" let ?ℐ⇩_{t}= "target_ring.ideals" let ?C⇩_{F}= "converse(F)" from assms(1,4) have "?C⇩_{F}∈ bij({K∈ℐ. ker⊆K}, ?ℐ⇩_{t})" using bij_converse_bij ideal_quot_bijection by auto then have I: "?C⇩_{F}:{K∈ℐ. ker⊆K} → ?ℐ⇩_{t}" unfolding bij_def inj_def by auto moreover from assms(2,3) have J: "J ∈ {K∈ℐ. ker⊆K}" using origin_ring.ideal_dest_subset by auto ultimately have ideal: "?C⇩_{F}`(J) ∈ ?ℐ⇩_{t}" using apply_funtype by blast with assms(1,4) ideal have "?g`(F`(?C⇩_{F}`(J))) = ?C⇩_{F}`(J)" using preimage_ideal origin_ring.ideal_dest_subset surj_image_vimage by auto moreover from assms(1) have "F: ?ℐ⇩_{t}→ {f-``(J). J∈?ℐ⇩_{t}}" using lam_funtype by simp with I J have "F`(?C⇩_{F}`(J)) = J" using right_inverse_lemma by simp ultimately have "?g`(J) = ?C⇩_{F}`(J)" by simp with J show ?thesis by simp qed text‹Since the map is surjective, this bijection restricts to prime ideals on both sides.› corollary (in ring_homo) prime_ideal_quot_3: assumes "K◃R⇩_{t}" "f ∈ surj(R,S)" shows "K◃⇩_{p}R⇩_{t}⟷ ((f-``(K))◃⇩_{p}R)" proof { assume "K◃⇩_{p}R⇩_{t}" with assms(2) show "(f-``(K))◃⇩_{p}R" using preimage_prime_ideal_surj target_ring.ideal_dest_subset unfolding target_ring.primeIdeal_def by auto } { assume "(f-``(K))◃⇩_{p}R" with assms(1,2) have "K◃R⇩_{t}" and "K≠S" using func1_1_L4 unfolding origin_ring.primeIdeal_def surj_def by auto moreover { fix J P assume jp: "J∈target_ring.ideals" "P∈target_ring.ideals" "target_ring.productIdeal(J, P) ⊆ K" from jp(3) have "f-``(target_ring.productIdeal(J, P)) ⊆ f-``(K)" by auto with assms(2) jp(1,2) have A: "((f-``(J)) ⋅⇩_{I}(f-``(P))) +⇩_{I}(ker) ⊆ f-``(K)" using prime_ideal_quot by auto from jp(1,2) have "(f-``(J))⋅⇩_{I}(f-``(P)) ∪ ker ⊆ ((f-``(J))⋅⇩_{I}(f-``(P))) +⇩_{I}(ker)" using preimage_ideal origin_ring.product_in_intersection(2) kernel_ideal origin_ring.comp_in_sum_ideals(3) by simp with A have "((f -`` J) ⋅⇩_{I}(f -`` P)) ⊆ f-``(K)" by auto with ‹(f-``(K))◃⇩_{p}R› jp(1,2) have "f-``(J) ⊆ f-``(K) ∨ f-``(P) ⊆ f-``(K)" using preimage_ideal origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def by auto then have "f``(f-``(J)) ⊆ f``(f-``(K)) ∨ f``(f-``(P)) ⊆ f``(f-``(K))" by blast with assms jp(1,2) have "J ⊆ K ∨ P ⊆ K" using surj_image_vimage target_ring.ideal_dest_subset by auto } ultimately show "K◃⇩_{p}R⇩_{t}" unfolding target_ring.primeIdeal_def by auto } qed text‹If the homomorphism is surjective then the function that maps ideals in the target ring to their inverse images (in the source ring) is a bijection between prime ideals in the target ring and the prime ideals containing the kernel in the source ring. › corollary (in ring_homo) bij_prime_ideals: defines "F ≡ λJ∈target_ring.ideals. f-``(J)" assumes "f ∈ surj(R,S)" shows "restrict(F,{J∈Pow(S). J◃⇩_{p}R⇩_{t}}) ∈ bij({J∈Pow(S). J◃⇩_{p}R⇩_{t}}, {J∈Pow(R). ker⊆J ∧ (J◃⇩_{p}R)})" proof - let ?ℐ⇩_{t}= "target_ring.ideals" from assms have I: "F:?ℐ⇩_{t}→ {K∈ℐ. ker ⊆ K}" using ideal_quot_bijection bij_is_fun by simp have II: "{J∈Pow(S). J◃⇩_{p}R⇩_{t}} ⊆ ?ℐ⇩_{t}" unfolding target_ring.primeIdeal_def by auto have III: "{J∈Pow(S). J◃⇩_{p}R⇩_{t}} ⊆ ?ℐ⇩_{t}" unfolding target_ring.primeIdeal_def by auto with assms have "restrict(F,{J∈Pow(S). J◃⇩_{p}R⇩_{t}}) ∈ bij({J∈Pow(S). J◃⇩_{p}R⇩_{t}}, F``{J∈Pow(S). J◃⇩_{p}R⇩_{t}})" using restrict_bij ideal_quot_bijection unfolding bij_def by auto moreover have "{t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)} = F``{J∈Pow(S). J◃⇩_{p}R⇩_{t}}" proof { fix t assume "t ∈ F``{J∈Pow(S). J◃⇩_{p}R⇩_{t}}" with I III obtain q where "q∈Pow(S)" "q◃⇩_{p}R⇩_{t}" "t=F`(q)" using func_imagedef by auto from ‹q∈Pow(S)› ‹q◃⇩_{p}R⇩_{t}› have "q∈?ℐ⇩_{t}" unfolding target_ring.primeIdeal_def by auto with I have "F`(q) ∈ {K∈ℐ. ker ⊆ K}" using apply_funtype by blast with assms ‹q◃⇩_{p}R⇩_{t}› ‹t=F`(q)› ‹q∈?ℐ⇩_{t}› ‹t=F`(q)› have "t◃R" "t◃⇩_{p}R" "ker⊆t" using prime_ideal_quot_3 by simp_all } then show "F``{J∈Pow(S). J◃⇩_{p}R⇩_{t}} ⊆ {t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)}" using origin_ring.ideal_dest_subset by blast { fix t assume "t∈{t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)}" then have "t∈Pow(R)" "ker⊆t" "t◃⇩_{p}R" by auto then have tSet: "t ∈ {t∈ℐ. ker ⊆ t}" unfolding origin_ring.primeIdeal_def by auto with assms have cont: "converse(F)`(t) ∈ ?ℐ⇩_{t}" using ideal_quot_bijection bij_converse_bij apply_funtype bij_is_fun by blast moreover from assms tSet have "F`(converse(F)`(t)) = t" using ideal_quot_bijection right_inverse_bij by blast ultimately have "f-``(converse(F)`(t)) = t" using assms(1) by simp with assms II tSet ‹t◃⇩_{p}R› cont have "t ∈ F``{J∈Pow(S). J◃⇩_{p}R⇩_{t}}" using prime_ideal_quot_3 target_ring.ideal_dest_subset bij_val_image_vimage ideal_quot_bijection unfolding target_ring.primeIdeal_def by auto } thus "{t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)} ⊆ F``{J∈Pow(S). J◃⇩_{p}R⇩_{t}}" by auto qed ultimately show ?thesis by auto qed end