colimitObjIsoColimitCompEvaluation_inv_colimit_map

English

The map induced by F maps commutes with the colimitObjIsoColimitCompEvaluation hom up to a limMap twist.

Русский

Отображение, индуцированное F, commute с гомоморфизмом limitObjIsoColimitCompEvaluation до twists limMap.

LaTeX

$$$(\mathrm{colimit} F) \!\text{map} f \circ (\mathrm{colimitObjIsoColimitCompEvaluation}\, F\, j)^{\mathrm{hom}} = (\mathrm{colimitObjIsoColimitCompEvaluation}\, F\, i)^{\mathrm{hom}} \circ \mathrm{limMap}(\mathrm{whiskerLeft}(F, (\mathrm{evaluation} \! k).map f))$$$

Lean4

@[reassoc (attr := simp)]
theorem colimitObjIsoColimitCompEvaluation_inv_colimit_map [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C) {i j : K}
    (f : i ⟶ j) :
    (colimitObjIsoColimitCompEvaluation _ _).inv ≫ (colimit F).map f =
      colimMap (whiskerLeft _ ((evaluation _ _).map f)) ≫ (colimitObjIsoColimitCompEvaluation _ _).inv :=
  by
  ext
  simp

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