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

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

Type (max 1 u₁ u₂ v₁ v₂)

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

@[protected, instance]

noncomputable def category_theory.limits.preserves_limits_of_shape_of_preserves_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] (J : Type w) [category_theory.small_category J] [category_theory.fin_category J] :

category_theory.limits.preserves_limits_of_shape J F

Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.

Equations

category_theory.limits.preserves_limits_of_shape_of_preserves_finite_limits F J = category_theory.limits.preserves_limits_of_shape_of_equiv (category_theory.fin_category.equiv_as_type J) F

noncomputable def category_theory.limits.preserves_limits_of_size.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_of_size F] :

category_theory.limits.preserves_finite_limits F

If we preserve limits of some arbitrary size, then we preserve all finite limits.

Equations

category_theory.limits.preserves_limits_of_size.preserves_finite_limits F = {preserves_finite_limits := λ (J : Type) (sJ : category_theory.small_category J) (fJ : category_theory.fin_category J), category_theory.limits.preserves_limits_of_shape_of_equiv (category_theory.fin_category.equiv_as_type J) F}

@[protected, instance]

noncomputable def category_theory.limits.preserves_limits_of_size.zero.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_of_size F] :

category_theory.limits.preserves_finite_limits F

Equations

category_theory.limits.preserves_limits_of_size.zero.preserves_finite_limits F = category_theory.limits.preserves_limits_of_size.preserves_finite_limits F

@[protected, instance]

noncomputable 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 = category_theory.limits.preserves_limits_of_size.preserves_finite_limits F

def category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (h : Π (J : Type w) {𝒥 : category_theory.small_category J}, category_theory.fin_category J → category_theory.limits.preserves_limits_of_shape J F) :

category_theory.limits.preserves_finite_limits F

We can always derive preserves_finite_limits C by showing that we are preserving limits at an arbitrary universe.

Equations

category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size F h = {preserves_finite_limits := λ (J : Type) (hJ : category_theory.small_category J) (hhJ : category_theory.fin_category J), let _inst : category_theory.category (category_theory.ulift_hom (ulift J)) := category_theory.ulift_hom.category in category_theory.limits.preserves_limits_of_shape_of_equiv (category_theory.ulift_hom_ulift_category.equiv J).symm F}

@[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) [_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}

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) (_x_1 : category_theory.small_category _x) (_x_2 : category_theory.fin_category _x), category_theory.limits.comp_preserves_limits_of_shape F G}

@[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₂)

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

@[protected, instance]

noncomputable def category_theory.limits.preserves_colimits_of_shape_of_preserves_finite_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_colimits F] (J : Type w) [category_theory.small_category J] [category_theory.fin_category J] :

category_theory.limits.preserves_colimits_of_shape J F

Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.

Equations

category_theory.limits.preserves_colimits_of_shape_of_preserves_finite_colimits F J = category_theory.limits.preserves_colimits_of_shape_of_equiv (category_theory.fin_category.equiv_as_type J) F

noncomputable def category_theory.limits.preserves_colimits_of_size.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_of_size F] :

category_theory.limits.preserves_finite_colimits F

If we preserve colimits of some arbitrary size, then we preserve all finite colimits.

Equations

category_theory.limits.preserves_colimits_of_size.preserves_finite_colimits F = {preserves_finite_colimits := λ (J : Type) (sJ : category_theory.small_category J) (fJ : category_theory.fin_category J), category_theory.limits.preserves_colimits_of_shape_of_equiv (category_theory.fin_category.equiv_as_type J) F}

@[protected, instance]

noncomputable def category_theory.limits.preserves_colimits_of_size.zero.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_of_size F] :

category_theory.limits.preserves_finite_colimits F

Equations

category_theory.limits.preserves_colimits_of_size.zero.preserves_finite_colimits F = category_theory.limits.preserves_colimits_of_size.preserves_finite_colimits F

@[protected, instance]

noncomputable 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 = category_theory.limits.preserves_colimits_of_size.preserves_finite_colimits F

def category_theory.limits.preserves_finite_colimits_of_preserves_finite_colimits_of_size {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (h : Π (J : Type w) {𝒥 : category_theory.small_category J}, category_theory.fin_category J → category_theory.limits.preserves_colimits_of_shape J F) :

category_theory.limits.preserves_finite_colimits F

We can always derive preserves_finite_limits C by showing that we are preserving limits at an arbitrary universe.

Equations

category_theory.limits.preserves_finite_colimits_of_preserves_finite_colimits_of_size F h = {preserves_finite_colimits := λ (J : Type) (hJ : category_theory.small_category J) (hhJ : category_theory.fin_category J), let _inst : category_theory.category (category_theory.ulift_hom (ulift J)) := category_theory.ulift_hom.category in category_theory.limits.preserves_colimits_of_shape_of_equiv (category_theory.ulift_hom_ulift_category.equiv J).symm F}

@[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) [_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}

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) (_x_1 : category_theory.small_category _x) (_x_2 : category_theory.fin_category _x), category_theory.limits.comp_preserves_colimits_of_shape F G}