English
If a category C has cofiltered limits of large size and satisfies AB5Star for those sizes, then C has cofiltered limits of smaller sizes and AB5Star for those smaller sizes.
Русский
Если у категории C существуют кофильтрованные пределы крупного размера и выполняется AB5Star для этих размеров, то C имеет кофильтрованные пределы меньшего размера и AB5Star для этих меньших размеров.
LaTeX
$$$\\operatorname{HasCofilteredLimitsOfSize}^{(w,w')}(C) \\land \\operatorname{AB5StarOfSize}^{(w,w')}(C) \\Leftarrow \\operatorname{HasCofilteredLimitsOfSize}^{(\\max w w',\\max w' w_2')}(C) \\land \\operatorname{AB5StarOfSize}^{(\\max w w',\\max w' w_2')}(C)$$$
Lean4
theorem AB5StarOfSize_of_univLE [HasCofilteredLimitsOfSize.{w₂, w₂'} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}]
[AB5StarOfSize.{w₂, w₂'} C] :
haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}
AB5StarOfSize.{w, w'} C :=
by
haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}
constructor
intro J _ _
haveI :=
IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <| Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))
exact
HasExactLimitsOfShape.of_domain_equivalence _
((ShrinkHoms.equivalence.{w₂} J).trans <| Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm
