comp — Mathlib

English

Let X, Y, Z be presheafed spaces and α: X → Y, β: Y → Z. For every x ∈ X, the stalk map of the composite equals the composition of the stalk maps: (α ≫ β).stalkMap x = (β.stalkMap (α.base x)) ∘ (α.stalkMap x).

Русский

Пусть X, Y, Z — предшаблонные пространства и α: X → Y, β: Y → Z. Для каждого x ∈ X отображение stalkMap для композиции равно композиции соответствующих stalkMap: (α ≫ β).stalkMap x = β.stalkMap (α.base x) ∘ α.stalkMap x.

LaTeX

$$$$(\\alpha \\gg \\beta).stalkMap x = (\\beta.stalkMap (\\alpha.base\\,x)) \\circ (\\alpha.stalkMap x)$$$$

Lean4

@[simp]
theorem comp {X Y Z : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : X) :
    (α ≫ β).stalkMap x =
      (β.stalkMap (α.base x) : Z.presheaf.stalk (β.base (α.base x)) ⟶ Y.presheaf.stalk (α.base x)) ≫
        (α.stalkMap x : Y.presheaf.stalk (α.base x) ⟶ X.presheaf.stalk x) :=
  by
  dsimp [Hom.stalkMap, stalkFunctor, stalkPushforward]
    -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159

  apply colimit.hom_ext
  rintro ⟨U, hU⟩
  simp

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