limit_map_limitObjIsoLimitCompEvaluation_hom

English

For a morphism f: i ⟶ j in K, the limit map interacts compatibly with the limit-object iso and the whiskered map.

Русский

Для морфизма f: i ⟶ j в K пределы совместимы с изоморфизмом limitObj и отбивкой whiskerLeft.

LaTeX

$$$(\lim F)\!\mathrm{map} f \;\circ\; (\limObjIsoLimitCompEvaluation\, F\, j)^{\mathrm{hom}} = (\limObjIsoLimitCompEvaluation\, F\, i)^{\mathrm{hom}} \circ \mathrm{limMap}(F, f)$$$

Lean4

@[reassoc (attr := simp)]
theorem limit_map_limitObjIsoLimitCompEvaluation_hom [HasLimitsOfShape J C] {i j : K} (F : J ⥤ K ⥤ C) (f : i ⟶ j) :
    (limit F).map f ≫ (limitObjIsoLimitCompEvaluation _ _).hom =
      (limitObjIsoLimitCompEvaluation _ _).hom ≫ limMap (whiskerLeft _ ((evaluation _ _).map f)) :=
  by
  ext
  simp

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