# Documentation

Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

# 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} {J : Type w} {F : } {c₁ : } {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.snd} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.fst }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.snd }) (i : ) :
= i.pt
@[simp]
theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app {C : Type u} {J : Type w} {F : } {c₁ : } {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.snd} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.fst }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.snd }) (i : ) (j : J) :
.app j = CategoryTheory.CategoryStruct.comp () (c₁.app { as := j })
def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit {C : Type u} {J : Type w} {F : } {c₁ : } {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.snd} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.fst }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.snd }) (i : ) :

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

Instances For
def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit {C : Type u} {J : Type w} {F : } {c₁ : } {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.snd} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.fst }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.snd }) {i : } (t₁ : ) (t₂ : ) (hi : ) :

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

Instances For

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.)

Instances For

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} {J : Type w} [] (F : ) :
fun j => F.obj j

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

Instances For

Any category with products and equalizers has all limits.

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

@[simp]
theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.fst} {c₂ : } (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.snd })) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.fst }) (i : ) (j : J) :
.app j = CategoryTheory.CategoryStruct.comp (c₂.app { as := j }) ()
@[simp]
theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.fst} {c₂ : } (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.snd })) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.fst }) (i : ) :
= i.pt
def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.fst} {c₂ : } (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.snd })) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.fst }) (i : ) :

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

Instances For
def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.fst} {c₂ : } (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.snd })) (ht : ∀ (f : (p : J × J) × (p.fst p.snd)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.fst }) {i : } (t₁ : ) (t₂ : ) (hi : ) :

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

Instances For

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.)

Instances For

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} {J : Type w} [] (F : ) :
( fun j => F.obj j)

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

Instances For

Any category with coproducts and coequalizers has all colimits.

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For