limitObjIsoLimitCompEvaluation_inv_π_app

English

The inverse of the limit-object–limit-comp evaluation is described by a map from the j-projection to the F ⋙ ev_k projection.

Русский

Обратный предел–оценивание описывается отображением из j-проекции к проекции F ⋙ ev_k.

LaTeX

$$$(\mathrm{limitObjIsoLimitCompEvaluation}\, F\, k)^{-1} \circ (\mathrm{limit}.\pi F\!_j) = \mathrm{limit}.\pi(F \!\circ (\mathrm{ev}_k))_j$$$

Lean4

@[reassoc (attr := simp)]
theorem limitObjIsoLimitCompEvaluation_inv_π_app [HasLimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J) (k : K) :
    (limitObjIsoLimitCompEvaluation F k).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j :=
  by
  dsimp [limitObjIsoLimitCompEvaluation]
  rw [Iso.inv_comp_eq]
  simp

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