stalkMap_comp — Mathlib

English

For morphisms f: X → Y and g: Y → Z, the stalk map of their composition at x equals the composition of stalk maps in the reverse order: (f ≫ g).stalkMap x = g.stalkMap (f.base x) ≫ f.stalkMap x.

Русский

Для гомоморфизмов f: X → Y и g: Y → Z отображение stalk у их композиции равно композиции stalk‑отображений в обратном порядке.

LaTeX

$$$$ (f \\gg g).\\mathrm{stalkMap}\; x = g.\\mathrm{stalkMap}(f.\\mathrm{base}\ x) \\circ f.\\mathrm{stalkMap} x. $$$$

Lean4

theorem stalkMap_comp (x : X) : (f ≫ g : X ⟶ Z).stalkMap x = g.stalkMap (f.base x) ≫ f.stalkMap x :=
  PresheafedSpace.stalkMap.comp f.toShHom g.toShHom x

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