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.

@[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
@[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