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

(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.
Instances For
def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit {C : Type u} {J : Type w} {F : } {c₁ : } {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 p.2)) => F.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.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 : } (t₁ : ) (t₂ : ) (hi : ) :

(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.
Instances For
noncomputable def CategoryTheory.Limits.limitConeOfEqualizerAndProduct {C : Type u} {J : Type w} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2)] :

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.
Instances For
theorem CategoryTheory.Limits.hasLimit_of_equalizer_and_product {C : Type u} {J : Type w} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2)] :

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 : J) => F.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.
Instances For
instance CategoryTheory.Limits.limitSubobjectProduct_mono {C : Type u} {J : Type w} [] (F : ) :
Equations
• =

Any category with products and equalizers has all limits.

See .

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

See .

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

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

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

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

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

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

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

Equations
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 : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : } (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.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 : ) (j : J) :
.app j = CategoryTheory.CategoryStruct.comp (c₂.app { as := j }) i
@[simp]
theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : } (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.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 : ) :
= i.pt
def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : } (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.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 : ) :

(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.
Instances For
def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit {C : Type u} {J : Type w} {F : } {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : } (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.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 : } (t₁ : ) (t₂ : ) (hi : ) :

(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.
Instances For
noncomputable def CategoryTheory.Limits.colimitCoconeOfCoequalizerAndCoproduct {C : Type u} {J : Type w} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1)] :

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.
Instances For
theorem CategoryTheory.Limits.hasColimit_of_coequalizer_and_coproduct {C : Type u} {J : Type w} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1)] :

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 : J) => F.obj j)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Limits.colimitQuotientCoproduct_epi {C : Type u} {J : Type w} [] (F : ) :
Equations
• =

Any category with coproducts and coequalizers has all colimits.

See .

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

See .

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

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

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

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

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

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

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

Equations
Instances For