mathlib documentation

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.

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

Instances
source
@[protected, instance]
def category_theory.limits.preserves_limits.preserves_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits F] :
category_theory.limits.preserves_finite_limits F
Equations
source
@[protected, instance]
def category_theory.limits.id_preserves_finite_limits {C : Type u₁} [category_theory.category C] :
category_theory.limits.preserves_finite_limits (𝟭 C)
Equations
source
def category_theory.limits.comp_preserves_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_finite_limits F] [category_theory.limits.preserves_finite_limits G] :
category_theory.limits.preserves_finite_limits (F ⋙ G)

The composition of two left exact functors is left exact.

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

The composition of two right exact functors is right exact.

Equations