stalkSpecializes_refl — Mathlib

English

Composition of specialization maps is compatible with the stalkSpecializes operation.

Русский

Согласованность композиции операций специализации над стэлами.

LaTeX

$$stalkSpecializes_comp {C} {X} {F} {h} {h'}$$

Lean4

@[simp]
theorem stalkSpecializes_refl {C : Type*} [Category C] [Limits.HasColimits C] {X : TopCat} (F : X.Presheaf C) (x : X) :
    F.stalkSpecializes (specializes_refl x) = 𝟙 _ := by
  ext
  simp

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