comap_ne_bot_of_root_mem — Mathlib

English

Let R,S be rings with Algebra Is Integral, and I ⊆ S an ideal with (I). IsPrime. Then if Q is a prime ideal of S, then there exists an extension Q over P with comap mapping back to P.

Русский

Пусть R,S кольца, и I ⊆ S прост, тогда существует идеал Q над I с комап-прообразом в P.

LaTeX

$$$$\exists Q\ge I,\ Q \text{ prime},\ Q.\mathrm{comap}(\mathrm{algebraMap} R S) = P.$$$$

Lean4

theorem comap_ne_bot_of_root_mem [IsDomain S] {r : S} (r_ne_zero : r ≠ 0) (hr : r ∈ I) {p : R[X]} (p_ne_zero : p ≠ 0)
    (hp : p.eval₂ f r = 0) : I.comap f ≠ ⊥ := fun h =>
  let ⟨_, hi, mem⟩ := exists_coeff_ne_zero_mem_comap_of_root_mem r_ne_zero hr p_ne_zero hp
  absurd (mem_bot.mp (eq_bot_iff.mp h mem)) hi

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