exists_ideal_liesOver_maximal_of_isIntegral

English

If p is maximal in A and B is integral over A, there exists P maximal in B with P lies over p.

Русский

Если p максимален в A и B интегрально над A, существует P максимальный в B, лежащий над p.

LaTeX

$$$\exists P : \mathrm{Ideal}(B),\; P.\mathrmIsMaximal( ) \land P.\mathrmLiesOver(p)$$$

Lean4

theorem exists_ideal_liesOver_maximal_of_isIntegral [p.IsMaximal] (B : Type*) [CommRing B] [Nontrivial B] [Algebra A B]
    [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] : ∃ P : Ideal B, P.IsMaximal ∧ P.LiesOver p :=
  by
  obtain ⟨P, hm, hP⟩ := exists_ideal_over_maximal_of_isIntegral (S := B) p <| by simp
  exact ⟨P, hm, ⟨hP.symm⟩⟩

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