English
For a limit F with W in C and a morphism f: ULift(W ⟶ lim F), the hom component of the limit isomorphism evaluated at f equals the composition of the constant functor map on f down with the projection π of the limit cone: limit.homIso F W).hom f = (const J).map f.down ≫ (limit.cone F).π.
Русский
Для предела F с объектом W в C и морфизма f: ULift(W ⟶ lim F), гом-компонент изоморфизма лимита применяется к f как композиция константного отображения и проекции конуса предела.
LaTeX
$$$(\\operatorname{limit.homIso} F W).\\hom f = (\\operatorname{const} J).map f.down \\\\gg (\\operatorname{limit.cone} F).\\pi$$$
Lean4
@[simp]
theorem homIso_hom (F : J ⥤ C) [HasLimit F] {W : C} (f : ULift (W ⟶ limit F)) :
(limit.homIso F W).hom f = (const J).map f.down ≫ (limit.cone F).π :=
(limit.isLimit F).homIso_hom f
