exists_ideal_over_prime_of_isIntegral

English

Under integrality, there exists an extension Q of I with Q prime and Q.comap = P.

Русский

При интегральности существует расширение Q над I, такое что Q является простым и Q.comap = P.

LaTeX

$$$$\exists Q \ge I,\ Q \text{ prime},\ Q^{\mathrm{comap}} = P.$$$$

Lean4

theorem exists_ideal_over_prime_of_isIntegral [Algebra.IsIntegral R S] (P : Ideal R) [IsPrime P] (I : Ideal S)
    (hIP : I.comap (algebraMap R S) ≤ P) : ∃ Q ≥ I, IsPrime Q ∧ Q.comap (algebraMap R S) = P :=
  by
  have ⟨P', hP, hP', hP''⟩ := exists_ideal_comap_le_prime P I hIP
  obtain ⟨Q, hQ, hQ', hQ''⟩ := exists_ideal_over_prime_of_isIntegral_of_isPrime P P' hP''
  exact ⟨Q, hP.trans hQ, hQ', hQ''⟩

Похожие утверждения