ι_coconeMorphism — Mathlib

English

For any cocone c over F with a colimit, the j-th leg of the colimit composed with the cocone morphism equals the j-th leg of c: colimit.ι F j ≫ (colimit.coconeMorphism c).hom = c.ι.app j.

Русский

Для коконa над F, имеющего колимит, композиция инъекции колимита по j и гомоморса коконa совпадает с j-й компонентой кокона c: colimit.ι F j ≫ (colimit.coconeMorphism c).hom = c.ι.app j.

LaTeX

$$$\operatorname{colimit.\iota} F\;j \;\circ\; (\operatorname{colimit.coconeMorphism} c).{\rm hom} = c.ι_{\!j}$$$

Lean4

theorem ι_coconeMorphism {F : J ⥤ C} [HasColimit F] (c : Cocone F) (j : J) :
    colimit.ι F j ≫ (colimit.coconeMorphism c).hom = c.ι.app j := by simp

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