nonempty_primesOver — Mathlib

English

If R is a commutative ring and S is integral over R with NoZeroDivisors, then for any prime P in R there exists a prime Q in S lying over P.

Русский

Если R — кольцо и S интегрально над R с отсутствием нулевых делителей, то для любого простого P в R существует простой Q в S над P.

LaTeX

$$$$\forall P \text{ prime in } R,\ exists\ Q \text{ prime in } S\ with\ liesOver(Q,P). $$$$

Lean4

instance nonempty_primesOver [Nontrivial S] [Algebra.IsIntegral R S] [NoZeroSMulDivisors R S] (P : Ideal R)
    [P.IsPrime] : Nonempty (primesOver P S) :=
  by
  obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_ideal_over_prime_of_isIntegral P (⊥ : Ideal S) (by simp)
  exact ⟨Q, ⟨hQ₁, (liesOver_iff _ _).mpr hQ₂.symm⟩⟩

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