# mathlib3documentation

category_theory.limits.constructions.limits_of_products_and_equalizers

# Constructing limits from products and equalizers. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit_π_app {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.snd)} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), s c₂.π.app {as := f} = c₁.π.app {as := f.fst.fst} F.map f.snd) (ht : (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app {as := f} = c₁.π.app {as := f.fst.snd}) (i : t) (j : J) :
= i.ι c₁.π.app {as := j}
@[simp]
theorem category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit_X {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.snd)} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), s c₂.π.app {as := f} = c₁.π.app {as := f.fst.fst} F.map f.snd) (ht : (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app {as := f} = c₁.π.app {as := f.fst.snd}) (i : t) :
def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.snd)} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), s c₂.π.app {as := f} = c₁.π.app {as := f.fst.fst} F.map f.snd) (ht : (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app {as := f} = c₁.π.app {as := f.fst.snd}) (i : t) :

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

Equations
def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.snd)} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), s c₂.π.app {as := f} = c₁.π.app {as := f.fst.fst} F.map f.snd) (ht : (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app {as := f} = c₁.π.app {as := f.fst.snd}) {i : t} (t₁ : category_theory.limits.is_limit c₁) (t₂ : category_theory.limits.is_limit c₂)  :

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

Equations

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

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 category_theory.limits.limit_subobject_product {C : Type u} {J : Type w} (F : J C) :
λ (j : J), F.obj j

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

Equations
Instances for category_theory.limits.limit_subobject_product
@[protected, instance]

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.

Equations

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

Equations

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

Equations

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

Equations

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

def category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.cofan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.fst)} {c₂ : category_theory.limits.cofan F.obj} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} s = F.map f.snd c₂.ι.app {as := f.fst.snd}) (ht : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} t = c₂.ι.app {as := f.fst.fst}) (i : t) :

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

Equations
@[simp]
theorem category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit_X {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.cofan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.fst)} {c₂ : category_theory.limits.cofan F.obj} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} s = F.map f.snd c₂.ι.app {as := f.fst.snd}) (ht : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} t = c₂.ι.app {as := f.fst.fst}) (i : t) :
@[simp]
theorem category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit_ι_app {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.cofan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.fst)} {c₂ : category_theory.limits.cofan F.obj} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} s = F.map f.snd c₂.ι.app {as := f.fst.snd}) (ht : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} t = c₂.ι.app {as := f.fst.fst}) (i : t) (j : J) :
= c₂.ι.app {as := j} i.π
def category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_colimit {C : Type u} {J : Type w} {F : J C} {c₁ : category_theory.limits.cofan (λ (f : Σ (p : J × J), p.fst p.snd), F.obj f.fst.fst)} {c₂ : category_theory.limits.cofan F.obj} (s t : c₁.X c₂.X) (hs : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} s = F.map f.snd c₂.ι.app {as := f.fst.snd}) (ht : (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app {as := f} t = c₂.ι.app {as := f.fst.fst}) {i : t}  :

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

Equations

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

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 category_theory.limits.colimit_quotient_coproduct {C : Type u} {J : Type w} (F : J C) :
( λ (j : J), F.obj j)

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

Equations
Instances for category_theory.limits.colimit_quotient_coproduct
@[protected, instance]

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.

Equations

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

Equations

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

Equations

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

Equations