ι_colimitCompWhiskeringLeftIsoCompColimit_hom

English

A dual form of the previous relation expresses compatibility of injections with whiskering and the limit analysis.

Русский

Двойственная форма предыдущего отношения выражает совместимость инъекций с whiskering и пределами.

LaTeX

$$$\mathrm{ι_colimitCompWhiskeringLeftIsoCompColimit\_hom}\ (F,G,j) = \text{equation}$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitCompWhiskeringLeftIsoCompColimit_hom (F : J ⥤ K ⥤ C) (G : D ⥤ K) [HasColimitsOfShape J C] (j : J) :
    colimit.ι (F ⋙ (whiskeringLeft _ _ _).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom =
      whiskerLeft G (colimit.ι F j) :=
  by
  ext d
  simp [colimitCompWhiskeringLeftIsoCompColimit]

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