limitObjIsoLimitCompEvaluation_hom_π

English

There is a canonical isomorphism between the limit of F and the limit obtained by evaluating at k; the hom component composes with projections to give the expected projection.

Русский

Существует каноническое изоморфизм между пределом F и пределом после вычисления в k; гомоморфизм компонуется с проекциями, чтобы дать ожидаемую проекцию.

LaTeX

$$$(\mathrm{limitObjIsoLimitCompEvaluation}\, F\, k).\mathrm{hom} \circ \mathrm{limit}.\pi(F)\!_j = \mathrm{limit}.\pi(F)\!_j \!\cdot \mathrm{app}_k$$$

Lean4

@[reassoc (attr := simp)]
theorem limitObjIsoLimitCompEvaluation_hom_π [HasLimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J) (k : K) :
    (limitObjIsoLimitCompEvaluation F k).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j = (limit.π F j).app k :=
  by
  dsimp [limitObjIsoLimitCompEvaluation]
  simp

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