stalkMap_congr — Mathlib

English

If f = g, then there is a simple expression expressing f.stalkMap x as the composition of a conjugation with g.stalkMap x.

Русский

Если f = g, то f.stalkMap x выражается как композиция конъюгации и g.stalkMap x.

LaTeX

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

Lean4

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

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