English
Relates pre-composition with isoColimitCocone: for s : ColimitCocone (E ⋙ F) and t : ColimitCocone F, colimit.pre F E equals the composite with (colimit.isoColimitCocone s).hom, s.isColimit.desc (t.cocone.whisker E), and (colimit.isoColimitCocone t).inv.
Русский
Связь pre-композиции с isoColimitCocone: для s : ColimitCocone (E ⋙ F) и t : ColimitCocone F выполняется равенство colimit.pre F E = (colimit.isoColimitCocone s).hom ∘ s.isColimit.desc (t.cocone.whisker E) ∘ (colimit.isoColimitCocone t).inv.
LaTeX
$$$ \\operatorname{colimit.pre} F E = (\\operatorname{colimit.isoColimitCocone} s).hom \\; \\circ \\; s.isColimit.desc (t.cocone.whisker E) \\; \\circ \\; (\\operatorname{colimit.isoColimitCocone} t).inv $$$
Lean4
instance colimMap_epi {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) [∀ j, Epi (α.app j)] : Epi (colimMap α) :=
⟨fun {Z} u v h => colimit.hom_ext fun j => (cancel_epi (α.app j)).1 <| by simpa using colimit.ι _ j ≫= h⟩
