ΓSpecIso_hom_stalkClosedPointIso_inv

English

The inverse of the stalk-closed-point isomorphism coincides with StructureSheaf.toStalk; hence the stalk identity at the closed point is given by localization to the stalk.

Русский

Обратное к изоморфизму stalk-closed-point совпадает с StructureSheaf.toStalk; следовательно, stalk-identity в закрытой точке задаётся локализацией в stalk.

LaTeX

$$stalkClosedPointIso_inv : (stalkClosedPointIso R).inv = StructureSheaf.toStalk R _$$

Lean4

theorem ΓSpecIso_hom_stalkClosedPointIso_inv :
    (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (closedPoint _) trivial :=
  by
  rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]
  rfl

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