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.
Related results #
category_theory.limits.preserves_finite_limits_of_preserves_equalizers_and_finite_products: seecategory_theory/limits/constructions/limits_of_products_and_equalizers.lean. Also provides the dual version.category_theory.limits.preserves_finite_limits_iff_flat: seecategory_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
- category_theory.limits.preserves_limits.preserves_finite_limits_of_size
- category_theory.limits.preserves_limits.preserves_finite_limits
- category_theory.limits.id_preserves_finite_limits
- category_theory.LeftExactFunctor.obj.limits.preserves_finite_limits
- category_theory.ExactFunctor.obj.limits.preserves_finite_limits
- FinVect.category_theory.forget₂.category_theory.limits.preserves_finite_limits
- category_theory.limits.filtered_colim_preserves_finite_limits_of_types
- category_theory.limits.colim.preserves_finite_limits
- category_theory.Lan_preserves_finite_limits_of_flat
- category_theory.Lan_preserves_finite_limits_of_preserves_finite_limits
- category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_finite_limits
- category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_finite_limits
- category_theory.presheaf_to_Sheaf.limits.preserves_finite_limits
- category_theory.sites.pushforward.limits.preserves_finite_limits
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] :
Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.
@[protected, instance]
noncomputable
def
category_theory.limits.preserves_limits.preserves_finite_limits_of_size
{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] :
Equations
- category_theory.limits.preserves_limits.preserves_finite_limits_of_size 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.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] :
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) :
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]
Equations
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] :
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] :
Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.
@[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_of_size F] :
Equations
- category_theory.limits.preserves_colimits.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}
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) :
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] :
Equations
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] :
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}