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

• CategoryTheory.Limits.preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts : see CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean. Also provides the dual version.
• CategoryTheory.Limits.preservesFiniteLimitsIffFlat : see CategoryTheory/Functor/Flat.lean.

structure CategoryTheory.Limits.PreservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor is said to preserve finite limits, if it preserves all limits of shape J, where J : Type is a finite category.

• preservesFiniteLimits (J : Type) [SmallCategory J] [FinCategory J] : PreservesLimitsOfShape J F

theorem CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesFiniteLimits F] (J : Type w) [SmallCategory J] [FinCategory J] : PreservesLimitsOfShape J F

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

theorem CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesLimitsOfSize F] : PreservesFiniteLimits F

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

theorem CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesLimitsOfSize F] : PreservesFiniteLimits F

theorem CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesLimits F] : PreservesFiniteLimits F

theorem CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) (h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F) : PreservesFiniteLimits F

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

theorem CategoryTheory.Limits.comp_preservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteLimits F] [PreservesFiniteLimits G] : PreservesFiniteLimits (F.comp G)

The composition of two left exact functors is left exact.

theorem CategoryTheory.Limits.preservesFiniteLimits_of_natIso {C : Type u₁} [Category C] {D : Type u₂} [Category D] {F G : Functor C D} (h : Iso F G) [PreservesFiniteLimits F] : PreservesFiniteLimits G

Transfer preservation of finite limits along a natural isomorphism in the functor.

structure CategoryTheory.Limits.PreservesFiniteProducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor F preserves finite products if it preserves all from Discrete J for Finite J. We require this for J = Fin n in the definition, then generalize to J : Type u in the instance.

• preserves (n : Nat) : PreservesLimitsOfShape (Discrete (Fin n)) F

theorem CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) (J : Type u) [Finite J] [PreservesFiniteProducts F] : PreservesLimitsOfShape (Discrete J) F

theorem CategoryTheory.Limits.comp_preservesFiniteProducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteProducts F] [PreservesFiniteProducts G] : PreservesFiniteProducts (F.comp G)

theorem CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesFiniteLimits F] : PreservesFiniteProducts F

structure CategoryTheory.Limits.ReflectsFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor is said to reflect finite limits, if it reflects all limits of shape J, where J : Type is a finite category.

• reflects (J : Type) [SmallCategory J] [FinCategory J] : ReflectsLimitsOfShape J F

structure CategoryTheory.Limits.ReflectsFiniteProducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor F preserves finite products if it reflects limits of shape Discrete J for finite J. We require this for J = Fin n in the definition, then generalize to J : Type u in the instance.

• reflects (n : Nat) : ReflectsLimitsOfShape (Discrete (Fin n)) F

theorem CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsFiniteProducts F] (J : Type u) [Finite J] : ReflectsLimitsOfShape (Discrete J) F

theorem CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsLimitsOfSize F] : ReflectsFiniteLimits F

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

theorem CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimitsOfSize {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsLimitsOfSize F] : ReflectsFiniteLimits F

theorem CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsLimits F] : ReflectsFiniteLimits F

theorem CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteLimits (F.comp G)] [ReflectsFiniteLimits G] : PreservesFiniteLimits F

If F ⋙ G preserves finite limits and G reflects finite limits, then F preserves finite limits.

theorem CategoryTheory.Limits.preservesFiniteProducts_of_reflects_of_preserves {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteProducts (F.comp G)] [ReflectsFiniteProducts G] : PreservesFiniteProducts F

If F ⋙ G preserves finite products and G reflects finite products, then F preserves finite products.

theorem CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteLimits C] [PreservesFiniteLimits F] : ReflectsFiniteLimits F

theorem CategoryTheory.Limits.reflectsFiniteProducts_of_reflectsIsomorphisms {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteProducts C] [PreservesFiniteProducts F] : ReflectsFiniteProducts F

theorem CategoryTheory.Limits.comp_reflectsFiniteProducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [ReflectsFiniteProducts F] [ReflectsFiniteProducts G] : ReflectsFiniteProducts (F.comp G)

theorem CategoryTheory.Limits.instReflectsFiniteProductsOfReflectsFiniteLimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsFiniteLimits F] : ReflectsFiniteProducts F

structure CategoryTheory.Limits.PreservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor is said to preserve finite colimits, if it preserves all colimits of shape J, where J : Type is a finite category.

• preservesFiniteColimits (J : Type) [SmallCategory J] [FinCategory J] : PreservesColimitsOfShape J F

theorem CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesFiniteColimits F] (J : Type w) [SmallCategory J] [FinCategory J] : PreservesColimitsOfShape J F

Preserving finite colimits also implies preserving colimits over finite shapes in higher universes.

theorem CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesColimitsOfSize F] : PreservesFiniteColimits F

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

theorem CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesColimitsOfSize F] : PreservesFiniteColimits F

theorem CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesColimits F] : PreservesFiniteColimits F

theorem CategoryTheory.Limits.preservesFiniteColimits_of_preservesFiniteColimitsOfSize {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) (h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F) : PreservesFiniteColimits F

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

theorem CategoryTheory.Limits.comp_preservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteColimits F] [PreservesFiniteColimits G] : PreservesFiniteColimits (F.comp G)

The composition of two right exact functors is right exact.

theorem CategoryTheory.Limits.preservesFiniteColimits_of_natIso {C : Type u₁} [Category C] {D : Type u₂} [Category D] {F G : Functor C D} (h : Iso F G) [PreservesFiniteColimits F] : PreservesFiniteColimits G

Transfer preservation of finite colimits along a natural isomorphism in the functor.

structure CategoryTheory.Limits.PreservesFiniteCoproducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor F preserves finite products if it preserves all from Discrete J for Fintype J. We require this for J = Fin n in the definition, then generalize to J : Type u in the instance.

• preserves (n : Nat) : PreservesColimitsOfShape (Discrete (Fin n)) F

  preservation of colimits indexed by Discrete (Fin n).

theorem CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) (J : Type u) [Finite J] [PreservesFiniteCoproducts F] : PreservesColimitsOfShape (Discrete J) F

theorem CategoryTheory.Limits.comp_preservesFiniteCoproducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteCoproducts F] [PreservesFiniteCoproducts G] : PreservesFiniteCoproducts (F.comp G)

theorem CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [PreservesFiniteColimits F] : PreservesFiniteCoproducts F

structure CategoryTheory.Limits.ReflectsFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor is said to reflect finite colimits, if it reflects all colimits of shape J, where J : Type is a finite category.

• reflects (J : Type) [SmallCategory J] [FinCategory J] : ReflectsColimitsOfShape J F

theorem CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsColimitsOfSize F] : ReflectsFiniteColimits F

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

theorem CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimitsOfSize {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsColimitsOfSize F] : ReflectsFiniteColimits F

theorem CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsColimits F] : ReflectsFiniteColimits F

structure CategoryTheory.Limits.ReflectsFiniteCoproducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) : Prop

A functor F preserves finite coproducts if it reflects colimits of shape Discrete J for finite J.

We require this for J = Fin n in the definition, then generalize to J : Type u in the instance.

• reflects (n : Nat) : ReflectsColimitsOfShape (Discrete (Fin n)) F

theorem CategoryTheory.Limits.instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsFiniteCoproducts F] (J : Type u) [Finite J] : ReflectsColimitsOfShape (Discrete J) F

theorem CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteColimits (F.comp G)] [ReflectsFiniteColimits G] : PreservesFiniteColimits F

If F ⋙ G preserves finite colimits and G reflects finite colimits, then F preserves finite colimits.

theorem CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [PreservesFiniteCoproducts (F.comp G)] [ReflectsFiniteCoproducts G] : PreservesFiniteCoproducts F

If F ⋙ G preserves finite coproducts and G reflects finite coproducts, then F preserves finite coproducts.

theorem CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteColimits C] [PreservesFiniteColimits F] : ReflectsFiniteColimits F

theorem CategoryTheory.Limits.reflectsFiniteCoproductsOfReflectsIsomorphisms {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteCoproducts C] [PreservesFiniteCoproducts F] : ReflectsFiniteCoproducts F

theorem CategoryTheory.Limits.comp_reflectsFiniteCoproducts {C : Type u₁} [Category C] {D : Type u₂} [Category D] {E : Type u₃} [Category E] (F : Functor C D) (G : Functor D E) [ReflectsFiniteCoproducts F] [ReflectsFiniteCoproducts G] : ReflectsFiniteCoproducts (F.comp G)

theorem CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : Functor C D) [ReflectsFiniteColimits F] : ReflectsFiniteCoproducts F