mathlib documentation


Preservation of finite (co)limits. #

These functors are also known as left exact (flat) or right exact functors when the categories involved are abelian, or more generally, finitely (co)complete.

structure category_theory.limits.preserves_finite_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 finite colimits, if it preserves all colimits of shape J, where J is a finite category.

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