mathlib documentation

category_theory.limits.preserves.filtered

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/Mon/filtered_colimits.

Future work #

This could be generalised to allow diagrams in lower universes.

@[class]
structure category_theory.limits.preserves_filtered_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : 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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_filtered_colimits
  • category_theory.limits.preserves_filtered_colimits.has_sizeof_inst
@[class]
structure category_theory.limits.preserves_cofiltered_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : 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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_cofiltered_limits
  • category_theory.limits.preserves_cofiltered_limits.has_sizeof_inst