Preservation of filtered colimits and cofiltered limits.

Typically forgetful functors from algebraic categories preserve filtered colimits (although not general colimits). See e.g. Mathlib/Algebra/Category/MonCat/FilteredColimits.lean.

Note also that using the results in the file Mathlib/CategoryTheory/Presentable/Directed.lean, in order to show that a functor preserves filtered colimits, it would be sufficient to check that it preserves colimits indexed by nonempty directed types.

class CategoryTheory.Limits.PreservesFilteredColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

PreservesFilteredColimitsOfSize.{w', w} F means that F sends all colimit cocones over any filtered diagram J ⥤ C to colimit cocones, where J : Type w with [Category.{w'} J].

• preserves_filtered_colimits (J : Type w) [Category.{w', w} J] [IsFiltered J] : PreservesColimitsOfShape J F

@[reducible, inline]

abbrev CategoryTheory.Limits.PreservesFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor is said to preserve filtered colimits, if it preserves all colimits of shape J, where J is a filtered category which is small relative to the universe in which morphisms of the source live.

Equations

• CategoryTheory.Limits.PreservesFilteredColimits F = CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{?u.28, ?u.28, ?u.29, ?u.28, ?u.27, ?u.26} F

@[instance 100]

instance CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

instance CategoryTheory.Limits.comp_preservesFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [PreservesFilteredColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : PreservesFilteredColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)

theorem CategoryTheory.Limits.preservesFilteredColimitsOfSize_of_univLE {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F] : PreservesFilteredColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F

A functor preserving larger filtered colimits also preserves smaller filtered colimits.

theorem CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

PreservesFilteredColimitsOfSize_shrink.{w, w'} F tries to obtain PreservesFilteredColimitsOfSize.{w, w'} F from some other PreservesFilteredColimitsOfSize F.

theorem CategoryTheory.Limits.preservesSmallestFilteredColimits_of_preservesFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : PreservesFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Preserving filtered colimits at any universe implies preserving filtered colimits at universe 0.

class CategoryTheory.Limits.ReflectsFilteredColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

ReflectsFilteredColimitsOfSize.{w', w} F means that whenever the image of a filtered cocone under F is a colimit cocone, the original cocone was already a colimit.

• reflects_filtered_colimits (J : Type w) [Category.{w', w} J] [IsFiltered J] : ReflectsColimitsOfShape J F

@[reducible, inline]

abbrev CategoryTheory.Limits.ReflectsFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor is said to reflect filtered colimits, if it reflects all colimits of shape J, where J is a filtered category which is small relative to the universe in which morphisms of the source live.

Equations

• CategoryTheory.Limits.ReflectsFilteredColimits F = CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{?u.28, ?u.28, ?u.29, ?u.28, ?u.27, ?u.26} F

@[instance 100]

instance CategoryTheory.Limits.ReflectsColimits.reflectsFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

instance CategoryTheory.Limits.comp_reflectsFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [ReflectsFilteredColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : ReflectsFilteredColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)

theorem CategoryTheory.Limits.reflectsFilteredColimitsOfSize_of_univLE {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [ReflectsFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F] : ReflectsFilteredColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F

A functor reflecting larger filtered colimits also reflects smaller filtered colimits.

theorem CategoryTheory.Limits.reflectsFilteredColimitsOfSize_shrink {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

ReflectsFilteredColimitsOfSize_shrink.{w, w'} F tries to obtain ReflectsFilteredColimitsOfSize.{w, w'} F from some other ReflectsFilteredColimitsOfSize F.

theorem CategoryTheory.Limits.reflectsSmallestFilteredColimits_of_reflectsFilteredColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : ReflectsFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Reflecting filtered colimits at any universe implies reflecting filtered colimits at universe 0.

class CategoryTheory.Limits.PreservesCofilteredLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

PreservesCofilteredLimitsOfSize.{w', w} F means that F sends all limit cones over any cofiltered diagram J ⥤ C to limit cones, where J : Type w with [Category.{w'} J].

• preserves_cofiltered_limits (J : Type w) [Category.{w', w} J] [IsCofiltered J] : PreservesLimitsOfShape J F

@[reducible, inline]

abbrev CategoryTheory.Limits.PreservesCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor is said to preserve cofiltered limits, if it preserves all limits of shape J, where J is a cofiltered category which is small relative to the universe in which morphisms of the source live.

Equations

• CategoryTheory.Limits.PreservesCofilteredLimits F = CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{?u.28, ?u.28, ?u.29, ?u.28, ?u.27, ?u.26} F

@[instance 100]

instance CategoryTheory.Limits.PreservesLimits.preservesCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

instance CategoryTheory.Limits.comp_preservesCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [PreservesCofilteredLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : PreservesCofilteredLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)

theorem CategoryTheory.Limits.preservesCofilteredLimitsOfSize_of_univLE {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [PreservesCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F] : PreservesCofilteredLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F

A functor preserving larger cofiltered limits also preserves smaller cofiltered limits.

theorem CategoryTheory.Limits.preservesCofilteredLimitsOfSize_shrink {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesCofilteredLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

PreservesCofilteredLimitsOfSizeShrink.{w, w'} F tries to obtain PreservesCofilteredLimitsOfSize.{w, w'} F from some other PreservesCofilteredLimitsOfSize F.

theorem CategoryTheory.Limits.preservesSmallestCofilteredLimits_of_preservesCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : PreservesCofilteredLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Preserving cofiltered limits at any universe implies preserving cofiltered limits at universe 0.

class CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

ReflectsCofilteredLimitsOfSize.{w', w} F means that whenever the image of a cofiltered cone under F is a limit cone, the original cone was already a limit.

• reflects_cofiltered_limits (J : Type w) [Category.{w', w} J] [IsCofiltered J] : ReflectsLimitsOfShape J F

@[reducible, inline]

abbrev CategoryTheory.Limits.ReflectsCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor is said to reflect cofiltered limits, if it reflects all limits of shape J, where J is a cofiltered category which is small relative to the universe in which morphisms of the source live.

Equations

• CategoryTheory.Limits.ReflectsCofilteredLimits F = CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{?u.28, ?u.28, ?u.29, ?u.28, ?u.27, ?u.26} F

@[instance 100]

instance CategoryTheory.Limits.ReflectsLimits.reflectsCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

instance CategoryTheory.Limits.comp_reflectsCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [ReflectsCofilteredLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)

theorem CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_of_univLE {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}] [ReflectsCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F] : ReflectsCofilteredLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F

A functor reflecting larger cofiltered limits also reflects smaller cofiltered limits.

theorem CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_shrink {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsCofilteredLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

ReflectsCofilteredLimitsOfSize_shrink.{w, w'} F tries to obtain ReflectsCofilteredLimitsOfSize.{w, w'} F from some other ReflectsCofilteredLimitsOfSize F.

theorem CategoryTheory.Limits.reflectsSmallestCofilteredLimits_of_reflectsCofilteredLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : ReflectsCofilteredLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Reflecting cofiltered limits at any universe implies reflecting cofiltered limits at universe 0.