English
The construction liftToFinset preserves finite limits: combining finite coproducts and finite limits in stages yields a functor liftToFinset that preserves finite limits.
Русский
Конструкция liftToFinset сохраняет конечные пределы: сочетание конечных бинпродуктов и конечных пределов ступенчато образует фунctor liftToFinset, сохраняющий конечные пределы.
LaTeX
$$$\\operatorname{PreservesFiniteLimits}(\\operatorname{liftToFinset} C \\alpha).$$$
Lean4
instance preservesFiniteLimits_liftToFinset : PreservesFiniteLimits (liftToFinset C α) :=
preservesFiniteLimits_of_evaluation _ fun I =>
letI : PreservesFiniteLimits (colim (J := Discrete I) (C := C)) :=
preservesFiniteLimits_of_natIso HasBiproductsOfShape.colimIsoLim.symm
letI : PreservesFiniteLimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj (Discrete.functor fun x ↦ ↑x)) :=
⟨fun J _ _ => whiskeringLeft_preservesLimitsOfShape J _⟩
letI :
PreservesFiniteLimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj (Discrete.functor (·.val)) ⋙ colim) :=
comp_preservesFiniteLimits _ _
preservesFiniteLimits_of_natIso (liftToFinsetEvaluationIso I).symm
