stalkIso'_germ — Mathlib

English

There is a canonical equivalence between the homogeneous localization at x and the stalk at x, realized by composing the previous isomorphisms in both directions.

Русский

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

LaTeX

$$$(\text{stalkIso}'_{\mathcal{A}}(x))^{-1} \circ \text{homogeneousLocalizationToStalk}_{\mathcal{A}}(x, -) = \mathrm{id}$$$

Lean4

@[simp]
theorem stalkIso'_germ (U : Opens (ProjectiveSpectrum.top 𝒜)) (x : ProjectiveSpectrum.top 𝒜) (hx : x ∈ U)
    (s : (Proj.structureSheaf 𝒜).1.obj (op U)) :
    Proj.stalkIso' 𝒜 x ((Proj.structureSheaf 𝒜).presheaf.germ _ x hx s) = s.1 ⟨x, hx⟩ :=
  stalkToFiberRingHom_germ 𝒜 U x hx s

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