colimit_map_colimitObjIsoColimitCompEvaluation_hom

English

The inverse of the colimitObjIsoColimitCompEvaluation interacts with colimit maps compatibly with whiskering.

Русский

Обратная сторона интеракции colimitObjIsoColimitCompEvaluation совместима с отображениями колимита через whiskerLeft.

LaTeX

$$$(\mathrm{colimitObjIsoColimitCompEvaluation}\, F\, i)^{-1} \circ (\mathrm{colimit} F).map f = \mathrm{colimMap}(\mathrm{whiskerLeft}(\_ , ((\mathrm{evaluation} \! \_).map f))) \circ (\mathrm{colimitObjIsoColimitCompEvaluation}\, F\, j)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem colimit_map_colimitObjIsoColimitCompEvaluation_hom [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C) {i j : K}
    (f : i ⟶ j) :
    (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation _ _).hom =
      (colimitObjIsoColimitCompEvaluation _ _).hom ≫ colimMap (whiskerLeft _ ((evaluation _ _).map f)) :=
  by rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv, colimitObjIsoColimitCompEvaluation_inv_colimit_map]

Похожие утверждения