Constructing limits from products and equalizers.

If a category has all products, and all equalizers, then it has all limits. Similarly, if it has all finite products, and all equalizers, then it has all finite limits.

If a functor preserves all products and equalizers, then it preserves all limits. Similarly, if it preserves all finite products and equalizers, then it preserves all finite limits.

TODO

Provide the dual results. Show the analogous results for functors which reflect or create (co)limits.

@[simp]

theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.2} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.toPrefunctor.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).pt = i.pt

@[simp]

theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.2} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.toPrefunctor.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) (j : J) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).π.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι i) (c₁.π.app { as := j })

def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.2} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.toPrefunctor.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : CategoryTheory.Limits.Cone F

(Implementation) Given the appropriate product and equalizer cones, build the cone for F which is limiting if the given cones are also.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.2} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.toPrefunctor.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) {i : CategoryTheory.Limits.Fork s t} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) (hi : CategoryTheory.Limits.IsLimit i) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i)

(Implementation) Show the cone constructed in buildLimit is limiting, provided the cones used in its construction are.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.limitConeOfEqualizerAndProduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.2)] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.LimitCone F

Given the existence of the appropriate (possibly finite) products and equalizers, we can construct a limit cone for F. (This assumes the existence of all equalizers, which is technically stronger than needed.)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasLimit_of_equalizer_and_product {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.2)] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasLimit F

Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of F exists. (This assumes the existence of all equalizers, which is technically stronger than needed.)

noncomputable def CategoryTheory.Limits.limitSubobjectProduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.limit F ⟶ ∏ fun (j : J) => F.toPrefunctor.obj j

A limit can be realised as a subobject of a product.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.limitSubobjectProduct_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Mono (CategoryTheory.Limits.limitSubobjectProduct F)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C

Any category with products and equalizers has all limits.

See .

theorem CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasFiniteLimits C

Any category with finite products and equalizers has all finite limits.

See .

noncomputable def CategoryTheory.Limits.preservesLimitOfPreservesEqualizersAndProduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C] [CategoryTheory.Limits.HasEqualizers C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G] : CategoryTheory.Limits.PreservesLimitsOfShape J G

If a functor preserves equalizers and the appropriate products, it preserves limits.

Equations

• CategoryTheory.Limits.preservesLimitOfPreservesEqualizersAndProduct G = CategoryTheory.Limits.PreservesLimitsOfShape.mk

noncomputable def CategoryTheory.Limits.preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasFiniteProducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesFiniteProducts G] : CategoryTheory.Limits.PreservesFiniteLimits G

If G preserves equalizers and finite products, it preserves finite limits.

Equations

• CategoryTheory.Limits.preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts G = CategoryTheory.Limits.PreservesFiniteLimits.mk

noncomputable def CategoryTheory.Limits.preservesLimitsOfPreservesEqualizersAndProducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasProducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [(J : Type w) → CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w, v, v₂, u, u₂} G

If G preserves equalizers and products, it preserves all limits.

Equations

• CategoryTheory.Limits.preservesLimitsOfPreservesEqualizersAndProducts G = CategoryTheory.Limits.PreservesLimitsOfSize.mk

theorem CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasFiniteLimits C

noncomputable def CategoryTheory.Limits.preservesFiniteLimitsOfPreservesTerminalAndPullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] : CategoryTheory.Limits.PreservesFiniteLimits G

If G preserves terminal objects and pullbacks, it preserves all finite limits.

Equations

• CategoryTheory.Limits.preservesFiniteLimitsOfPreservesTerminalAndPullbacks G = CategoryTheory.Limits.preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts G

We now dualize the above constructions, resorting to copy-paste.

@[simp]

theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) (j : J) : (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).ι.app j = CategoryTheory.CategoryStruct.comp (c₂.ι.app { as := j }) (CategoryTheory.Limits.Cofork.π i)

@[simp]

theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) : (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).pt = i.pt

def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) : CategoryTheory.Limits.Cocone F

(Implementation) Given the appropriate coproduct and coequalizer cocones, build the cocone for F which is colimiting if the given cocones are also.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt ⟶ c₂.pt) (t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) {i : CategoryTheory.Limits.Cofork s t} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) (hi : CategoryTheory.Limits.IsColimit i) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i)

(Implementation) Show the cocone constructed in buildColimit is colimiting, provided the cocones used in its construction are.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.colimitCoconeOfCoequalizerAndCoproduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.1)] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.ColimitCocone F

Given the existence of the appropriate (possibly finite) coproducts and coequalizers, we can construct a colimit cocone for F. (This assumes the existence of all coequalizers, which is technically stronger than needed.)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasColimit_of_coequalizer_and_coproduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) => F.toPrefunctor.obj f.fst.1)] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasColimit F

Given the existence of the appropriate (possibly finite) coproducts and coequalizers, we know a colimit of F exists. (This assumes the existence of all coequalizers, which is technically stronger than needed.)

noncomputable def CategoryTheory.Limits.colimitQuotientCoproduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C) : (∐ fun (j : J) => F.toPrefunctor.obj j) ⟶ CategoryTheory.Limits.colimit F

A colimit can be realised as a quotient of a coproduct.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.colimitQuotientCoproduct_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Epi (CategoryTheory.Limits.colimitQuotientCoproduct F)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C

Any category with coproducts and coequalizers has all colimits.

See .

theorem CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasFiniteColimits C

Any category with finite coproducts and coequalizers has all finite colimits.

See .

noncomputable def CategoryTheory.Limits.preservesColimitOfPreservesCoequalizersAndCoproduct {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C] [CategoryTheory.Limits.HasCoequalizers C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) G] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G] : CategoryTheory.Limits.PreservesColimitsOfShape J G

If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits.

Equations

• CategoryTheory.Limits.preservesColimitOfPreservesCoequalizersAndCoproduct G = CategoryTheory.Limits.PreservesColimitsOfShape.mk

noncomputable def CategoryTheory.Limits.preservesFiniteColimitsOfPreservesCoequalizersAndFiniteCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasFiniteCoproducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesFiniteCoproducts G] : CategoryTheory.Limits.PreservesFiniteColimits G

If G preserves coequalizers and finite coproducts, it preserves finite colimits.

Equations

• CategoryTheory.Limits.preservesFiniteColimitsOfPreservesCoequalizersAndFiniteCoproducts G = CategoryTheory.Limits.PreservesFiniteColimits.mk

noncomputable def CategoryTheory.Limits.preservesColimitsOfPreservesCoequalizersAndCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasCoproducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [(J : Type w) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, v, v₂, u, u₂} G

If G preserves coequalizers and coproducts, it preserves all colimits.

Equations

• CategoryTheory.Limits.preservesColimitsOfPreservesCoequalizersAndCoproducts G = CategoryTheory.Limits.PreservesColimitsOfSize.mk

theorem CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasFiniteColimits C

noncomputable def CategoryTheory.Limits.preservesFiniteColimitsOfPreservesInitialAndPushouts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] : CategoryTheory.Limits.PreservesFiniteColimits G

If G preserves initial objects and pushouts, it preserves all finite colimits.

Equations

• CategoryTheory.Limits.preservesFiniteColimitsOfPreservesInitialAndPushouts G = CategoryTheory.Limits.preservesFiniteColimitsOfPreservesCoequalizersAndFiniteCoproducts G