stalkSpecializes_comp — Mathlib

English

Specialization on the domain interacts compatibly with pushforward along f: the diagram with stalkPushforward commutes.

Русский

Специализация домена совместима с pushforward вдоль f: диаграмма со stalkPushforward коммутирует.

LaTeX

$$stalkSpecializes_stalkPushforward {f} {F} {x} {h}$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem stalkSpecializes_comp {C : Type*} [Category C] [Limits.HasColimits C] {X : TopCat} (F : X.Presheaf C)
    {x y z : X} (h : x ⤳ y) (h' : y ⤳ z) :
    F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h') :=
  by
  ext
  simp

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