mathlib3 documentation

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} [category_theory.category C] {J : Type w} [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 {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 : 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 w} [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 {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 : 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 w} [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 {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 : 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 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.)

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 w} [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 {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 : 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 w} [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 {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 : 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 w} [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 {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 : 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 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.)

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

Equations