isFinitelyAccessible_iff_preservesFilteredColimits

English

Again, IsFinitelyAccessible F is equivalent to preserving filtered colimits of a given size.

Русский

Повторно: IsFinitelyAccessible F эквивалентно сохранению фильтрованных колимитов заданного размера.

LaTeX

$$$IsFinitelyAccessible^{w} F \iff PreservesFilteredColimitsOfSize^{w,w} F$$$

Lean4

theorem isFinitelyAccessible_iff_preservesFilteredColimits {F : C ⥤ D} :
    IsFinitelyAccessible.{v'} F ↔ PreservesFilteredColimits F :=
  IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

Похожие утверждения