comp_hom_app — Mathlib

English

In a composition of two morphisms f, g, the homogeneous component on an open U is the identity on that open's section.

Русский

В композиции морфизмов f, g компонент hom на открытом U равен тождественному отображению секций над U.

LaTeX

$$((comp f g ℱ).hom.app U) = 𝟙 _$$

Lean4

@[simp]
theorem comp_hom_app {X Y Z : TopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) (U) :
    (comp f g ℱ).hom.app U = 𝟙 _ :=
  rfl

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