Preservation of filtered colimits and cofiltered limits.

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

Future work

This could be generalised to allow diagrams in lower universes.

class CategoryTheory.Limits.PreservesFilteredColimits {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : CategoryTheory.Functor C D) : Type (max u₁ u₂ (v + 1))

A functor is said to preserve filtered colimits, if it preserves all colimits of shape J, where J is a filtered category.

• preserves_filtered_colimits : (J : Type v) → [inst : CategoryTheory.SmallCategory J] → [inst_1 : CategoryTheory.IsFiltered J] → CategoryTheory.Limits.PreservesColimitsOfShape J F

@[instance 100]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

class CategoryTheory.Limits.PreservesCofilteredLimits {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : CategoryTheory.Functor C D) : Type (max u₁ u₂ (v + 1))

A functor is said to preserve cofiltered limits, if it preserves all limits of shape J, where J is a cofiltered category.

• preserves_cofiltered_limits : (J : Type v) → [inst : CategoryTheory.SmallCategory J] → [inst_1 : CategoryTheory.IsCofiltered J] → CategoryTheory.Limits.PreservesLimitsOfShape J F

@[instance 100]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.