whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv

English

Whiskering with a colimit injection commutes with the colimit-iso on the left.

Русский

Отбивка слева через whiskerLeft совместима с инъекцией колимита и изоморфизмами слева.

LaTeX

$$$\text{whiskerLeft}\ G (\mathrm{colimit}.ι F j) \; = \; (\mathrm{colimitCompWhiskeringLeftIsoCompColimit}\, F\, G)^{\!\mathrm{hom}} \circ \mathrm{colimit}.ι (F \circ j)$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv (F : J ⥤ K ⥤ C) (G : D ⥤ K) [HasColimitsOfShape J C]
    (j : J) :
    whiskerLeft G (colimit.ι F j) ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).inv =
      colimit.ι (F ⋙ (whiskeringLeft _ _ _).obj G) j :=
  by simp [Iso.comp_inv_eq]

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