English
If for every prime P of S the localized map Spec S_p → Spec R_p is surjective, then going down holds for R → S.
Русский
Если для каждого прима S локализованный переход Spec S_p → Spec R_p сюръективен, тогда свойствоGoingDown верно для R → S.
LaTeX
$$$\text{If } \forall P, \text{Prime}(S), \; \text{surjective}(\text{Localization.localRingHom } (P.under R) P (algebraMap R S)).\text{specComap}, \text{then } Algebra.HasGoingDown R S.$$$
Lean4
/-- An `R`-algebra `S` has the going down property if and only if generalizations lift
along `Spec S → Spec R`. -/
@[stacks 00HW "(1)"]
theorem iff_generalizingMap_primeSpectrumComap :
Algebra.HasGoingDown R S ↔ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S)) :=
by
refine ⟨?_, fun h ↦ ⟨fun {p} hp Q hQ hlt ↦ ?_⟩⟩
· intro h Q p hp
rw [← PrimeSpectrum.le_iff_specializes] at hp
obtain ⟨P, hle, hP, h⟩ := Q.asIdeal.exists_ideal_le_liesOver_of_le (p := p.asIdeal) (q := Q.asIdeal.under R) hp
refine ⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩
ext : 1
exact h.over.symm
· have : (⟨p, hp⟩ : PrimeSpectrum R) ⤳ (PrimeSpectrum.comap (algebraMap R S) ⟨Q, hQ⟩) :=
(PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
obtain ⟨P, hs, heq⟩ := h this
refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩
simpa [PrimeSpectrum.ext_iff] using heq.symm
