stalkMap_germ — Mathlib

English

The stalk map interacts with germ maps: the germ of a section at a point maps via stalkMap to the germ in the target stalk.

Русский

StalkMap взаимодействует с germ‑отображениями: образец секции в точке отображается через stalkMap к germ в целевом stalk.

LaTeX

$$$$\\text{stalkMap\\_germ: } f.\\mathrm{stalkMap} (\\text{germ}) = \\text{germ}\\, (\\text{map})$$$$

Lean4

@[reassoc (attr := simp)]
theorem stalkMap_germ (U : Opens Y) (x : X) (hx : f.base x ∈ U) :
    Y.presheaf.germ U (f.base x) hx ≫ f.stalkMap x = f.c.app (op U) ≫ X.presheaf.germ ((Opens.map f.base).obj U) x hx :=
  PresheafedSpace.stalkMap_germ f.toShHom U x hx

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