Theory Ring_ZF_3

(*
    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>⇩Rb ≡ A`⟨x,b⟩"

  fixes ringminus ("\<rm>⇩R _" 89)
  defines ringminus_def [simp]: "(\<rm>⇩Rx) ≡ GroupInv(R,A)`(x)"

  fixes ringsub (infixl "\<rs>⇩R" 90)
  defines ringsub_def [simp]: "x\<rs>⇩Rb ≡ x\<ra>⇩R(\<rm>⇩Rb)"

  fixes ringm (infixl "⋅⇩R" 95)
  defines ringm_def [simp]: "x⋅⇩Rb ≡ 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⋅⇩Rx"

  fixes ringas (infixl "\<ra>⇩S" 90)
  defines ringas_def [simp]: "x\<ra>⇩Sb ≡ U`⟨x,b⟩"

  fixes ringminuss ("\<rm>⇩S _" 89)
  defines ringminuss_def [simp]: "(\<rm>⇩Sx) ≡ GroupInv(S,U)`(x)"

  fixes ringsubs (infixl "\<rs>⇩S" 90)
  defines ringsubs_def [simp]: "x\<rs>⇩Sb ≡ x\<ra>⇩S(\<rm>⇩Sb)"

  fixes ringms (infixl "⋅⇩S" 95)
  defines ringms_def [simp]: "x⋅⇩Sb ≡ 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⋅⇩Sx"

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 ("_◃⇩pR⇩t")
  where "I◃⇩pR⇩t ≡ ring0.primeIdeal(S,U,V,I)"

abbreviation (in ring_homo) prime_ideal_origin ("_◃⇩pR⇩o")
  where "I◃⇩pR⇩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⋅⇩Ry) = (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>⇩Ry) = (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>⇩Rx) = \<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>⇩Ry) = (f`x)\<rs>⇩S(f`y)"
  using assms homomor_dest_add[of x "\<rm>⇩Ry"]
    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◃⇩pR⇩t" "V{is commutative on}S"
  shows "(f-``J)◃⇩pR⇩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)⋅⇩Ss⋅⇩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)⋅⇩Ss⋅⇩S(f`y) = s⋅⇩S(f`(x⋅⇩Ry))"
        using homomor_dest_mult[OF as(1,2)]
        by auto moreover
      from as(3) have "x⋅⇩Ry : 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⋅⇩Ry) : J" using func1_1_L15 fun by auto
      with s have "s⋅⇩S(f`(x⋅⇩Ry)) :J" using assms(1)
        unfolding target_ring.primeIdeal_def using target_ring.ideal_dest_mult(2)
        by auto
      ultimately have "(f`x)⋅⇩Ss⋅⇩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◃⇩pR⇩t" "f:surj(R,S)"
  shows "(f-``J)◃⇩pR⇩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⋅⇩Rt⋅⇩Ry)"
        using homomor_dest_mult as(1,2) t(2)
        origin_ring.Ring_ZF_1_L4(3) by auto
      moreover have "(x⋅⇩Rt⋅⇩Ry)∈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)⋅⇩Ss⋅⇩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 ("_◃⇩pR⇩I") where
  "J◃⇩pR⇩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+⇩II) = f``J" "f``(I+⇩IJ) = f``J"
proof-
  have sub:"J+⇩II ⊆ 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+⇩II)"
    then obtain q where q:"q∈J+⇩II" "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>⇩Rqi" 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>⇩Rqi)" 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+⇩II" unfolding origin_ring.sumIdeal_def[OF assms(1,3)].
    with q(2) have "t∈f``(J+⇩II)" 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⋅⇩Rs∈J" "s⋅⇩Rj∈J" using origin_ring.ideal_dest_mult[OF assms(1)]
      x(2) y(2) by auto
    ultimately have "(x⋅⇩Sy)∈f``J" "(y⋅⇩Sx)∈f``J"
      using func_imagedef fun origin_ring.ideal_dest_subset[OF assms(1)]
      by auto
  }
  then show "∀x∈f `` J. ∀y∈S. (y⋅⇩Sx) ∈ f `` J ∧ (x⋅⇩Sy) ∈ 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>⇩Rs) = 𝟬⇩S" using homomor_dest_subs
      t(2) ss by auto moreover
    from t(2) ss have "t\<rs>⇩Rs ∈R" using origin_ring.Ring_ZF_1_L4(2) by auto
    ultimately have "t\<rs>⇩Rs ∈ f-``{𝟬⇩S}" using func1_1_L15
      surj_is_fun[OF assms(3)] by auto
    then have "t\<rs>⇩Rs ∈ ?P" using p by auto
    then have "s\<ra>⇩R(t\<rs>⇩Rs) ∈ ?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⋅⇩Rtk" "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⋅⇩Rtk)" 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◃⇩pR⇩o" "ker ⊆ J" "f∈surj(R,S)"
  shows "(f``J)◃⇩pR⇩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>⇩Rj) =𝟬⇩S" using homomor_dest_subs
      t jt by auto moreover
    have "t\<rs>⇩Rj ∈R" using origin_ring.Ring_ZF_1_L4(2)
      t jt by auto
    ultimately have "t\<rs>⇩Rj∈f-``{𝟬⇩S}" using func1_1_L15[OF surj_is_fun]
      assms(3) by auto
    with assms(2) have tjJ:"t\<rs>⇩Rj∈J" by auto
    with j(1) have "j\<ra>⇩R(t\<rs>⇩Rj) ∈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>⇩Rs) = 𝟬⇩S" using homomor_dest_subs
        t(2) ss by auto
      moreover have "t\<rs>⇩Rs ∈R" using ss t(2)
        origin_ring.Ring_ZF_1_L4(2) by auto
      ultimately have "t\<rs>⇩Rs ∈ f-``{𝟬⇩S}" using func1_1_L15
        fun by auto
      with assms(2) have "t\<rs>⇩Rs ∈ J" by auto
      with s(2) have "s\<ra>⇩R(t\<rs>⇩Rs)∈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>⇩Rs) = 𝟬⇩S" using homomor_dest_subs
        t(2) `s:R` by auto
      moreover from ‹s∈R› have "t\<rs>⇩Rs ∈R" 
        using origin_ring.Ring_ZF_1_L4(2) t(2) by auto
      ultimately have "t\<rs>⇩Rs ∈ f-``{𝟬⇩S}"
        using func1_1_L15[OF surj_is_fun] assms(1) by auto
      with y(3) have "t\<rs>⇩Rs ∈ y" by auto
      with s(1) have "s\<ra>⇩R(t\<rs>⇩Rs) ∈ 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◃⇩pR⇩t ⟷ ((f-``K)◃⇩pR⇩o)"
proof
  {
    assume as:"K◃⇩pR⇩t"
    then have "(f-``K)◃⇩pR⇩o" using preimage_prime_ideal_surj
      assms(2) by auto
    then show "(f-``K)◃⇩pR⇩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)◃⇩pR⇩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◃⇩pR⇩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◃⇩pR⇩t})∈bij({J∈Pow(S). J◃⇩pR⇩t}, {J∈Pow(R). ker⊆J ∧ (J◃⇩pR)})"
proof-
  have "{J∈Pow(S). J◃⇩pR⇩t} ⊆ target_ring.ideals"
    unfolding target_ring.primeIdeal_def by auto
  then have rest_bij:"restrict(idealFun,{J∈Pow(S). J◃⇩pR⇩t})∈bij({J∈Pow(S). J◃⇩pR⇩t}, idealFun``{J∈Pow(S). J◃⇩pR⇩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◃⇩pR⇩t}"
    have sub:"{J∈Pow(S). J◃⇩pR⇩t} ⊆ target_ring.ideals"
      unfolding target_ring.primeIdeal_def by auto
    from t obtain q where q:"q∈{J∈Pow(S). J◃⇩pR⇩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◃⇩pR" "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◃⇩pR)}"
    using origin_ring.ideal_dest_subset by blast moreover
  {
    fix t assume "t∈{t∈Pow(R). ker⊆t ∧ (t◃⇩pR)}"
    then have t:"t∈Pow(R)" "ker⊆t" "t◃⇩pR" 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) ◃⇩pR⇩t"
      using prime_ideal_quot_3 cont assms(2) by auto
    then have "(converse(idealFun)`t) ◃⇩pR⇩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◃⇩pR⇩t}"
      by auto
    have sub:"{q∈Pow(S). q◃⇩pR⇩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◃⇩pR)} ⊆ idealFun``Collect(Pow(S), prime_ideal_target)" by auto
  ultimately
  have "{t∈Pow(R). ker⊆t ∧ (t◃⇩pR)} = idealFun``Collect(Pow(S), prime_ideal_target)"
    by auto
  with rest_bij show ?thesis by auto
qed
    
end