limitObjIsoLimitCompEvaluation_inv_limit_map

English

The inverse limit-object iso interacts with limMap to yield a natural equality for f: i ⟶ j.

Русский

Обратный предел–изоморфизм взаимодействует с limMap и дает естественное равенство для f: i ⟶ j.

LaTeX

$$$(\mathrm{limitObjIsoLimitCompEvaluation}\, F\, i)^{-1} \circ (\mathrm{limit}.map F)\!_j = \mathrm{limMap}(\mathrm{whiskerLeft}(F, (\mathrm{ev}_f))) \circ (\mathrm{limitObjIsoLimitCompEvaluation}\, F\, j)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem limitObjIsoLimitCompEvaluation_inv_limit_map [HasLimitsOfShape J C] {i j : K} (F : J ⥤ K ⥤ C) (f : i ⟶ j) :
    (limitObjIsoLimitCompEvaluation _ _).inv ≫ (limit F).map f =
      limMap (whiskerLeft _ ((evaluation _ _).map f)) ≫ (limitObjIsoLimitCompEvaluation _ _).inv :=
  by rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, limit_map_limitObjIsoLimitCompEvaluation_hom]

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