stalkIso — Mathlib

English

The inverse of the stalk isomorphism equals the stalk map along the inclusion.

Русский

Обратный к изоморфизму сталков равен stalk-переходу вдоль включения.

LaTeX

$$$ (U.stalkIso x)^{-1} = U.\\iota.stalkMap x $$$

Lean4

/-- The stalks of an open subscheme are isomorphic to the stalks of the original scheme. -/
def stalkIso {X : Scheme.{u}} (U : X.Opens) (x : U) : U.toScheme.presheaf.stalk x ≅ X.presheaf.stalk x.1 :=
  X.restrictStalkIso (Opens.isOpenEmbedding _) _

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