(* 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.› definition ringHomomor ("_{is a ring homomorphism}{_,_,_}→{_,_,_}" 85) where "IsAring(R,A,M) ⟹ IsAring(S,U,V) ⟹ ringHomomor(f,R,A,M,S,U,V) ≡ Homomor(f,R,A,S,U) ∧ (∀x∈R. ∀y∈R. f`(M`⟨x,y⟩) = V`⟨f`x,f`y⟩) ∧ f`(TheNeutralElement(R,M)) = TheNeutralElement(S,V)" locale ring_homo = fixes R A M S U V f assumes origin:"IsAring(R,A,M)" and target:"IsAring(S,U,V)" and fun:"f:R→S" and homomorphism:"f{is a ring homomorphism}{R,A,M}→{S,U,V}" fixes ringa (infixl "\<ra>⇩_{R}" 90) defines ringa_def [simp]: "x\<ra>⇩_{R}b ≡ A`⟨x,b⟩" 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}b ≡ x\<ra>⇩_{R}(\<rm>⇩_{R}b)" fixes ringm (infixl "⋅⇩_{R}" 95) defines ringm_def [simp]: "x⋅⇩_{R}b ≡ M`⟨x,b⟩" 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" abbreviation (in ring_homo) ideal_origin ("_◃R⇩_{o}") where "I◃R⇩_{o}≡ ring0.Ideal(R,A,M,I)" abbreviation (in ring_homo) prime_ideal_target ("_◃⇩_{p}R⇩_{t}") where "I◃⇩_{p}R⇩_{t}≡ ring0.primeIdeal(S,U,V,I)" abbreviation (in ring_homo) prime_ideal_origin ("_◃⇩_{p}R⇩_{o}") where "I◃⇩_{p}R⇩_{o}≡ ring0.primeIdeal(R,A,M,I)" abbreviation (in ring_homo) ideal_target ("_◃R⇩_{t}") where "I◃R⇩_{t}≡ ring0.Ideal(S,U,V,I)" abbreviation (in ring_homo) kernel ("ker" 90) where "ker ≡ f-``{𝟬⇩_{S}}" sublocale ring_homo < origin_ring:ring0 using origin unfolding ring0_def by auto sublocale ring_homo < target_ring:ring0 S U V ringas ringminuss ringsubs ringms ringzeros ringones ringtwos ringsqs using target unfolding ring0_def by auto 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 ringHomomor_def by auto 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[of R A S U f x y] origin target homomorphism assms unfolding IsAring_def ringHomomor_def[OF origin target] by auto lemma (in ring_homo) homomor_dest_minus: assumes "x∈R" shows "f`(\<rm>⇩_{R}x) = \<rm>⇩_{S}(f`x)" using image_inv[of R A S U f x] origin target homomorphism assms fun unfolding IsAring_def ringHomomor_def[OF origin target] by auto 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[of x "\<rm>⇩_{R}y"] homomor_dest_minus[of y] using origin_ring.Ring_ZF_1_L3(1) by auto lemma (in ring_homo) homomor_dest_zero: shows "f`(𝟬⇩_{R}) = 𝟬⇩_{S}" proof- have "f`(𝟬⇩_{R}) = f`(𝟬⇩_{R}\<rs>⇩_{R}𝟬⇩_{R})" using origin_ring.Ring_ZF_1_L3(7) origin_ring.Ring_ZF_1_L2(1) by auto then have "f`(𝟬⇩_{R}) = f`(𝟬⇩_{R})\<rs>⇩_{S}(f`𝟬⇩_{R})" using homomor_dest_subs origin_ring.Ring_ZF_1_L2(1) by auto then show ?thesis using target_ring.Ring_ZF_1_L3(7) origin_ring.Ring_ZF_1_L2(1) apply_type[OF fun] by auto qed lemma (in ring_homo) preimage_ideal: assumes "J◃R⇩_{t}" shows "(f-``J)◃R⇩_{o}" "ker ⊆ f-``J" proof- have "IsAnormalSubgroup(R,A,f-``J)" using preimage_normal_subgroup[OF _ _ _ fun] target_ring.ideal_normal_add_subgroup origin assms target homomorphism unfolding IsAring_def ring0_def ringHomomor_def[OF origin target] by auto then have "IsAsubgroup(f-``J,A)" unfolding IsAnormalSubgroup_def by auto moreover { fix x y assume xy:"x∈f-``J" "y∈R" from xy(1) have "f`x ∈ J" "x∈R" using func1_1_L15 fun by auto moreover have "f`y∈S" using xy(2) apply_type fun by auto ultimately have "V`⟨f`x,f`y⟩∈J" "V`⟨f`y,f`x⟩∈J" using target_ring.ideal_dest_mult assms by auto then have "f`(M`⟨x,y⟩)∈J" "f`(M`⟨y,x⟩)∈J" using homomor_dest_mult xy(2) ‹x∈R› by auto moreover have "M`⟨x,y⟩∈R" "M`⟨y,x⟩∈R" using xy(2) ‹x∈R› origin_ring.Ring_ZF_1_L4(3) by auto ultimately have "M`⟨x,y⟩∈f-``J" "M`⟨y,x⟩∈f-``J" using func1_1_L15 fun by auto } ultimately show "(f-``J)◃R⇩_{o}" using origin_ring.Ideal_def by auto have "𝟬⇩_{S}∈J" using assms target_ring.ideal_dest_zero by auto then show "ker ⊆ f-``J" by auto qed text‹Even more, if the target ring of the homomorphism is commutative or the homomorphism is surjective; we show that if the ideal es 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(rule origin_ring.equivalent_prime_ideal_2) show "(f-``J)◃R⇩_{o}" using preimage_ideal assms unfolding target_ring.primeIdeal_def by auto { assume "R = f-`` J" then have "R = {x∈R. f`x ∈J}" using fun func1_1_L15 by auto moreover have "𝟭⇩_{R}∈R" using origin_ring.Ring_ZF_1_L2(2). ultimately have "𝟭⇩_{R}∈{x∈R. f`x ∈J}" by auto then have "f`(𝟭⇩_{R}) ∈J" by auto moreover have "f`𝟭⇩_{R}= 𝟭⇩_{S}" using homomorphism unfolding ringHomomor_def[OF origin_ring.ringAssum target_ring.ringAssum] by auto ultimately have "𝟭⇩_{S}∈ J" by auto then have False using target_ring.ideal_with_one assms unfolding target_ring.primeIdeal_def by auto } then show "f -`` J ≠ R" by auto show "∀x∈R. ∀y∈R. (∀z∈R. x ⋅⇩_{R}z ⋅⇩_{R}y ∈ f -`` J) ⟶ x ∈ f -`` J ∨ y ∈ f -`` J" proof(safe) fix x y assume as:"x∈R" "y∈R" "∀z∈R. x ⋅⇩_{R}z ⋅⇩_{R}y ∈ f -`` J" "y ∉ f -`` J" { fix s assume s:"s∈S" then have "(f`x)⋅⇩_{S}s⋅⇩_{S}(f`y) = s⋅⇩_{S}((f`x)⋅⇩_{S}(f`y))" using assms(2) unfolding IsCommutative_def using apply_type[OF fun as(1)] target_ring.Ring_ZF_1_L11(2) apply_type[OF fun as(2)] by auto then have "(f`x)⋅⇩_{S}s⋅⇩_{S}(f`y) = s⋅⇩_{S}(f`(x⋅⇩_{R}y))" using homomor_dest_mult[OF as(1,2)] by auto moreover from as(3) have "x⋅⇩_{R}y : f-``J" using origin_ring.Ring_ZF_1_L2(2) origin_ring.Ring_ZF_1_L3(5)[OF as(1)] by force then have "f`(x⋅⇩_{R}y) : J" using func1_1_L15 fun by auto with s have "s⋅⇩_{S}(f`(x⋅⇩_{R}y)) :J" using assms(1) unfolding target_ring.primeIdeal_def using target_ring.ideal_dest_mult(2) by auto ultimately have "(f`x)⋅⇩_{S}s⋅⇩_{S}(f`y):J" by auto } then have "∀z∈S. (f`x) ⋅⇩_{S}z ⋅⇩_{S}(f`y) ∈ J" by auto with target_ring.equivalent_prime_ideal[OF assms(1)] apply_type[OF fun] as(1,2) have "f`x:J∨f`y:J" by auto with as(4,2) have "f`x:J" using func1_1_L15 fun by auto then show "x:f-``J" using as(1) func1_1_L15 fun by auto qed qed lemma (in ring_homo) preimage_prime_ideal_surj: assumes "J◃⇩_{p}R⇩_{t}" "f:surj(R,S)" shows "(f-``J)◃⇩_{p}R⇩_{o}" proof(rule origin_ring.equivalent_prime_ideal_2) show "(f-``J)◃R⇩_{o}" using preimage_ideal assms unfolding target_ring.primeIdeal_def by auto { assume "R = f-`` J" then have "R = {x∈R. f`x ∈J}" using fun func1_1_L15 by auto moreover have "𝟭⇩_{R}∈R" using origin_ring.Ring_ZF_1_L2(2). ultimately have "𝟭⇩_{R}∈{x∈R. f`x ∈J}" by auto then have "f`(𝟭⇩_{R}) ∈J" by auto moreover have "f`𝟭⇩_{R}= 𝟭⇩_{S}" using homomorphism unfolding ringHomomor_def[OF origin_ring.ringAssum target_ring.ringAssum] by auto ultimately have "𝟭⇩_{S}∈ J" by auto then have False using target_ring.ideal_with_one assms unfolding target_ring.primeIdeal_def by auto } then show "f -`` J ≠ R" by auto show "∀x∈R. ∀y∈R. (∀z∈R. x ⋅⇩_{R}z ⋅⇩_{R}y ∈ f -`` J) ⟶ x ∈ f -`` J ∨ y ∈ f -`` J" proof(safe) fix x y assume as:"x∈R" "y∈R" "∀z∈R. x ⋅⇩_{R}z ⋅⇩_{R}y ∈ f -`` J" "y ∉ f -`` J" { fix s assume s:"s∈S" with assms(2) obtain t where t:"s=f`t" "t:R" unfolding surj_def by auto then have "(f`x)⋅⇩_{S}(f`t)⋅⇩_{S}(f`y) = f`(x⋅⇩_{R}t⋅⇩_{R}y)" using homomor_dest_mult as(1,2) t(2) origin_ring.Ring_ZF_1_L4(3) by auto moreover have "(x⋅⇩_{R}t⋅⇩_{R}y)∈f-``J" using as(3) t(2) by auto ultimately have "(f`x)⋅⇩_{S}(f`t)⋅⇩_{S}(f`y)∈J" using func1_1_L15 fun by auto with t(1) have "(f`x)⋅⇩_{S}s⋅⇩_{S}(f`y)∈J" by auto } then have "∀z∈S. (f`x) ⋅⇩_{S}z ⋅⇩_{S}(f`y) ∈ J" by auto with target_ring.equivalent_prime_ideal[OF assms(1)] apply_type[OF fun] as(1,2) have "f`x:J∨f`y:J" by auto with as(4,2) have "f`x:J" using func1_1_L15 fun by auto then show "x:f-``J" using as(1) func1_1_L15 fun by auto qed qed section‹Quotient ring with quotient map› 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)" abbreviation (in ring2) qideal ("_◃R⇩_{I}") where "J◃R⇩_{I}≡ ring0.Ideal(R⇩_{I},A⇩_{I},M⇩_{I},J)" abbreviation (in ring2) qprimeIdeal ("_◃⇩_{p}R⇩_{I}") where "J◃⇩_{p}R⇩_{I}≡ ring0.primeIdeal(R⇩_{I},A⇩_{I},M⇩_{I},J)" lemma (in ring_homo) image_kernel: assumes "x∈ker" shows "f`x = 𝟬⇩_{S}" using assms func1_1_L15 fun by auto corollary (in ring_homo) image_kernel_2: shows "f``(ker) = {𝟬⇩_{S}}" proof- have "𝟬⇩_{R}∈ker" using homomor_dest_zero origin_ring.Ring_ZF_1_L2(1) func1_1_L15 fun by auto moreover have "ker ⊆ R" using func1_1_L15[OF fun, of "{𝟬⇩_{S}}"] by auto then have "f `` (ker) = {f ` x . x ∈ ker}" using func_imagedef[OF fun, of ker] by auto ultimately show ?thesis using image_kernel by auto qed 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)" unfolding ring0_def quot_def using quotientBy_is_ring[OF idealAssum] apply simp unfolding ideal_radd_def ideal_rmin_def ideal_rsub_def ideal_rmult_def ideal_rzero_def ideal_rone_def ideal_rtwo_def ideal_rsqr_def apply auto using neutral_quotient[OF idealAssum] apply simp using one_quotient[OF idealAssum] apply simp using two_quotient[OF idealAssum] by simp text‹The quotient map is a homomorphism of rings› theorem (in ring2) quotient_fun_homomor: shows "f⇩_{I}{is a ring homomorphism}{R,A,M}→{R⇩_{I},A⇩_{I},M⇩_{I}}" unfolding ringHomomor_def[OF ringAssum quotient_ring.ringAssum] proof(safe) from add_group.quotient_map[OF ideal_normal_add_subgroup[OF idealAssum]] show "Homomor(f⇩_{I},R,A,R⇩_{I},A⇩_{I})" unfolding qfun_def quot_def qadd_def QuotientBy_def[OF idealAssum] by auto { fix x y assume as:"x∈R" "y∈R" have "f⇩_{I}` (x⋅y) = QuotientGroupRel(R,A,I)``{x⋅y}" unfolding qfun_def using as Ring_ZF_1_L4(3) lamE lam_funtype by auto then have "f⇩_{I}` (x⋅y) = ((QuotientGroupRel(R,A,I)``{x}){⋅I}(QuotientGroupRel(R,A,I)``{y}))" using EquivClass_1_L10[OF equiv_rel[OF idealAssum] quotientBy_mul_monoid(1)[OF idealAssum]] as by auto then have "f⇩_{I}` (x⋅y) = ((f⇩_{I}`x){⋅I}(f⇩_{I}`y))" unfolding qfun_def using as lamE lam_funtype by auto then show "f⇩_{I}` (M ` ⟨x, y⟩) =M⇩_{I}` ⟨f⇩_{I}` x, f⇩_{I}` y⟩" by auto } have "f⇩_{I}`𝟭 = QuotientGroupRel(R,A,I)``{𝟭}" unfolding qfun_def using lam_funtype lamE Ring_ZF_1_L2(2) by auto then have "f⇩_{I}`𝟭 = TheNeutralElement(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R,A,I), M))" using Group_ZF_2_2_L1[OF _ equiv_rel[OF idealAssum] quotientBy_mul_monoid(1)[OF idealAssum]] ringAssum unfolding IsAring_def QuotientBy_def[OF idealAssum] by auto then show "f⇩_{I}` TheNeutralElement(R, M) = TheNeutralElement(R⇩_{I}, M⇩_{I})" unfolding quot_def by auto qed text‹The quotient map is surjective› lemma (in ring2) quot_fun: shows "f⇩_{I}∈surj(R,R⇩_{I})" unfolding qfun_def using lam_funtype unfolding quot_def QuotientBy_def[OF idealAssum] quotient_def qrel_def surj_def by auto 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)" unfolding ring_homo_def using ringAssum quotient_ring.ringAssum quotient_fun_homomor quot_fun unfolding surj_def by auto lemma (in ring2) quotient_kernel: shows "quot_homomorphism.kernel = I" proof { fix t assume t:"t∈quot_homomorphism.kernel" then have t:"f⇩_{I}`t = 𝟬⇩I" "t∈R" using quot_homomorphism.image_kernel func1_1_L15[OF surj_is_fun[OF quot_fun]] by auto then have "r⇩_{I}``{t} = 𝟬⇩I" using beta by auto then have "t∈I" using add_group.Group_ZF_2_4_L5E[OF ideal_normal_add_subgroup[OF idealAssum] t(2)] neutral_quotient[OF idealAssum] unfolding ideal_rzero_def QuotientBy_def[OF idealAssum] by auto } then show "quot_homomorphism.kernel ⊆ I" by auto { fix t assume t:"t∈I" then have tt:"t∈R" using ideal_dest_subset idealAssum by auto then have "r⇩_{I}``{t} = 𝟬⇩I" using add_group.Group_ZF_2_4_L5E[OF ideal_normal_add_subgroup[OF idealAssum] tt] t neutral_quotient[OF idealAssum] unfolding ideal_rzero_def QuotientBy_def[OF idealAssum] by auto then have "f⇩_{I}`t = 𝟬⇩I" using beta tt by auto with tt have "t∈f⇩_{I}-``{𝟬⇩I}" using func1_1_L15 surj_is_fun quot_fun by auto } then show "I ⊆ quot_homomorphism.kernel" by auto qed 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)" unfolding ring0_def quot_def using quotientBy_is_ring[OF idealAssum] apply simp unfolding ideal_radd_def ideal_rmin_def ideal_rsub_def ideal_rmult_def ideal_rzero_def ideal_rone_def ideal_rtwo_def ideal_rsqr_def apply auto using neutral_quotient[OF idealAssum] apply simp using one_quotient[OF idealAssum] apply simp using two_quotient[OF idealAssum] by simp 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)" unfolding ring_homo_def using ringAssum quotient_ring.ringAssum quotient_fun_homomor quot_fun unfolding surj_def by auto 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- have sub:"J+⇩_{I}I ⊆ R" using assms origin_ring.sum_ideals_is_ideal[THEN origin_ring.ideal_dest_subset] origin_ring.ideal_dest_subset by auto { fix t assume "t∈f``(J+⇩_{I}I)" then obtain q where q:"q∈J+⇩_{I}I" "t=f`q" using func_imagedef fun sub(1) by auto from q(1) 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 then obtain qj qi where qji:"qj∈J" "qi∈I" "q=qj\<ra>⇩_{R}qi" using func_imagedef[of A "R×R" R] origin_ring.add_group.groupAssum unfolding IsAgroup_def IsAmonoid_def IsAssociative_def by auto from qji(3) have "f`q = f`(qj\<ra>⇩_{R}qi)" by auto with qji(1,2) assms(1,3) have "(f`q) = ((f`qj)\<ra>⇩_{S}(f`qi))" using homomor_dest_add[of qj qi] origin_ring.ideal_dest_subset by auto moreover from qji(2) assms(2) have "qi∈ker" by auto ultimately have "f ` q = ((f ` qj)\<ra>⇩_{S}𝟬⇩_{S})" using image_kernel by auto then have "f ` qj ∈S ⟹ f ` q = (f ` qj)" using target_ring.Ring_ZF_1_L3(3) by auto moreover have "qj∈R" using assms qji(1) origin_ring.ideal_dest_subset by auto then have "f ` qj ∈S" using apply_type[OF fun] by auto ultimately have "f ` q = (f ` qj)" by auto with q(2) have "t = f` qj" by auto then have "t∈ f``J" using qji(1) func_imagedef fun assms origin_ring.ideal_dest_subset by auto } then have "f `` (J +⇩_{I}I) ⊆ f `` J" by auto moreover { fix t assume t:"t∈f``J" then obtain q where q:"q∈J" "t=f`q" using func_imagedef fun assms(1) origin_ring.ideal_dest_subset by auto from q(1) have "q∈J∪I" by auto moreover have "J∪I ⊆ R" using assms(1,3) origin_ring.ideal_dest_subset by auto ultimately have "q∈⟨J∪I⟩⇩_{I}" using origin_ring.generated_ideal_contains_set by auto then have "q∈J+⇩_{I}I" unfolding origin_ring.sumIdeal_def[OF assms(1,3)]. with q(2) have "t∈f``(J+⇩_{I}I)" using func_imagedef fun sub by auto } then have "f``J ⊆ f `` (J +⇩_{I}I)" by auto ultimately show "f `` (J +⇩_{I}I) = f``J" "f `` (I +⇩_{I}J) = f``J" using origin_ring.sum_ideals_commute assms(1,3) by auto qed subsection‹Quotient ideals› 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 quot_homomorphism.preimage_ideal[OF assms] show "(f⇩_{I}-``J) ◃R" by auto { fix x assume x:"x∈I" with quot_fun have "f⇩_{I}`x = r⇩_{I}``{x}" using lamI[of x R] ideal_dest_subset[OF idealAssum] apply_equality[of x "r⇩_{I}``{x}" "f⇩_{I}"] unfolding qfun_def by auto then have "f⇩_{I}`x = 𝟬⇩I" using add_group.Group_ZF_2_4_L5E[OF ideal_normal_add_subgroup[OF idealAssum], of x "r⇩_{I}" "𝟬⇩I"] x ideal_dest_subset[OF idealAssum] unfolding qrel_def ideal_rzero_def using Group_ZF_2_4_L5B[OF _ ideal_normal_add_subgroup[OF idealAssum]] using ringAssum unfolding IsAring_def by auto then have "f⇩_{I}`x ∈ J" using quotient_ring.ideal_dest_zero assms by auto then have "x∈f⇩_{I}-``J" using x ideal_dest_subset[OF idealAssum] quot_fun func1_1_L15 by auto } then show "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}" unfolding target_ring.Ideal_def proof show "IsAsubgroup(f``J,U)" proof (rule image_subgroup) show "IsAgroup(R,A)" using origin_ring.ringAssum unfolding IsAring_def by auto show "f : R → S" using fun . show "IsAsubgroup(J,A)" using assms unfolding origin_ring.Ideal_def by auto show "Homomor(f,R,A,S,U)" using homomorphism unfolding ringHomomor_def[OF origin target] by auto show "IsAgroup(S,U)" using target_ring.ringAssum unfolding IsAring_def by auto qed { fix x y assume xy:"x∈f``J" "y∈S" from xy(1) obtain j where x:"x=f`j" "j∈J" using func_imagedef fun origin_ring.ideal_dest_subset[OF assms(1)] by auto from xy(2) have "y∈f``R" using assms(2) surj_range_image_domain by auto then obtain s where y:"y=f`s" "s∈R" using func_imagedef origin_ring.ideal_dest_subset[OF assms(1)] fun by auto from x(1) y(1) have "V`⟨x,y⟩ = V`⟨f`j,f`s⟩" "V`⟨y,x⟩ = V`⟨f`s,f`j⟩" by auto then have "V`⟨x,y⟩ = f`(M`⟨j,s⟩)" "V`⟨y,x⟩ = f`(M`⟨s,j⟩)" using homomor_dest_mult[of s j] homomor_dest_mult[of j s] x(2) y(2) origin_ring.ideal_dest_subset[OF assms(1)] by auto moreover have "j⋅⇩_{R}s∈J" "s⋅⇩_{R}j∈J" using origin_ring.ideal_dest_mult[OF assms(1)] x(2) y(2) by auto ultimately have "(x⋅⇩_{S}y)∈f``J" "(y⋅⇩_{S}x)∈f``J" using func_imagedef fun origin_ring.ideal_dest_subset[OF assms(1)] by auto } then show "∀x∈f `` J. ∀y∈S. (y⋅⇩_{S}x) ∈ f `` J ∧ (x⋅⇩_{S}y) ∈ f `` J" by auto qed 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}})" have qRI:"target_ring.productIdeal(J, K)◃R⇩_{t}" using target_ring.product_in_intersection(2) assms by auto 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 have idealSum:"?P ◃R" using origin_ring.sum_ideals_is_sum_elements[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]] origin_ring.sum_elements_is_ideal[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]] by auto then have ideal:"(f``?P) ◃R⇩_{t}" using image_ideal_surj assms(3) by auto { fix t assume "t∈V ``(J×K)" moreover have "J×K ⊆ S×S" using assms target_ring.ideal_dest_subset by auto moreover have "V:S×S → S" using target_ring.ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto ultimately obtain j k where jk:"j∈J" "k∈K" "t=V`⟨j,k⟩" using func_imagedef by auto from jk(1) have "j∈S" using assms(1) target_ring.ideal_dest_subset by auto then obtain jj where jj:"jj∈R" "f`jj = j" using assms(3) unfolding surj_def by auto from jk(2) have "k∈S" using assms(2) target_ring.ideal_dest_subset by auto then obtain kk where kk:"kk∈R" "f`kk = k" using assms(3) unfolding surj_def by auto from jk(3) jj(2) kk(2) have "t=V`⟨f`jj,f`kk⟩" by auto then have t:"t=f`(M`⟨jj,kk⟩)" using homomor_dest_mult[OF jj(1) kk(1)] by auto have "f-``J ⊆ R" using assms(3) using func1_1_L6A[OF surj_is_fun] by auto moreover have "f-``K ⊆ R" using assms(3) using func1_1_L6A[OF surj_is_fun] by auto ultimately have sub:"(f-``J)×(f-``K) ⊆ R×R" by auto moreover have "M:R×R → R" using origin_ring.ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto moreover { from jj have "jj∈f-``J" using func1_1_L15 assms(3) jk(1) unfolding surj_def by auto moreover from kk have "kk∈f-``K" using func1_1_L15 assms(3) jk(2) unfolding surj_def by auto ultimately have "⟨jj,kk⟩∈(f-``J)×(f-``K)" by auto } ultimately have "M`⟨jj,kk⟩ ∈ M``((f-``J)×(f-``K))" using func_imagedef by auto then have "M`⟨jj,kk⟩ ∈ (f-``J) ⋅⇩_{I}(f-``K)" using preimage_ideal assms origin_ring.product_in_intersection(3) by blast then have "M`⟨jj,kk⟩ ∈ ((f-``J) ⋅⇩_{I}(f-``K))∪(f-``{𝟬⇩_{S}})" by auto moreover have "((f-``J) ⋅⇩_{I}(f -`` K))∪(f-``{𝟬⇩_{S}})⊆R" using func1_1_L6A[OF surj_is_fun[OF assms(3)]] origin_ring.ideal_dest_subset[OF idealJK] by auto ultimately have "M`⟨jj,kk⟩ ∈ ?P" unfolding origin_ring.sumIdeal_def[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]] using origin_ring.generated_ideal_contains_set[of "((f-`` J) ⋅⇩_{I}(f-`` K)) ∪ (f-``{𝟬⇩_{S}})"] by blast then have "f`(M`⟨jj,kk⟩) ∈ f``?P" using func1_1_L15D[OF surj_is_fun[OF assms(3)] _ idealSum[THEN origin_ring.ideal_dest_subset]] by auto moreover note t ultimately have "t∈(f``?P)" by auto } then have "V `` (J × K) ⊆ f``?P" by blast then have "target_ring.generatedIdeal(V `` (J × K)) ⊆ f``?P" using ideal target_ring.generated_ideal_small by auto then have "target_ring.productIdeal(J, K) ⊆ f``(?P)" unfolding target_ring.productIdeal_def[OF assms(1,2)]. then have R:"f-``target_ring.productIdeal(J, K) ⊆ f-``(f``?P)" unfolding vimage_def by blast have "((f-``J) ⋅⇩_{I}(f-``K)) ∪ (f -`` {𝟬⇩_{S}}) ⊆ R" using idealJK origin_ring.ideal_dest_subset func1_1_L6A[OF surj_is_fun] assms(3) by blast then have p:"(f -`` {𝟬⇩_{S}}) ⊆ ?P" unfolding origin_ring.sumIdeal_def[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]] using origin_ring.generated_ideal_contains_set by blast moreover from idealSum origin_ring.ideal_dest_subset have "?P ⊆R" by auto moreover note idealSum ultimately have P_ideal:"?P ∈ {N∈ℐ. f-``{𝟬⇩_{S}} ⊆ N}" by auto have P:"f``?P ⊆ S" using ideal P_ideal assms(3) target_ring.ideal_dest_subset by auto { fix t assume "t∈f-``(f``?P)" then have t:"f`t∈f``?P" "t∈R" using func1_1_L15 surj_is_fun[OF assms(3)] by auto then obtain s where s:"f`t = f`s" "s∈?P" using func_imagedef[OF surj_is_fun[OF assms(3)]] P_ideal by auto from s(2) have ss:"s∈R" using P_ideal by auto from s(1) have "(f`t) \<rs>⇩_{S}(f`s) = 𝟬⇩_{S}" using target_ring.Ring_ZF_1_L3(7)[OF apply_type[OF surj_is_fun[OF assms(3)] t(2)]] by auto then have "f`(t\<rs>⇩_{R}s) = 𝟬⇩_{S}" using homomor_dest_subs t(2) ss by auto moreover from t(2) ss have "t\<rs>⇩_{R}s ∈R" using origin_ring.Ring_ZF_1_L4(2) by auto ultimately have "t\<rs>⇩_{R}s ∈ f-``{𝟬⇩_{S}}" using func1_1_L15 surj_is_fun[OF assms(3)] by auto then have "t\<rs>⇩_{R}s ∈ ?P" using p by auto then have "s\<ra>⇩_{R}(t\<rs>⇩_{R}s) ∈ ?P" using origin_ring.ideal_dest_sum P_ideal s(2) by auto then have "t∈?P" using origin_ring.Ring_ZF_2_L1A(5) ss t(2) by auto } then have "f-``(f``?P) ⊆ ?P" by auto with R show "f-``target_ring.productIdeal(J, K) ⊆ ?P" by auto { fix t assume as:"t∈M``((f-``J)×(f-``K))" moreover have "(f-``J)×(f-``K) ⊆ R×R" using func1_1_L15[OF surj_is_fun[OF assms(3)]] by auto ultimately obtain tj tk where jk:"t=tj⋅⇩_{R}tk" "tj∈f-``J" "tk∈f-``K" using func_imagedef[of M "R×R" R] origin_ring.ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto from as have tR:"t∈R" using func1_1_L6(2)[of M "R×R" R] origin_ring.ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto from jk(2) have j:"tj∈R" "f`tj ∈J" using func1_1_L15 surj_is_fun[OF assms(3)] by auto from jk(3) have k:"tk∈R" "f`tk ∈K" using func1_1_L15 surj_is_fun[OF assms(3)] by auto from jk(1) have "f`t = f`(tj⋅⇩_{R}tk)" by auto then have ft:"f`t = ((f`tj)⋅⇩_{S}(f`tk))" using homomor_dest_mult using j(1) k(1) by auto from j(2) k(2) have "⟨f`tj,f`tk⟩∈J×K" by auto moreover have "V:S×S→S" using target_ring.ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def by auto moreover have "J×K ⊆ S×S" using assms using target_ring.ideal_dest_subset by auto ultimately have "V`⟨f ` tj, f ` tk⟩ ∈V``(J×K)" using func_imagedef[of V "S×S" S "J×K"] by force with ft have "f`t∈V``(J×K)" by auto then have "f`t∈target_ring.productIdeal(J, K)" using target_ring.product_in_intersection(3) assms by blast then have "t∈f-``target_ring.productIdeal(J, K)" using func1_1_L15 surj_is_fun[OF assms(3)] tR by auto } then have "M `` (f -`` J × f -`` K) ⊆ f -`` target_ring.productIdeal(J, K)" by auto moreover have id:"(f -``target_ring.productIdeal(J, K)) ◃R⇩_{o}" apply (rule preimage_ideal) apply (rule target_ring.product_in_intersection(2)) using assms(1,2) . ultimately have "(f -`` J) ⋅⇩_{I}(f -`` K) ⊆ f -``target_ring.productIdeal(J, K)" using origin_ring.generated_ideal_small origin_ring.productIdeal_def[OF ideals] by auto moreover have "𝟬⇩_{S}∈ target_ring.productIdeal(J, K)" using target_ring.product_in_intersection(2) assms(1,2) target_ring.ideal_dest_zero by auto then have "(f -`` {𝟬⇩_{S}}) ⊆ f -``target_ring.productIdeal(J, K)" by auto ultimately have "((f -`` J) ⋅⇩_{I}(f -`` K))∪(f -`` {𝟬⇩_{S}}) ⊆ f -``target_ring.productIdeal(J, K)" by auto then show "((f -`` J) ⋅⇩_{I}(f -`` K))+⇩_{I}(f -`` {𝟬⇩_{S}}) ⊆ f -``target_ring.productIdeal(J, K)" using origin_ring.generated_ideal_small id origin_ring.sumIdeal_def[OF idealJK preimage_ideal(1)[OF target_ring.zero_ideal]] by auto qed 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- have "f-`` target_ring.productIdeal(J, K) = ((f-`` J) ⋅⇩_{I}(f-`` K)) +⇩_{I}(ker)" using prime_ideal_quot assms beta by auto then have "f``(f-`` target_ring.productIdeal(J, K)) = f``(((f -`` J) ⋅⇩_{I}(f -`` K)) +⇩_{I}(ker))" by auto moreover have "target_ring.productIdeal(J, K)◃R⇩_{t}" using target_ring.product_in_intersection(2) assms(1,2) by auto then have "target_ring.productIdeal(J, K) ⊆ S" using target_ring.ideal_dest_subset by auto ultimately have A:"target_ring.productIdeal(J, K) = f``(((f-`` J) ⋅⇩_{I}(f-`` K)) +⇩_{I}(f-``{𝟬⇩_{S}}))" using surj_image_vimage assms(3) by auto have idealJK:"((f-``J) ⋅⇩_{I}(f-``K)) ◃R" using origin_ring.product_in_intersection(2) preimage_ideal assms(1,2) by auto with A show "target_ring.productIdeal(J, K) = f``((f-`` J) ⋅⇩_{I}(f-`` K))" using kernel_empty_image(1) preimage_ideal[OF target_ring.zero_ideal] by auto qed 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,3) have "(f``J)◃R⇩_{t}" using image_ideal_surj unfolding origin_ring.primeIdeal_def by auto moreover from assms(1) have JT:"J ⊆ R" "J ≠ R" unfolding origin_ring.primeIdeal_def using origin_ring.ideal_dest_subset by auto { assume full:"f``J = S" from JT obtain t where t:"t∈R-J" by auto with assms(3) have "f`t∈S" using apply_type[OF surj_is_fun] by auto with full have "f`t∈f``J" by auto with assms(3) JT(1) obtain j where j:"j∈J" "f`t= f`j" using func_imagedef[OF surj_is_fun] by auto from j(1) have jt:"j∈R" using JT(1) by auto then have fj:"f`j∈S" using apply_type assms(3) unfolding surj_def by auto from j(2) have "(f`t)\<rs>⇩_{S}(f`j) = 𝟬⇩_{S}" using target_ring.Ring_ZF_1_L3(7) fj by auto then have "f`(t\<rs>⇩_{R}j) =𝟬⇩_{S}" using homomor_dest_subs t jt by auto moreover have "t\<rs>⇩_{R}j ∈R" using origin_ring.Ring_ZF_1_L4(2) t jt by auto ultimately have "t\<rs>⇩_{R}j∈f-``{𝟬⇩_{S}}" using func1_1_L15[OF surj_is_fun] assms(3) by auto with assms(2) have tjJ:"t\<rs>⇩_{R}j∈J" by auto with j(1) have "j\<ra>⇩_{R}(t\<rs>⇩_{R}j) ∈J" using assms(1) unfolding origin_ring.primeIdeal_def using origin_ring.ideal_dest_sum by auto then have False using origin_ring.Ring_ZF_2_L1A(5) using jt t by auto } then have "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" then have "f `` ((f -`` I) ⋅⇩_{I}(f -`` K)) ⊆ f``J" using prime_ideal_quot_2 assms(3) by auto then have "f-``(f `` ((f -`` I) ⋅⇩_{I}(f -`` K))) ⊆ f-``(f``J)" by blast moreover have "((f -`` I) ⋅⇩_{I}(f -`` K)) ◃R" using origin_ring.product_in_intersection(2)[OF preimage_ideal(1) preimage_ideal(1)] as(1,2) by auto then have "((f -`` I) ⋅⇩_{I}(f -`` K)) ⊆ R" using origin_ring.ideal_dest_subset by auto ultimately have "(f -`` I) ⋅⇩_{I}(f -`` K) ⊆ f-``(f``J)" using func1_1_L9[OF fun, of "(f -`` I) ⋅⇩_{I}(f -`` K)"] by auto moreover have "J ⊆ f-``(f``J)" using func1_1_L9 fun assms(1) origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def by auto moreover { fix t assume "t∈f-``(f``J)" then have t:"f`t∈f``J" "t∈R" using func1_1_L15 fun by auto from t(1) obtain s where s:"f`t = f`s" "s∈J" using func_imagedef fun assms(1) origin_ring.ideal_dest_subset unfolding origin_ring.primeIdeal_def by auto from s(2) assms(1) have ss:"s∈R" unfolding origin_ring.primeIdeal_def using origin_ring.ideal_dest_subset by auto from s(1) have "f`t \<rs>⇩_{S}(f`s) = 𝟬⇩_{S}" using target_ring.Ring_ZF_1_L3(7)[ OF apply_type[OF fun t(2)]] by auto then have "f`(t\<rs>⇩_{R}s) = 𝟬⇩_{S}" using homomor_dest_subs t(2) ss by auto moreover have "t\<rs>⇩_{R}s ∈R" using ss t(2) origin_ring.Ring_ZF_1_L4(2) by auto ultimately have "t\<rs>⇩_{R}s ∈ f-``{𝟬⇩_{S}}" using func1_1_L15 fun by auto with assms(2) have "t\<rs>⇩_{R}s ∈ J" by auto with s(2) have "s\<ra>⇩_{R}(t\<rs>⇩_{R}s)∈J" using assms(1) origin_ring.ideal_dest_sum unfolding origin_ring.primeIdeal_def by auto then have "t: J" using origin_ring.Ring_ZF_2_L1A(5) ss t(2) by auto } then have "f-``(f``J) ⊆ J" by auto ultimately have "(f -`` I) ⋅⇩_{I}(f -`` K) ⊆ J" by auto moreover have "(f -`` I) ∈ℐ" "(f -`` K) ∈ℐ" using as(1,2) preimage_ideal origin_ring.ideal_dest_subset by auto ultimately have "(f -`` I) ⊆ J ∨ (f -`` K) ⊆ J" using assms(1) unfolding origin_ring.primeIdeal_def by auto then have "f``(f -`` I) ⊆ f``J ∨ f``(f -`` K) ⊆ f``J" by auto with assms(3) have "I ⊆ f``J ∨ K ⊆ f``J" using surj_image_vimage as(1,2) 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})" unfolding bij_def inj_def surj_def proof(safe) have "idealFun ∈ target_ring.ideals → {f-``J. J∈target_ring.ideals}" unfolding idealFun_def using lam_funtype by auto moreover { fix t assume "t∈{f-``J. J∈target_ring.ideals}" then obtain K where "K∈target_ring.ideals" "f-``K = t" by auto then have "ker ⊆ t" "t◃R" "t ⊆ R" using preimage_ideal[of K] using func1_1_L3[OF surj_is_fun[OF assms(1)], of K] by auto then have "t∈{K∈ℐ. ker ⊆ K}" by auto } then have "{f-``J. J∈target_ring.ideals} ⊆ {K∈ℐ. ker ⊆ K}" by blast ultimately show "idealFun ∈ target_ring.ideals → {K∈ℐ. ker ⊆ K}" using func1_1_L1B by auto then show "idealFun ∈ target_ring.ideals → {K∈ℐ. ker ⊆ K}". { fix w x assume as:"w◃R⇩_{t}" "x◃R⇩_{t}" "w⊆S" "x⊆S" "idealFun ` w = idealFun ` x" then have "f-``w = f-``x" unfolding idealFun_def using beta by auto then have "f``(f-``w) = f``(f-``x)" by auto then show "w = x" using surj_image_vimage assms(1) as by auto } { fix y assume y:"y◃R" "y⊆R" "ker ⊆ y" from y(2) have "y ⊆ f-``(f``y)" using func1_1_L9[OF surj_is_fun] assms(1) by auto moreover { fix t assume "t∈f-``(f``y)" then have t:"f`t∈f``y" "t∈R" using func1_1_L15[OF surj_is_fun] assms(1) by auto from t(1) y(2) obtain s where s:"s∈y" "f`t = f`s" using func_imagedef[of f R S y, OF surj_is_fun] assms(1) by auto from s(1) have "s∈R" using y(2) by auto with t(2) have E:"f`t : S" "f`s: S" using apply_type[of f R "λu. S", OF surj_is_fun] assms(1) by auto from E(1) s(2) have "(f`t)\<rs>⇩_{S}(f`s) = 𝟬⇩_{S}" using target_ring.Ring_ZF_1_L3(7) by auto then have "f`(t\<rs>⇩_{R}s) = 𝟬⇩_{S}" using homomor_dest_subs t(2) `s:R` by auto moreover from ‹s∈R› have "t\<rs>⇩_{R}s ∈R" using origin_ring.Ring_ZF_1_L4(2) t(2) by auto ultimately have "t\<rs>⇩_{R}s ∈ f-``{𝟬⇩_{S}}" using func1_1_L15[OF surj_is_fun] assms(1) by auto with y(3) have "t\<rs>⇩_{R}s ∈ y" by auto with s(1) have "s\<ra>⇩_{R}(t\<rs>⇩_{R}s) ∈ y" using origin_ring.ideal_dest_sum y(1) by auto then have "t∈y" using origin_ring.Ring_ZF_2_L1A(5) using `s∈R` t(2) by auto } ultimately have "f-``(f``y) = y" by blast moreover have "f``y ⊆ S" using func1_1_L6(2)[of f R S] assms(1) unfolding surj_def by auto moreover have "(f``y)◃R⇩_{t}" using image_ideal_surj assms(1) y(1) by auto ultimately show "∃x∈target_ring.ideals. idealFun ` x = y" unfolding idealFun_def by auto } qed theorem (in ring_homo) quot_converse: defines "idealFun ≡ λJ∈target_ring.ideals. f-``J" assumes "J◃R" "ker⊆J" "f:surj(R,S)" shows "converse(idealFun)`J = f``J" proof- let ?g="λJ∈{K∈ℐ. ker⊆K}. f``J" have "?g∈{K∈ℐ. ker⊆K} → {f``J. J∈{K∈ℐ. ker⊆K}}" using lam_funtype by auto moreover have "{f``J. J∈{K∈ℐ. ker⊆K}} ⊆ target_ring.ideals" using image_ideal_surj target_ring.ideal_dest_subset assms(4) by auto ultimately have "?g∈{K∈ℐ. ker⊆K} → target_ring.ideals" using func1_1_L1B by auto have "converse(idealFun)∈bij({K∈ℐ. ker⊆K}, target_ring.ideals)" using bij_converse_bij ideal_quot_bijection assms(4) unfolding idealFun_def by auto then have confun:"converse(idealFun):{K∈ℐ. ker⊆K} → target_ring.ideals" unfolding bij_def inj_def by auto moreover have J:"J∈{K∈ℐ. ker⊆K}" using assms(2,3) origin_ring.ideal_dest_subset by auto ultimately have ideal:"converse(idealFun)`J ∈ target_ring.ideals" using apply_type[of "converse(idealFun)" "{K∈ℐ. ker⊆K}" "λq. target_ring.ideals" J] by auto then have "?g`(idealFun`(converse(idealFun)`J)) = ?g`(f-``(converse(idealFun)`J))" using beta unfolding idealFun_def by auto moreover from preimage_ideal ideal have "(f-``(converse(idealFun)`J))◃R" "ker ⊆ (f-``(converse(idealFun)`J))" by auto then have "?g`(f-``(converse(idealFun)`J)) = f``(f-``(converse(idealFun)`J))" using beta origin_ring.ideal_dest_subset by auto ultimately have "?g`(idealFun`(converse(idealFun)`J)) = f``(f-``(converse(idealFun)`J))" by auto then have "?g`(idealFun`(converse(idealFun)`J)) = converse(idealFun)`J" using surj_image_vimage assms(4) ideal by auto then have "?g`J = converse(idealFun)`J" using right_inverse_lemma[of idealFun target_ring.ideals "{K ∈ ℐ . ker ⊆ K}" "{K ∈ ℐ . ker ⊆ K}" J ] J confun bij_is_fun[OF ideal_quot_bijection] assms(4) unfolding idealFun_def by auto then show ?thesis using beta J by auto 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⇩_{o})" proof { assume as:"K◃⇩_{p}R⇩_{t}" then have "(f-``K)◃⇩_{p}R⇩_{o}" using preimage_prime_ideal_surj assms(2) by auto then show "(f-``K)◃⇩_{p}R⇩_{o}" using beta[of K target_ring.ideals] using target_ring.ideal_dest_subset[of K] as unfolding target_ring.primeIdeal_def by auto } moreover { assume as:"(f-``K)◃⇩_{p}R⇩_{o}" from assms(1) have "K◃R⇩_{t}". moreover { assume "K=S" then have "f-``K = f-``S" by auto then have "f-``K = R" using func1_1_L4 assms(2) unfolding surj_def by auto with as have False unfolding origin_ring.primeIdeal_def by auto } then have "K≠S" by auto moreover { fix J P assume jp:"J∈target_ring.ideals" "P∈target_ring.ideals" "target_ring.productIdeal(J, P) ⊆ K" have sub:"((f -`` J) ⋅⇩_{I}(f -`` P)) ∪ ker ⊆ R" using origin_ring.ideal_dest_subset origin_ring.product_in_intersection(2) preimage_ideal target_ring.zero_ideal jp by auto from jp(3) have "f -``target_ring.productIdeal(J, P) ⊆ f -``K" by auto with jp(1,2) have A:"((f -`` J) ⋅⇩_{I}(f -`` P)) +⇩_{I}(ker) ⊆ f -``K" using prime_ideal_quot assms(2) by auto moreover have j:"J◃R⇩_{t}" and p:"P◃R⇩_{t}" using jp(1,2) by auto then have "(f -`` J) ⋅⇩_{I}(f -`` P) ∪ ker ⊆ R" using origin_ring.ideal_dest_subset[OF origin_ring.product_in_intersection(2) [OF preimage_ideal(1) preimage_ideal(1)]] origin_ring.ideal_dest_subset[OF preimage_ideal(1)[OF target_ring.zero_ideal]] by auto with A have "((f -`` J) ⋅⇩_{I}(f -`` P)) ⊆ f -``K" unfolding origin_ring.sumIdeal_def[OF origin_ring.product_in_intersection(2) [OF preimage_ideal(1)[OF j] preimage_ideal(1)[OF p]] preimage_ideal(1)[OF target_ring.zero_ideal]] using origin_ring.generated_ideal_contains_set[of "(f -`` J) ⋅⇩_{I}(f -`` P) ∪ ker"] by auto moreover have "f -`` J ∈ℐ" "f -`` P ∈ℐ" using preimage_ideal origin_ring.ideal_dest_subset jp(1,2) by auto ultimately have "f -`` J ⊆ f -`` K ∨ f -`` P ⊆ f -`` K" using as unfolding origin_ring.primeIdeal_def by auto then have "f``(f -`` J) ⊆ f``(f -`` K) ∨ f``(f -`` P) ⊆ f``(f -`` K)" by blast then have "J ⊆ K ∨ P ⊆ K" using assms(2) surj_image_vimage jp(1,2) assms target_ring.ideal_dest_subset by auto } ultimately show "K◃⇩_{p}R⇩_{t}" unfolding target_ring.primeIdeal_def by auto } qed corollary (in ring_homo) bij_prime_ideals: defines "idealFun ≡ λJ∈target_ring.ideals. f-``J" assumes "f:surj(R,S)" shows "restrict(idealFun,{J∈Pow(S). J◃⇩_{p}R⇩_{t}})∈bij({J∈Pow(S). J◃⇩_{p}R⇩_{t}}, {J∈Pow(R). ker⊆J ∧ (J◃⇩_{p}R)})" proof- have "{J∈Pow(S). J◃⇩_{p}R⇩_{t}} ⊆ target_ring.ideals" unfolding target_ring.primeIdeal_def by auto then have rest_bij:"restrict(idealFun,{J∈Pow(S). J◃⇩_{p}R⇩_{t}})∈bij({J∈Pow(S). J◃⇩_{p}R⇩_{t}}, idealFun``{J∈Pow(S). J◃⇩_{p}R⇩_{t}})" using restrict_bij assms(2) ideal_quot_bijection unfolding bij_def idealFun_def by auto { fix t assume t:"t∈idealFun``{J∈Pow(S). J◃⇩_{p}R⇩_{t}}" have sub:"{J∈Pow(S). J◃⇩_{p}R⇩_{t}} ⊆ target_ring.ideals" unfolding target_ring.primeIdeal_def by auto from t obtain q where q:"q∈{J∈Pow(S). J◃⇩_{p}R⇩_{t}}" "t=idealFun`q" using assms(2) func_imagedef[OF bij_is_fun[OF ideal_quot_bijection] sub] unfolding idealFun_def by auto note q(1) moreover then have "q∈target_ring.ideals" unfolding target_ring.primeIdeal_def by auto moreover with q(2) have "t = f-``q" "ker⊆t" "t◃R" unfolding idealFun_def using beta apply_type[OF ideal_quot_bijection[THEN bij_is_fun], of q] assms(2) by auto ultimately have "t◃R" "t◃⇩_{p}R" "ker⊆t" using assms(2) prime_ideal_quot_3 by auto } then have "idealFun `` Collect(Pow(S), prime_ideal_target) ⊆ {t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)}" using origin_ring.ideal_dest_subset by blast moreover { fix t assume "t∈{t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)}" then have t:"t∈Pow(R)" "ker⊆t" "t◃⇩_{p}R" by auto then have tSet:"t∈{t∈ℐ. ker ⊆ t}" unfolding origin_ring.primeIdeal_def by auto have "converse(idealFun)∈bij({t∈ℐ. ker ⊆ t}, target_ring.ideals)" using ideal_quot_bijection[OF assms(2)] bij_converse_bij unfolding idealFun_def by auto with tSet have cont:"converse(idealFun)`t ∈ target_ring.ideals" using apply_type[OF bij_is_fun] by blast moreover from tSet have eq:"idealFun`(converse(idealFun)`t) = t" using ideal_quot_bijection assms(2) unfolding idealFun_def using right_inverse_bij by blast ultimately have "f-``(converse(idealFun)`t) = t" using beta unfolding idealFun_def by auto with t(3) have "(converse(idealFun)`t) ◃⇩_{p}R⇩_{t}" using prime_ideal_quot_3 cont assms(2) by auto then have "(converse(idealFun)`t) ◃⇩_{p}R⇩_{t}" "(converse(idealFun)`t) ⊆ S" unfolding target_ring.primeIdeal_def using target_ring.ideal_dest_subset by auto then have elem:"converse(idealFun)`t∈{q∈Pow(S). q◃⇩_{p}R⇩_{t}}" by auto have sub:"{q∈Pow(S). q◃⇩_{p}R⇩_{t}} ⊆ target_ring.ideals" unfolding target_ring.primeIdeal_def by auto have "t∈idealFun``Collect(Pow(S), prime_ideal_target)" using assms(2) func_imagedef[OF ideal_quot_bijection[THEN bij_is_fun] sub] unfolding idealFun_def using eq elem unfolding idealFun_def by auto } then have "{t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)} ⊆ idealFun``Collect(Pow(S), prime_ideal_target)" by auto ultimately have "{t∈Pow(R). ker⊆t ∧ (t◃⇩_{p}R)} = idealFun``Collect(Pow(S), prime_ideal_target)" by auto with rest_bij show ?thesis by auto qed end