limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π

English

A relation equates the composition of limit components with a whiskered projection under a limit compatibility iso.

Русский

Соотношение приравнивает композицию компонент предела к отбивке whiskerLeft под изоморфизм совместимости пределов.

LaTeX

$$$(\mathrm{limitCompWhiskeringLeftIsoCompLimit}\, F\, G)^{\mathrm{hom}} \circ \mathrm{whiskerLeft}\ G (\mathrm{limit}.π F j) = \mathrm{limit}.π (F \circ (\mathrm{whiskeringLeft}\ D K C).obj G) j$$

Lean4

@[reassoc (attr := simp)]
theorem limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π (F : J ⥤ K ⥤ C) (G : D ⥤ K) [HasLimitsOfShape J C]
    (j : J) :
    (limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ whiskerLeft G (limit.π F j) =
      limit.π (F ⋙ (whiskeringLeft _ _ _).obj G) j :=
  by
  ext d
  simp [limitCompWhiskeringLeftIsoCompLimit]

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