isPrime_carrier — Mathlib

English

The carrier ideal from FromSpec is prime for Proj top component; this ensures the image lands in a prime ideal in the corresponding localized spectrum.

Русский

Carrier-идеал FromSpec для компонента Proj является простым, следовательно образ принадлежит простому идеалу в локализованном спектре.

LaTeX

$$$\text{carrier}_{FromSpec}(f_{deg})\text{ prime}$$$

Lean4

theorem isPrime_carrier : Ideal.IsPrime (carrier x) :=
  by
  refine Ideal.IsPrime.comap _ (hK := ?_)
  exact
    IsLocalization.isPrime_of_isPrime_disjoint (Submonoid.powers f) _ _ inferInstance
      ((disjoint_powers_iff_notMem _ (Ideal.IsPrime.isRadical inferInstance)).mpr x.2)

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