English
A functor reflecting larger colimits also reflects smaller colimits. More precisely, if F reflects colimits of size (w', w2') in some universe, then F reflects colimits of size (w, w2) in a smaller or equal universe, given appropriate universe relations.
Русский
Функтор, отражающий более крупные колимиты, также отражает меньшие колимиты. Буквально: если F отражает колимиты размера (w', w2') в одной вселенной, то он отражает колимиты размера (w, w2) в более мелкой (или равной) вселенной при соблюдении соответствующих условий.
LaTeX
$$$\\forall C,D\\,w,w',w2,w2'\\; (UnivLE:\\; w,w')\\; (UnivLE:\\; w2,w2')\\; (F:\\, C\\to D)\\; [ReflectsColimitsOfSize^{w',w2'}F]\\; \\Rightarrow\\; ReflectsColimitsOfSize^{w,w2}F . $$$
Lean4
/-- A functor reflecting larger colimits also reflects smaller colimits. -/
theorem reflectsColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
[ReflectsColimitsOfSize.{w', w₂'} F] : ReflectsColimitsOfSize.{w, w₂} F where
reflectsColimitsOfShape
{J} := reflectsColimitsOfShape_of_equiv ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F
