stalkIso — Mathlib

English

The inverse of the isomorphism's hom composed with fst yields the away-map on the left side.

Русский

Обратный образ модуля-изоморфизма после fst даёт away-map слева.

LaTeX

$$$(pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv \\circ \\mathrm{Limits.pullback.fst} = \\mathrm{awayMap}(𝒜, f_deg, hx)$$$

Lean4

/-- The stalk of `Proj A` at `x` is the degree `0` part of the localization of `A` at `x`. -/
noncomputable def stalkIso (x : Proj 𝒜) : (Proj 𝒜).presheaf.stalk x ≅ .of (AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) :=
  (stalkIso' 𝒜 x).toCommRingCatIso

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