-- Mathlib/RingTheory/Ideal/GoingDown.lean
/-- An `R`-algebra `S` has the going down property if and only if generalizations lift
along `Spec S → Spec R`. -/
@[stacks 00HW "(1)"]
lemma iff_generalizingMap_primeSpectrumComap :
    Algebra.HasGoingDown R S ↔
      GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

Proof state:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' Q ∧ (PrimeSpectrum.comap (algebraMap R S)) a' = p

Tactic:
obtain ⟨P, hle, hP, h⟩ := Q.asIdeal.exists_ideal_le_liesOver_of_le (p := p.asIdeal)
  (q := Q.asIdeal.under R) hp

Result:
case refine_1.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' Q ∧ (PrimeSpectrum.comap (algebraMap R S)) a' = p

Proof state:
case refine_1.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' Q ∧ (PrimeSpectrum.comap (algebraMap R S)) a' = p

Tactic:
refine ⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩

Result:
case refine_1.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := P, isPrime := hP } = p

Proof state:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := Q, isPrime := hQ }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hs, heq⟩ := h this

Result:
case refine_2.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := Q, isPrime := hQ }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : (PrimeSpectrum.comap (algebraMap R S)) P = { asIdeal := p, isPrime := hp }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case refine_1.intro.intro.intro.asIdeal
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ ((PrimeSpectrum.comap (algebraMap R S)) { asIdeal := P, isPrime := hP }).asIdeal = p.asIdeal

Tactic:
exact h.over.symm

Result:
no goals

Proof state:
case refine_2.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := Q, isPrime := hQ }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : (PrimeSpectrum.comap (algebraMap R S)) P = { asIdeal := p, isPrime := hp }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩

Result:
case refine_2.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := Q, isPrime := hQ }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : (PrimeSpectrum.comap (algebraMap R S)) P = { asIdeal := p, isPrime := hp }
⊢ p = Ideal.under R P.asIdeal

Proof state:
case refine_1.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := P, isPrime := hP } = p

Tactic:
ext : 1

Result:
case refine_1.intro.intro.intro.asIdeal
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ ((PrimeSpectrum.comap (algebraMap R S)) { asIdeal := P, isPrime := hP }).asIdeal = p.asIdeal

Proof state:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingDown R S → GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))

Tactic:
intro h Q p hp

Result:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ⤳ (PrimeSpectrum.comap (algebraMap R S)) Q
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' Q ∧ (PrimeSpectrum.comap (algebraMap R S)) a' = p

Proof state:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
have : (⟨p, hp⟩ : PrimeSpectrum R) ⤳ (PrimeSpectrum.comap (algebraMap R S) ⟨Q, hQ⟩) :=
  (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le

Result:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := Q, isPrime := hQ }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingDown R S ↔ GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))

Tactic:
refine ⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩

Result:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingDown R S → GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))

case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p