English
The constructed limit cone is indeed a limit cone for the diagram F.
Русский
Сконструированный предел действительно является пределом для диаграммы F.
LaTeX
$$$\text{limitConeIsLimit } F : \operatorname{IsLimit}(\text{limitCone } F)$$$
Lean4
/-- Witness that the limit cone in `ModuleCat R` is a limit cone.
(Internal use only; use the limits API.)
-/
def limitConeIsLimit : IsLimit (limitCone.{t, v, w} F) :=
by
refine
IsLimit.ofFaithful (forget (ModuleCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
(fun s => ofHom ⟨⟨(Types.Small.limitConeIsLimit.{v, w} _).lift ((forget (ModuleCat R)).mapCone s), ?_⟩, ?_⟩)
(fun s => rfl)
· intro x y
simp only [Types.Small.limitConeIsLimit_lift, Functor.mapCone_π_app, forget_map, map_add]
rw [← equivShrink_add]
rfl
· intro r x
simp only [Types.Small.limitConeIsLimit_lift, Functor.mapCone_π_app, forget_map, map_smul]
rw [← equivShrink_smul]
rfl
