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.

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))

preserves_finite_limits : (Π (J : Type ?) [_inst_5 : category_theory.small_category J] [_inst_6 : category_theory.fin_category J], category_theory.limits.preserves_limits_of_shape J F) . "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

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

category_theory.limits.preserves_limits.preserves_finite_limits F = {preserves_finite_limits := λ (J : Type v) [_inst_5_1 : category_theory.small_category J] [_inst_6 : category_theory.fin_category J], category_theory.limits.preserves_limits_of_size.preserves_limits_of_shape}

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

category_theory.limits.id_preserves_finite_limits = {preserves_finite_limits := λ (J : Type v) [_inst_5 : category_theory.small_category J] [_inst_6 : category_theory.fin_category J], category_theory.limits.preserves_limits_of_size.preserves_limits_of_shape}

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

category_theory.limits.comp_preserves_finite_limits F G = {preserves_finite_limits := λ (_x : Type v) (_x_1 : category_theory.small_category _x) (_x_2 : category_theory.fin_category _x), category_theory.limits.comp_preserves_limits_of_shape F G}

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))

preserves_finite_colimits : (Π (J : Type ?) [_inst_5 : category_theory.small_category J] [_inst_6 : category_theory.fin_category J], category_theory.limits.preserves_colimits_of_shape J F) . "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

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

category_theory.limits.preserves_colimits.preserves_finite_colimits F = {preserves_finite_colimits := λ (J : Type v) [_inst_5_1 : category_theory.small_category J] [_inst_6 : category_theory.fin_category J], category_theory.limits.preserves_colimits_of_size.preserves_colimits_of_shape}

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

category_theory.limits.id_preserves_finite_colimits = {preserves_finite_colimits := λ (J : Type v) [_inst_5 : category_theory.small_category J] [_inst_6 : category_theory.fin_category J], category_theory.limits.preserves_colimits_of_size.preserves_colimits_of_shape}

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

category_theory.limits.comp_preserves_finite_colimits F G = {preserves_finite_colimits := λ (_x : Type v) (_x_1 : category_theory.small_category _x) (_x_2 : category_theory.fin_category _x), category_theory.limits.comp_preserves_colimits_of_shape F G}

Preservation of finite (co)limits. #

Related results #