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 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
- category_theory.limits.preserves_limits.preserves_finite_limits
- category_theory.limits.id_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]
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] :
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}
@[protected, instance]
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}
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 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}
@[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
@[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] :
Equations
@[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 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}