English
If a category has cofiltered limits of a given size and AB5Star, then AB4Star holds for discrete finite cases.
Русский
Если у категории есть кофилтрованные пределы заданного размера и AB5Star, то AB4Star справедлив для дискретных конечных случаев.
LaTeX
$$$\\operatorname{HasCofilteredLimitsOfSize}^{(w,w')} C \\land \\operatorname{AB5StarOfSize}^{(w,w')} C \\Rightarrow \\operatorname{AB4StarOfSize}^{(w,w')} C$$$
Lean4
/-- `HasExactLimitsOfShape (Finset (Discrete J))ᵒᵖ C` implies `HasExactLimitsOfShape (Discrete J) C`
-/
theorem hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op [HasLimitsOfShape (Discrete J) C]
[HasLimitsOfShape (Finset (Discrete J))ᵒᵖ C] [HasExactLimitsOfShape (Finset (Discrete J))ᵒᵖ C] :
HasExactLimitsOfShape (Discrete J) C where
preservesFiniteColimits :=
letI : PreservesFiniteColimits (ProductsFromFiniteCofiltered.liftToFinset C J ⋙ lim) :=
comp_preservesFiniteColimits _ _
preservesFiniteColimits_of_natIso (ProductsFromFiniteCofiltered.liftToFinsetLimIso _ _)
