# mathlibdocumentation

category_theory.limits.preserves.finite

# 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.

• category_theory.limits.preserves_finite_limits_of_preserves_equalizers_and_finite_products : see category_theory/limits/constructions/limits_of_products_and_equalizers.lean. Also provides the dual version.
• category_theory.limits.preserves_finite_limits_iff_flat : see category_theory/flat_functors.lean.
@[class]
structure category_theory.limits.preserves_finite_limits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ (v+1))
• preserves_finite_limits : (Π (J : Type ?) [_inst_5 : [_inst_6 : , . "apply_instance"

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

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_finite_limits
• category_theory.limits.preserves_finite_limits.has_sizeof_inst
@[protected, instance]
def category_theory.limits.preserves_limits.preserves_finite_limits {C : Type u₁} {D : Type u₂} (F : C D)  :
Equations
@[protected, instance]
Equations
def category_theory.limits.comp_preserves_finite_limits {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E)  :

The composition of two left exact functors is left exact.

Equations
@[class]
structure category_theory.limits.preserves_finite_colimits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ (v+1))
• preserves_finite_colimits : (Π (J : Type ?) [_inst_5 : [_inst_6 : , . "apply_instance"

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
@[protected, instance]
def category_theory.limits.preserves_colimits.preserves_finite_colimits {C : Type u₁} {D : Type u₂} (F : C D)  :
Equations
@[protected, instance]
Equations
def category_theory.limits.comp_preserves_finite_colimits {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E)  :

The composition of two right exact functors is right exact.

Equations