mathlib documentation

category_theory.limits.constructions.limits_of_products_and_equalizers

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 category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit_π_app {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {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 f = c₁.π.app f.fst.fst F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app f = c₁.π.app f.fst.snd) (i : category_theory.limits.fork s t) (j : J) :
@[simp]
theorem category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit_X {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {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 f = c₁.π.app f.fst.fst F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app f = c₁.π.app f.fst.snd) (i : category_theory.limits.fork s t) :
def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {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 f = c₁.π.app f.fst.fst F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst p.snd), t c₂.π.app f = c₁.π.app f.fst.snd) (i : category_theory.limits.fork s t) :

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

Equations

(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 know a limit of F exists. (This assumes the existence of all equalizers, which is technically stronger than needed.)

If a functor preserves equalizers and the appropriate products, it preserves 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} [category_theory.category C] {J : Type v} [category_theory.small_category J] {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 f s = F.map f.snd c₂.ι.app f.fst.snd) (ht : ∀ (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app f t = c₂.ι.app f.fst.fst) (i : category_theory.limits.cofork s 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} [category_theory.category C] {J : Type v} [category_theory.small_category J] {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 f s = F.map f.snd c₂.ι.app f.fst.snd) (ht : ∀ (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app f t = c₂.ι.app f.fst.fst) (i : category_theory.limits.cofork s t) :
@[simp]
theorem category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit_ι_app {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {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 f s = F.map f.snd c₂.ι.app f.fst.snd) (ht : ∀ (f : Σ (p : J × J), p.fst p.snd), c₁.ι.app f t = c₂.ι.app f.fst.fst) (i : category_theory.limits.cofork s t) (j : J) :

(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 know a colimit of F exists. (This assumes the existence of all coequalizers, which is technically stronger than needed.)

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

Equations