[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
suffices
  ∃ m ∈ {p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p},
    OrderDual.toDual J ≤ m ∧ ∀ z ∈ {p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p}, m ≤ z → z = m
  by
  obtain ⟨p, h₁, h₂, h₃⟩ := this
  simp_rw [← @eq_comm _ p] at h₃ 
  exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
this :
  ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
obtain ⟨p, h₁, h₂, h₃⟩ := this
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → z = p
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
simp_rw [← @eq_comm _ p] at h₃ 
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → p = z
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
[PROOFSTEP]
apply zorn_nonempty_partialOrder₀
[GOAL]
case ih
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
case hxs
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
[PROOFSTEP]
swap
[GOAL]
case hxs
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
[PROOFSTEP]
refine' ⟨show J.IsPrime by infer_instance, e⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ IsPrime J
[PROOFSTEP]
infer_instance
[GOAL]
case ih
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
[PROOFSTEP]
rintro (c : Set (Ideal R)) hc hc' J' hJ'
[GOAL]
case ih
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
[PROOFSTEP]
refine' ⟨OrderDual.toDual (sInf c), ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, _⟩, _⟩
[GOAL]
case ih.refine'_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ I ≤ ↑OrderDual.ofDual (↑OrderDual.toDual (sInf c))
[PROOFSTEP]
rw [OrderDual.ofDual_toDual, le_sInf_iff]
[GOAL]
case ih.refine'_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (b : Ideal R), b ∈ c → I ≤ b
[PROOFSTEP]
exact fun _ hx => (hc hx).2
[GOAL]
case ih.refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ↑OrderDual.toDual (sInf c)
[PROOFSTEP]
rintro z hz
[GOAL]
case ih.refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ ↑OrderDual.toDual (sInf c)
[PROOFSTEP]
rw [OrderDual.le_toDual]
[GOAL]
case ih.refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ sInf c ≤ ↑OrderDual.ofDual z
[PROOFSTEP]
exact sInf_le hz
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes (radical I) = Ideal.minimalPrimes I
[PROOFSTEP]
rw [Ideal.minimalPrimes, Ideal.minimalPrimes]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
ext p
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} ↔
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case h.refine'_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} →
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
rintro ⟨⟨a, ha⟩, b⟩
[GOAL]
case h.refine'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p} →
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
[PROOFSTEP]
rintro ⟨⟨a, ha⟩, b⟩
[GOAL]
case h.refine'_1.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩
[GOAL]
case h.refine'_1.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
[PROOFSTEP]
simp only [Set.mem_setOf_eq, and_imp] at *
[GOAL]
case h.refine'_1.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : radical I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
[PROOFSTEP]
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4
[GOAL]
case h.refine'_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
[PROOFSTEP]
refine' ⟨⟨a, a.radical_le_iff.2 ha⟩, _⟩
[GOAL]
case h.refine'_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
[PROOFSTEP]
simp only [Set.mem_setOf_eq, and_imp] at *
[GOAL]
case h.refine'_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
[PROOFSTEP]
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = radical I
[PROOFSTEP]
rw [I.radical_eq_sInf]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) ≤ sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
intro x hx
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : x ∈ sInf (Ideal.minimalPrimes I)
⊢ x ∈ sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
rw [Ideal.mem_sInf] at hx ⊢
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsPrime J} → x ∈ I_1
[PROOFSTEP]
rintro J ⟨e, hJ⟩
[GOAL]
case a.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
⊢ x ∈ J
[PROOFSTEP]
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e
[GOAL]
case a.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
p : Ideal R
hp : p ∈ Ideal.minimalPrimes I
hp' : p ≤ J
⊢ x ∈ J
[PROOFSTEP]
exact hp' (hx hp)
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf {J | I ≤ J ∧ IsPrime J} ≤ sInf (Ideal.minimalPrimes I)
[PROOFSTEP]
apply sInf_le_sInf _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes I ⊆ {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
intro I hI
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J I : Ideal R
hI : I ∈ Ideal.minimalPrimes I✝
⊢ I ∈ {J | I✝ ≤ J ∧ IsPrime J}
[PROOFSTEP]
exact hI.1.symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
have := H.1.1
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
have : Nontrivial (Localization (Submonoid.map f p.primeCompl)) :=
  by
  refine' ⟨⟨1, 0, _⟩⟩
  convert
    (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p)
          (Localization <| p.primeCompl.map f) hf).ne
      one_ne_zero
  · rw [map_one]
  · rw [map_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ Nontrivial (Localization (Submonoid.map f (primeCompl p)))
[PROOFSTEP]
refine' ⟨⟨1, 0, _⟩⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 ≠ 0
[PROOFSTEP]
convert
  (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p) (Localization <| p.primeCompl.map f)
        hf).ne
    one_ne_zero
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      1
[PROOFSTEP]
rw [map_one]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 0 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      0
[PROOFSTEP]
rw [map_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl))
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, _⟩
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap f (comap (algebraMap S (Localization (Submonoid.map f (primeCompl p)))) M) = p
[PROOFSTEP]
rw [Ideal.comap_comap, ←
  @IsLocalization.map_comp _ _ _ _ _ _ _ _ Localization.isLocalization _ _ _ _ p.primeCompl.le_comap_map _
    Localization.isLocalization,
  ← Ideal.comap_comap]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
[PROOFSTEP]
suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝¹ : IsPrime p
this✝ : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
this : ?m.48761 ≤ p
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
[PROOFSTEP]
exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) ≤
    p
[PROOFSTEP]
intro x hx
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
⊢ x ∈ p
[PROOFSTEP]
by_contra h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ False
[PROOFSTEP]
apply hM.ne_top
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ M = ⊤
[PROOFSTEP]
apply M.eq_top_of_isUnit_mem hx
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit
    (↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      (↑(algebraMap R (Localization (primeCompl p))) x))
[PROOFSTEP]
apply IsUnit.map
[GOAL]
case intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit (↑(algebraMap R (Localization (primeCompl p))) x)
[PROOFSTEP]
apply IsLocalization.map_units _ (show p.primeCompl from ⟨x, h⟩)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have := H.1.1
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
let f' := (Ideal.Quotient.mk I).comp f
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have e : RingHom.ker f' = I.comap f := by
  ext1
  exact Submodule.Quotient.mk_eq_zero _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ RingHom.ker f' = comap f I
[PROOFSTEP]
ext1
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
x✝ : R
⊢ x✝ ∈ RingHom.ker f' ↔ x✝ ∈ comap f I
[PROOFSTEP]
exact Submodule.Quotient.mk_eq_zero _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p :=
  by
  rw [Ideal.mk_ker, e]
  exact H.1.2
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
[PROOFSTEP]
rw [Ideal.mk_ker, e]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ comap f I ≤ p
[PROOFSTEP]
exact H.1.2
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
suffices _
  by
  have ⟨p', hp₁, hp₂⟩ :=
    Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective (RingHom.kerLift_injective f')
      (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this
  refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩
  · exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le)
  · convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂
    rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') Ideal.Quotient.mk_surjective, eq_comm,
      sup_eq_left]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : ?m.53321
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have ⟨p', hp₁, hp₂⟩ :=
  Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective (RingHom.kerLift_injective f')
    (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ I ≤ comap (Quotient.mk I) p'
[PROOFSTEP]
exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le)
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ comap f (comap (Quotient.mk I) p') = p
[PROOFSTEP]
convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ p = comap (Quotient.mk (RingHom.ker f')) (map (Quotient.mk (RingHom.ker f')) p)
[PROOFSTEP]
rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') Ideal.Quotient.mk_surjective, eq_comm,
  sup_eq_left]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
[PROOFSTEP]
refine' ⟨⟨_, bot_le⟩, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ IsPrime (map (Quotient.mk (RingHom.ker f')) p)
[PROOFSTEP]
apply Ideal.map_isPrime_of_surjective _ this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker f'))
[PROOFSTEP]
exact Ideal.Quotient.mk_surjective
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∀ ⦃b : Ideal (R ⧸ RingHom.ker f')⦄,
    b ∈ {p | IsPrime p ∧ ⊥ ≤ p} →
      (fun x x_1 => x ≤ x_1) b (map (Quotient.mk (RingHom.ker f')) p) →
        (fun x x_1 => x ≤ x_1) (map (Quotient.mk (RingHom.ker f')) p) b
[PROOFSTEP]
rintro q ⟨hq, -⟩ hq'
[GOAL]
case refine'_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤ q
[PROOFSTEP]
rw [←
  Ideal.map_comap_of_surjective (Ideal.Quotient.mk (RingHom.ker ((Ideal.Quotient.mk I).comp f)))
    Ideal.Quotient.mk_surjective q]
[GOAL]
case refine'_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤
    map (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
      (comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q)
[PROOFSTEP]
apply Ideal.map_mono
[GOAL]
case refine'_2.intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ≤ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q
[PROOFSTEP]
apply H.2
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ∈ {p | IsPrime p ∧ comap f I ≤ p}
[PROOFSTEP]
refine' ⟨inferInstance, (Ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ≤ p
[PROOFSTEP]
refine' (Ideal.comap_mono hq').trans _
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) (map (Quotient.mk (RingHom.ker f')) p) ≤ p
[PROOFSTEP]
rw [Ideal.comap_map_of_surjective]
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ⊔ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) ⊥ ≤ p
case refine'_2.intro.h.a.hf
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
[PROOFSTEP]
exacts [sup_le rfl.le this, Ideal.Quotient.mk_surjective]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
[PROOFSTEP]
obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
[PROOFSTEP]
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
[PROOFSTEP]
refine' ⟨q, hq, Eq.symm _⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ p = comap f q
[PROOFSTEP]
have := hq.1.1
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this : IsPrime q
⊢ p = comap f q
[PROOFSTEP]
have := (Ideal.comap_mono hq').trans_eq h₃
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this✝ : IsPrime q
this : comap f q ≤ p
⊢ p = comap f q
[PROOFSTEP]
exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
have := h.1.1
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ ∀ ⦃b : Ideal R⦄,
    b ∈ {p | IsPrime p ∧ comap f I ≤ p} → (fun x x_1 => x ≤ x_1) b (comap f J) → (fun x x_1 => x ≤ x_1) (comap f J) b
[PROOFSTEP]
rintro K ⟨hK, e₁⟩ e₂
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
⊢ comap f J ≤ K
[PROOFSTEP]
have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K
[PROOFSTEP]
rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ comap f (map f K)
[PROOFSTEP]
apply Ideal.comap_mono _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ J ≤ map f K
[PROOFSTEP]
apply h.2 _ _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ∈ {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J
[PROOFSTEP]
exact Ideal.map_le_of_le_comap e₂
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
⊢ Ideal.minimalPrimes (comap f I) = comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) ↔ J ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) → J ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
intro H
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
H : J ∈ Ideal.minimalPrimes (comap f I)
⊢ J ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
[GOAL]
case h.mp.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I p : Ideal S
h : p ∈ Ideal.minimalPrimes I
H : comap f p ∈ Ideal.minimalPrimes (comap f I)
⊢ comap f p ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
exact ⟨p, h, rfl⟩
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' Ideal.minimalPrimes I → J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
rintro ⟨J, hJ, rfl⟩
[GOAL]
case h.mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
hJ : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
exact Ideal.mimimal_primes_comap_of_surjective hf hJ
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes I = comap (Quotient.mk I) '' minimalPrimes (R ⧸ I)
[PROOFSTEP]
rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective, ←
  RingHom.ker_eq_comap_bot, Ideal.mk_ker]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ Ideal.minimalPrimes I = {radical I}
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {radical I}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {radical I}
[PROOFSTEP]
exact fun H =>
  let e := H.1.1.radical_le_iff.mpr H.1.2
  (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ {radical I} → J ∈ Ideal.minimalPrimes I
[PROOFSTEP]
rintro (rfl : J = I.radical)
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ radical I ∈ Ideal.minimalPrimes I
[PROOFSTEP]
exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime I
⊢ Ideal.minimalPrimes I = {I}
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {I}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {I}
[PROOFSTEP]
exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ {I} → J ∈ Ideal.minimalPrimes I
[PROOFSTEP]
rintro (rfl : J = I)
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
J✝ J : Ideal R
inst✝ : IsPrime J
⊢ J ∈ Ideal.minimalPrimes J
[PROOFSTEP]
refine' ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩
