stalkMap_germ_apply — Mathlib

English

Applying stalkMap to a germ yields the induced germ in the target stalk after applying the corresponding map.

Русский

Применение stalkMap к герму даёт соответствующую гермy в целевом stalk после применения соответствующего отображения.

LaTeX

$$$$f.stalkMap x (Y.presheaf.germ U (f.base x) hx y) = X.presheaf.germ ((Opens.map f.base).obj U) x hx (f.c.app (op U) y).$$$$

Lean4

theorem stalkMap_germ_apply (U : Opens Y) (x : X) (hx : f.base x ∈ U) (y) :
    f.stalkMap x (Y.presheaf.germ U (f.base x) hx y) =
      X.presheaf.germ ((Opens.map f.base).obj U) x hx (f.c.app (op U) y) :=
  PresheafedSpace.stalkMap_germ_apply f.toShHom U x hx y

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