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.

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

source

class CategoryTheory.Limits.PreservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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) [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J], CategoryTheory.Limits.PreservesLimitsOfShape J F

Instances

source

instance CategoryTheory.Limits.instSubsingletonPreservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.PreservesFiniteLimits F)

Equations

⋯ = ⋯

source

@[instance 100]

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

CategoryTheory.Limits.PreservesLimitsOfShape J F

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

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteLimits F

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

source

@[instance 120]

instance CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :

CategoryTheory.Limits.PreservesFiniteLimits F

Equations

⋯ = ⋯

source

@[instance 120]

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

CategoryTheory.Limits.PreservesFiniteLimits F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteLimits F

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

source

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

CategoryTheory.Limits.PreservesFiniteLimits (F.comp G)

The composition of two left exact functors is left exact.

source

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

CategoryTheory.Limits.PreservesFiniteLimits G

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

source

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

Prop

A functor F preserves finite products if it preserves all from Discrete J for Fintype J

preserves : ∀ (J : Type) [inst : Fintype J], CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

Instances

source

instance CategoryTheory.Limits.instSubsingletonPreservesFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.PreservesFiniteProducts F)

Equations

⋯ = ⋯

source

@[instance 100]

instance CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteProducts F] :

CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteProducts F

Equations

⋯ = ⋯

source

class CategoryTheory.Limits.ReflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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) [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J], CategoryTheory.Limits.ReflectsLimitsOfShape J F

Instances

source

instance CategoryTheory.Limits.instSubsingletonReflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.ReflectsFiniteLimits F)

Equations

⋯ = ⋯

source

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

Prop

A functor F preserves finite products if it reflects limits of shape Discrete J for finite J

reflects : ∀ (J : Type) [inst : Fintype J], CategoryTheory.Limits.ReflectsLimitsOfShape (CategoryTheory.Discrete J) F

Instances

source

instance CategoryTheory.Limits.instSubsingletonReflectsFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.ReflectsFiniteProducts F)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteLimits F

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

source

@[instance 120]

instance CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :

CategoryTheory.Limits.ReflectsFiniteLimits F

Equations

⋯ = ⋯

source

@[instance 120]

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

CategoryTheory.Limits.ReflectsFiniteLimits F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteLimits F

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

source

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

CategoryTheory.Limits.PreservesFiniteProducts F

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

source

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

CategoryTheory.Limits.ReflectsFiniteLimits F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteProducts F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteProducts (F.comp G)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteProducts F

Equations

⋯ = ⋯

source

class CategoryTheory.Limits.PreservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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) [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J], CategoryTheory.Limits.PreservesColimitsOfShape J F

Instances

source

instance CategoryTheory.Limits.instSubsingletonPreservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.PreservesFiniteColimits F)

Equations

⋯ = ⋯

source

@[instance 100]

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

CategoryTheory.Limits.PreservesColimitsOfShape J F

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

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteColimits F

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

source

@[instance 120]

instance CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :

CategoryTheory.Limits.PreservesFiniteColimits F

Equations

⋯ = ⋯

source

@[instance 120]

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

CategoryTheory.Limits.PreservesFiniteColimits F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteColimits F

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

source

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

CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)

The composition of two right exact functors is right exact.

source

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

CategoryTheory.Limits.PreservesFiniteColimits G

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

source

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

Prop

A functor F preserves finite products if it preserves all from Discrete J for Fintype J

preserves : ∀ (J : Type) [inst : Fintype J], CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
preservation of colimits indexed by Discrete J when [Fintype J]

Instances

source

instance CategoryTheory.Limits.instSubsingletonPreservesFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.PreservesFiniteCoproducts F)

Equations

⋯ = ⋯

source

@[instance 100]

instance CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteCoproducts F] :

CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteCoproducts (F.comp G)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteCoproducts F

Equations

⋯ = ⋯

source

class CategoryTheory.Limits.ReflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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) [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J], CategoryTheory.Limits.ReflectsColimitsOfShape J F

Instances

source

instance CategoryTheory.Limits.instSubsingletonReflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.ReflectsFiniteColimits F)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteColimits F

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

source

@[instance 120]

instance CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :

CategoryTheory.Limits.ReflectsFiniteColimits F

Equations

⋯ = ⋯

source

@[instance 120]

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

CategoryTheory.Limits.ReflectsFiniteColimits F

Equations

⋯ = ⋯

source

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

Prop

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

reflects : ∀ (J : Type) [inst : Fintype J], CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete J) F

Instances

source

instance CategoryTheory.Limits.instSubsingletonReflectsFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

Subsingleton (CategoryTheory.Limits.ReflectsFiniteCoproducts F)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.PreservesFiniteColimits F

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

source

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

CategoryTheory.Limits.PreservesFiniteCoproducts F

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

source

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

CategoryTheory.Limits.ReflectsFiniteColimits F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteCoproducts F

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteCoproducts (F.comp G)

Equations

⋯ = ⋯

source

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

CategoryTheory.Limits.ReflectsFiniteCoproducts F

Equations

⋯ = ⋯

HepLean Documentation

Mathlib.CategoryTheory.Limits.Preserves.Finite

Preservation of finite (co)limits. #

Preservation of finite (co)limits. #

Related results #