stalkMap_congr — Mathlib

English

If morphisms f and g are equal, then their stalk maps agree up to the appropriate specialization, expressing coherence when f = g.

Русский

Если гомоморфизмы f и g равны, то их stalk‑отображения совпадают с учётом соответствующей специализации, обеспечивая когерентность при f = g.

LaTeX

$$$$f = g \\Rightarrow f.stalkMap x \\circ X.presheaf.stalkSpecializes (\\mathrm{specializes\\_of\\_eq}\\,\\cdot) = g.stalkMap x' \\circ Y.presheaf.stalkSpecializes (\\mathrm{specializes\\_of\\_eq}\\,\\cdot).$$$$

Lean4

@[reassoc]
theorem stalkMap_congr (f g : X ⟶ Y) (hfg : f = g) (x x' : X) (hxx' : x = x') :
    f.stalkMap x ≫ X.presheaf.stalkSpecializes (specializes_of_eq hxx'.symm) =
      Y.presheaf.stalkSpecializes (specializes_of_eq <| hfg ▸ hxx' ▸ rfl) ≫ g.stalkMap x' :=
  by
  subst hfg
  subst hxx'
  simp

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