English
If s and t are colimit cocones for E ⋙ F and F respectively, then the colimit pre F E equals the composite built from the isoColimitCocone of s, the isColimit descent of t whiskered by E, and the inverse of the isoColimitCocone of t.
Русский
Если s и t — коконы колимита для E ⋙ F и F соответственно, то colimit.pre F E равен композиции, составленной из изоморфного кокона s, desc через t, подвергнутого whisker'у E, и обратного изоморога кокона t.
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
/-- -
If we have particular colimit cocones available for `E ⋙ F` and for `F`,
we obtain a formula for `colimit.pre F E`.
-/
theorem pre_eq (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 :=
by cat_disch
