English
Let K : J ⥤ C and F : C ⥤ D be such that F creates the limit of K. If c is a cone on K ⋙ F that is a limit, then for every object j in J the canonical map from the lifted limit to the original limit commutes with the functor F on the j-th projection; i.e. the j-th projection after lifting equals the image under F of the j-th projection of the lifted limit.
Русский
Пусть K : J ⥤ C и F : C ⥤ D таковы, что F создаёт предел для K. Если c — конус над K ∘ F, и он является пределом, то для каждого j ∈ J каноническое отображение между «поднятым» пределом и исходным пределом коммютирует с отображением F на j-ой проекции: j-ая проекция после подъёма равна образу F от j-ой проекции поднятого предела.
LaTeX
$$$\forall K : J \to C,\, F : C \to D\, [\text{CreatesLimit } K F] \Rightarrow \forall c : Cone (K \circ F), \ \text{IsLimit } c \Rightarrow \forall j:\, J,\n(\text{liftedLimitMapsToOriginal } t).hom.hom \circ c.\pi_{j} = F( (\mathrm{liftLimit} t).\pi_{j} ).$$$
Lean4
theorem liftedLimitMapsToOriginal_hom_π {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c)
(j : J) : (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j = F.map ((liftLimit t).π.app j) :=
by
rw [← liftedLimitMapsToOriginal_inv_map_π (t := t)]
simp only [Functor.mapCone_pt, Functor.comp_obj, ← Category.assoc, ← Cone.category_comp_hom, Iso.hom_inv_id,
Cone.category_id_hom, Category.id_comp, Functor.const_obj_obj]
