English
For D : I ⥤ Cᵒᵖ and F : Cᵒᵖ ⥤ Type, and α : F ⟶ G, a post-composition compatibility with H holds: colimit.post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ colimit.post G H.
Русский
Для D : I ⥤ Cᵒᵖ и F : Cᵒᵖ ⥤ Type, и α : F ⟶ G, выполняется совместимость после композиции: colimit.post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ colimit.post G H.
LaTeX
$$$\\text{colimit.post } F H \\,\\;\\;\\; H.map(\\text{colim.map } \\alpha) = \\text{colim.map}(\\text{whiskerRight } \\alpha H) \\;\\;\\; \\text{colimit.post } G H$$$
Lean4
theorem map_post {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D] (H : C ⥤ D) :
/- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
colimit.post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ colimit.post G H :=
by
ext
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]
rfl
