English
Under suitable hypotheses, one can construct a limit cone for liftToFinsetObj F; this is done by defining a cone with apex the limit of liftToFinsetObj F and showing it is universal.
Русский
При допустимых гипотезах можно построить предел конуса для liftToFinsetObj F; вершина и его универсальность доказываются через лимит liftToFinsetObj F.
LaTeX
$$$$ \mathrm{liftToFinsetLimitCone}(F) \text{ is a limit cone for } \mathrm{liftToFinsetObj}(F). $$$$
Lean4
/-- The cone `finiteSubproductsCone` is a limit cone. -/
def isLimitFiniteSubproductsCone (f : α → C) [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] [HasProduct f] :
IsLimit (finiteSubproductsCone f) :=
IsLimit.ofIsoLimit (limit.isLimit _)
(Cones.ext (IsLimit.conePointUniqueUpToIso (liftToFinsetLimitCone (Discrete.functor f)).isLimit (limit.isLimit _) :)
(by
intro S
simp only [limit.cone_x, Functor.const_obj_obj, liftToFinsetObj_obj, Discrete.functor_obj_eq_as, limit.cone_π,
finiteSubproductsCone_pt, finiteSubproductsCone_π_app]
ext j
simp only [Discrete.functor_obj_eq_as, Category.assoc, limit.lift_π, Fan.mk_pt, Fan.mk_π_app,
limit.conePointUniqueUpToIso_hom_comp, liftToFinsetLimitCone_cone_pt, Discrete.mk_as,
liftToFinsetLimitCone_cone_π_app]
simp [← limit.w (liftToFinsetObj _) (Quiver.Hom.op (homOfLE (x := { j.1 }) (y := S.unop) (by simp)))]))
