English
For colimits along F and E, G, the two natural ways to compose pre- and post-operations on colimits agree: colimit.post (E ⋙ F) G ≫ G.map (colim.map α) = colim.map (whiskerRight α G) ≫ colimit.post F G.
Русский
Для колимитов по F и E, G существует согласование двух естественных способов последовательного применения прe- и пост-операций: colimit.post (E ⋙ F) G ≫ G.map (colim.map α) = colim.map (whiskerRight α G) ≫ colimit.post F G.
LaTeX
$$$\operatorname{colimit.post} (E \!\!\!\!\!\! F) G \\; \; ≫ G.map (\operatorname{colim.map} \alpha) = \operatorname{colim.map} (\text{whiskerRight } \alpha G) \\; ≫ \operatorname{colimit.post} F G$$$
Lean4
theorem pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D) [HasColimit F] [HasColimit (E ⋙ F)]
[HasColimit (F ⋙ G)] [h : HasColimit ((E ⋙ F) ⋙ G)] :
-- G (colimit F) ⟶ G (colimit (E ⋙ F)) ⟶ colimit ((E ⋙ F) ⋙ G) vs
-- G (colimit F) ⟶ colimit F ⋙ G ⟶ colimit (E ⋙ (F ⋙ G)) or
haveI : HasColimit (E ⋙ F ⋙ G) := h
colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G :=
by
ext j
rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]
haveI : HasColimit (E ⋙ F ⋙ G) := h
erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]
