toLocallyRingedSpace — Mathlib

English

There exists a canonical ring isomorphism between the stalk at x and the homogeneous localization at x, compatible with the respective projections to the fiber and localized rings.

Русский

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

LaTeX

$$$(\mathrm{stalkIso}'_{\mathcal{A}}(x)): (\mathcal{O}_{X,x}) \cong \mathrm{AtPrime}_{\mathcal{A}} x$$$

Lean4

/-- `Proj` of a graded ring as a `LocallyRingedSpace` -/
def toLocallyRingedSpace : LocallyRingedSpace :=
  { Proj.toSheafedSpace 𝒜 with
    isLocalRing := fun x =>
      @RingEquiv.isLocalRing _ _ _ (show IsLocalRing (at x) from inferInstance) _ (Proj.stalkIso' 𝒜 x).symm }

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