English
For K : J ⥤ C and F : C ⥤ D with CreatesLimit K F, and for a cone c on K ⋙ F that is IsLimit, the lifted limit maps to original commute with the π maps: (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j for all j.
Русский
Для K : J ⥤ C и F : C ⥤ D с CreatesLimit K F, и для конуса c на K ⋙ F, являющегося IsLimit, отображения поднятого предела к оригиналу удовлетворяют сопоставимости: (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j для всех j.
LaTeX
$$$$ (liftedLimitMapsToOriginal(t)).inv.hom \;\circ\; F.map((liftLimit(t)).\pi.app j) = c.\pi.app j \quad\text{for all } j. $$$$
Lean4
theorem liftedLimitMapsToOriginal_inv_map_π {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)}
(t : IsLimit c) (j : J) : (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j :=
by
rw [show F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j from (by simp), ←
Category.assoc, ← Cone.category_comp_hom]
simp
