English
Let R and S be commutative rings and f: R → S a ring hom with S integral over R. If P is a maximal ideal of R and ker(f) ≤ P, then there exists a maximal ideal Q of S such that Q.comap (algebraMap R S) = P.
Русский
Пусть R и S — коммутативные кольца, f: R → S — кольцо-гомоморф, причём S интегрально над R через f. Если P — максимальный идеал R и ker(f) ≤ P, то существует максимальный идеал Q S такой, что Q comap (алгебраобразующие) = P.
LaTeX
$$$\exists Q : \mathrm{Ideal}(S),\; \mathrm{IsMaximal}(Q) \land Q.\mathrm{comap}(\mathrm{algebraMap}\, R\, S) = P$$$
Lean4
/-- `comap (algebraMap R S)` is a surjection from the max spec of `S` to max spec of `R`.
`hP : (algebraMap R S).ker ≤ P` is a slight generalization of the extension being injective -/
theorem exists_ideal_over_maximal_of_isIntegral [Algebra.IsIntegral R S] (P : Ideal R) [P_max : IsMaximal P]
(hP : RingHom.ker (algebraMap R S) ≤ P) : ∃ Q : Ideal S, IsMaximal Q ∧ Q.comap (algebraMap R S) = P :=
by
obtain ⟨Q, -, Q_prime, hQ⟩ := exists_ideal_over_prime_of_isIntegral P ⊥ hP
exact ⟨Q, isMaximal_of_isIntegral_of_isMaximal_comap _ (hQ.symm ▸ P_max), hQ⟩
