specStalkEquiv — Mathlib

English

A detailed part of the universal property of localization at a prime is established, showing compatibility with the decomposition data of homogeneous elements.

Русский

Доказана детальная часть универсальной характеристики локализации по простому идеалу, показывающая совместимость с разложением однородных элементов.

LaTeX

$$$$\text{IsLocalization atPrime with decomposition and compatibility conditions}$$$$

Lean4

/-- For an element `f ∈ A` with positive degree and a homogeneous ideal in `D(f)`, we have that the
stalk of `Spec A⁰_ f` at `y` is isomorphic to `A⁰ₓ` where `y` is the point in `Proj` corresponding
to `x`.
-/
def specStalkEquiv (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
    («Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x) ≅
      CommRingCat.of (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
  letI : Algebra (Away 𝒜 f) (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
    (mapId 𝒜 (Submonoid.powers_le.mpr x.2)).toAlgebra
  haveI := isLocalization_atPrime 𝒜 f x f_deg hm
  (IsLocalization.algEquiv (R := A⁰_ f) (M := ((toSpec 𝒜 f).base x).asIdeal.primeCompl) (S :=
      («Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) (Q :=
      AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)).toRingEquiv.toCommRingCatIso

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