ι_desc_app — Mathlib

English

For a colimit of a functor H : J ⥤ K ⥤ C with cocone c, the componentwise description of the universal morphism aligns with the induced cocone maps

Русский

Для колимита F : J ⥤ K ⥤ C с коконом c свойство компоновок мортимов согласуется с отображениями кокона

LaTeX

$$$\\bigl(\\text{colimit}.\\iota H j\\bigr)\\!\\cdot\\!\\text{(cocone part)} \\,=\\, (c.\\iota.app j).\\mathrm{app}\\; k$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_desc_app (H : J ⥤ K ⥤ C) [HasColimit H] (c : Cocone H) (j : J) (k : K) :
    (colimit.ι H j).app k ≫ (colimit.desc H c).app k = (c.ι.app j).app k :=
  congr_app (colimit.ι_desc c j) k

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