mathlib3 documentation

category_theory.limits.preserves.finite

Preservation of finite (co)limits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[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 1 u₁ u₂ v₁ v₂)

A functor is said to preserve finite limits, if it preserves all limits of shape J, where J : Type 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
@[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 1 u₁ u₂ v₁ v₂)

A functor is said to preserve finite colimits, if it preserves all colimits of shape J, where J : Type 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