English
Given P prime in R and I prime in S with hIP, there exists Q in S, prime, with Q.comap (algebraMap R S) = P.
Русский
Пусть P — простой идеал в R и I — простой идеал в S, удовлетворяющий hIP; тогда существует Q в S, простой, с Q.comap (algebraMap R S) = P.
LaTeX
$$$$\exists Q \ge I,\ Q \text{ prime},\ Q^{\mathrm{comap}} = P.$$$$
Lean4
/-- `comap (algebraMap R S)` is a surjection from the prime spec of `R` to prime spec of `S`.
`hP : (algebraMap R S).ker ≤ P` is a slight generalization of the extension being injective -/
theorem exists_ideal_over_prime_of_isIntegral_of_isDomain [Algebra.IsIntegral R S] (P : Ideal R) [IsPrime P]
(hP : RingHom.ker (algebraMap R S) ≤ P) : ∃ Q : Ideal S, IsPrime Q ∧ Q.comap (algebraMap R S) = P :=
by
have hP0 : (0 : S) ∉ Algebra.algebraMapSubmonoid S P.primeCompl :=
by
rintro ⟨x, ⟨hx, x0⟩⟩
exact absurd (hP x0) hx
let Rₚ := Localization P.primeCompl
let Sₚ := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
letI : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
obtain ⟨Qₚ : Ideal Sₚ, Qₚ_maximal⟩ := exists_maximal Sₚ
let _ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
have : Algebra.IsIntegral Rₚ Sₚ := ⟨isIntegral_localization⟩
have Qₚ_max : IsMaximal (comap _ Qₚ) := isMaximal_comap_of_isIntegral_of_isMaximal (R := Rₚ) (S := Sₚ) Qₚ
refine ⟨comap (algebraMap S Sₚ) Qₚ, ⟨comap_isPrime _ Qₚ, ?_⟩⟩
convert Localization.AtPrime.comap_maximalIdeal (I := P)
rw [comap_comap, ← IsLocalRing.eq_maximalIdeal Qₚ_max, ←
IsLocalization.map_comp (P := S) (Q := Sₚ) (g := algebraMap R S) (M := P.primeCompl) (T :=
Algebra.algebraMapSubmonoid S P.primeCompl) (S := Rₚ)
(fun p hp => Algebra.mem_algebraMapSubmonoid_of_mem ⟨p, hp⟩)]
rfl
