stalkMap_congr_hom — Mathlib

English

For f: X ⟶ Y and x = x' in X, the stalk maps at x and x' are related by a simple congruence with respect to the base.

Русский

Для f: X ⟶ Y и x = x' отношение stalkMap между точками упрощено через конгруэнцию.

LaTeX

$$f.stalkMap x = (Y.presheaf.stalkCongr (.of_eq <| hxx' ▸ rfl)).hom ≫ g.stalkMap x$$

Lean4

@[reassoc]
theorem stalkMap_congr_hom (f g : X ⟶ Y) (hfg : f = g) (x : X) :
    f.stalkMap x = (Y.presheaf.stalkCongr (.of_eq <| hfg ▸ rfl)).hom ≫ g.stalkMap x :=
  LocallyRingedSpace.stalkMap_congr_hom f.toLRSHom g.toLRSHom congr(($hfg).toLRSHom) x

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