English
In a category with filtered colimits of certain sizes, and universe bounds, the AB5 property ascends along universe bounds; i.e., AB5OfSize transfers to bigger size parameters under suitable universes.
Русский
В категории с фильтрованными колимитами заданного размера и с ограничениями по вселенным, свойство AB5 создано для больших размерностей; свойство AB5OfSize переносится при переходе к более крупным размерам при надлежащих условиях.
LaTeX
$$$\forall C,\ HasFilteredColimitsOfSize{w_2,w_2'} C,\ UnivLE{w,w_2},\ UnivLE{w',w_2'} ,\ AB5OfSize{w_2,w_2'} C \Rightarrow \ AB5OfSize{w,w'} C.$$$
Lean4
theorem AB5OfSize_of_univLE [HasFilteredColimitsOfSize.{w₂, w₂'} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}]
[AB5OfSize.{w₂, w₂'} C] :
haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}
AB5OfSize.{w, w'} C :=
by
haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}
constructor
intro J _ _
haveI :=
IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <| Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))
exact
HasExactColimitsOfShape.of_domain_equivalence _
((ShrinkHoms.equivalence.{w₂} J).trans <| Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm
