English
For any cocone c for F, and any j ∈ J, the equation colimit.ι F j ≫ colimit.desc F c = c.ι.app j holds.
Русский
Для любого кокона c для F и любого j ∈ J выполняется равенство colimit.ι F j ≫ colimit.desc F c = c.ι.app j.
LaTeX
$$$\\iota_F(j) \\;\\gg\\; \\text{desc}_F c = c.\\iota_j$$$
Lean4
/-- We have lots of lemmas describing how to simplify `colimit.ι F j ≫ _`,
and combined with `colimit.ext` we rely on these lemmas for many calculations.
However, since `Category.assoc` is a `@[simp]` lemma, often expressions are
right associated, and it's hard to apply these lemmas about `colimit.ι`.
We thus use `reassoc` to define additional `@[simp]` lemmas, with an arbitrary extra morphism.
(see `Tactic/reassoc_axiom.lean`)
-/
@[reassoc (attr := simp)]
theorem ι_desc {F : J ⥤ C} [HasColimit F] (c : Cocone F) (j : J) : colimit.ι F j ≫ colimit.desc F c = c.ι.app j :=
IsColimit.fac _ c j
