English
Let F, G be functors from J to C. For a cocone c over F and a cocone d over G, with hc an IsColimit on c, and α: F ⟶ G, for every j in J the leg c.ι.app j followed by the colimit map IsColimit.map hc d α equals the leg α.app j followed by the leg d.ι.app j. In words, the universal cocone map commutes with the legs of the cocones via α.
Русский
Пусть F, G — функторы из J в C. Пусть коконы c над F и d над G, с hc, являющимся IsColimit, и α: F ⟶ G. Для каждого j ∈ J выполняется равенство c.ι.app j ≫ IsColimit.map hc d α = α.app j ≫ d.ι.app j. Иными словами, универсальное отображение кокона сохраняет естественность относительно α.
LaTeX
$$$ \forall {F,G : J \to C} {c : Cocone F} (hc : IsColimit c) {d : Cocone G} (α : F \to G) (j : J),\\ c.\iota.app j \\!\\,\\! IsColimit.map hc d α = α.app j \\!\\,\\! d.\iota.app j $$$
Lean4
@[reassoc (attr := simp)]
theorem ι_map {F G : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (d : Cocone G) (α : F ⟶ G) (j : J) :
c.ι.app j ≫ IsColimit.map hc d α = α.app j ≫ d.ι.app j :=
fac _ _ _
