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.
def
category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_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}
(t₁ : category_theory.limits.is_limit c₁)
(t₂ : category_theory.limits.is_limit c₂)
(hi : category_theory.limits.is_limit i) :
(Implementation) Show the cone constructed in build_limit is limiting, provided the cones used in
its construction are.
Equations
- category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit s t hs ht t₁ t₂ hi = {lift := λ (q : category_theory.limits.cone F), hi.lift (category_theory.limits.fork.of_ι (t₁.lift (category_theory.limits.fan.mk q.X (λ (j : J), q.π.app j))) _), fac' := _, uniq' := _}
noncomputable
def
category_theory.limits.limit_cone_of_equalizer_and_product
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_limit (category_theory.discrete.functor F.obj)]
[category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))]
[category_theory.limits.has_equalizers C] :
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
- category_theory.limits.limit_cone_of_equalizer_and_product F = {cone := category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.fst} ≫ F.map f.snd)) (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.snd})) _ _ (category_theory.limits.limit.cone (category_theory.limits.parallel_pair (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.fst} ≫ F.map f.snd)) (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.snd})))), is_limit := category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.fst} ≫ F.map f.snd)) (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.snd})) _ _ (category_theory.limits.limit.is_limit (category_theory.discrete.functor F.obj)) (category_theory.limits.limit.is_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))) (category_theory.limits.limit.is_limit (category_theory.limits.parallel_pair (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.fst} ≫ F.map f.snd)) (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.snd}))))}
theorem
category_theory.limits.has_limit_of_equalizer_and_product
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_limit (category_theory.discrete.functor F.obj)]
[category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))]
[category_theory.limits.has_equalizers C] :
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}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
[category_theory.limits.has_limits_of_size C]
(F : J ⥤ C) :
category_theory.limits.limit F ⟶ ∏ λ (j : J), F.obj j
A limit can be realised as a subobject of a product.
Equations
- category_theory.limits.limit_subobject_product F = (category_theory.limits.limit.iso_limit_cone (category_theory.limits.limit_cone_of_equalizer_and_product F)).hom ≫ category_theory.limits.equalizer.ι (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.fst} ≫ F.map f.snd)) (category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor F.obj) {as := f.fst.snd}))
Instances for category_theory.limits.limit_subobject_product
@[protected, instance]
def
category_theory.limits.limit_subobject_product_mono
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
[category_theory.limits.has_limits_of_size C]
(F : J ⥤ C) :
theorem
category_theory.limits.has_limits_of_has_equalizers_and_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
[category_theory.limits.has_equalizers C] :
Any category with products and equalizers has all limits.
theorem
category_theory.limits.has_finite_limits_of_has_equalizers_and_finite_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_equalizers C] :
Any category with finite products and equalizers has all finite limits.
noncomputable
def
category_theory.limits.preserves_limit_of_preserves_equalizers_and_product
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_limits_of_shape (category_theory.discrete J) C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete (Σ (p : J × J), p.fst ⟶ p.snd)) C]
[category_theory.limits.has_equalizers C]
(G : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair G]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete (Σ (p : J × J), p.fst ⟶ p.snd)) G] :
If a functor preserves equalizers and the appropriate products, it preserves limits.
Equations
- category_theory.limits.preserves_limit_of_preserves_equalizers_and_product G = {preserves_limit := λ (K : J ⥤ C), let P : C := ∏ K.obj, Q : C := ∏ λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.obj f.fst.snd, s : P ⟶ Q := category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor K.obj) {as := f.fst.fst} ≫ K.map f.snd), t : P ⟶ Q := category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.limit.π (category_theory.discrete.functor K.obj) {as := f.fst.snd}), I : C := category_theory.limits.equalizer s t, i : I ⟶ P := category_theory.limits.equalizer.ι s t in category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit s t _ _ (category_theory.limits.limit.is_limit (category_theory.discrete.functor K.obj)) (category_theory.limits.limit.is_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.obj f.fst.snd))) (category_theory.limits.limit.is_limit (category_theory.limits.parallel_pair s t))) ((category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit (G.map s) (G.map t) _ _ (category_theory.limits.is_limit_of_has_product_of_preserves_limit G K.obj) (category_theory.limits.is_limit_of_has_product_of_preserves_limit G (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.obj f.fst.snd)) (category_theory.limits.is_limit_fork_map_of_is_limit G _ (category_theory.limits.equalizer_is_equalizer s t))).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl (category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit (G.map s) (G.map t) _ _ (category_theory.limits.fork.of_ι (G.map i) _)).X) _))}
noncomputable
def
category_theory.limits.preserves_finite_limits_of_preserves_equalizers_and_finite_products
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_finite_products C]
(G : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair G]
[Π (J : Type) [_inst_8 : fintype J], category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G] :
If G preserves equalizers and finite products, it preserves finite limits.
Equations
noncomputable
def
category_theory.limits.preserves_limits_of_preserves_equalizers_and_products
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_products C]
(G : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair G]
[Π (J : Type w), category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G] :
If G preserves equalizers and products, it preserves all limits.
noncomputable
def
category_theory.limits.preserves_finite_limits_of_preserves_terminal_and_pullbacks
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C]
(G : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) G]
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan G] :
If G preserves terminal objects and pullbacks, it preserves all finite limits.
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.
@[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) :
def
category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_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}
(t₁ : category_theory.limits.is_colimit c₁)
(t₂ : category_theory.limits.is_colimit c₂)
(hi : category_theory.limits.is_colimit i) :
(Implementation) Show the cocone constructed in build_colimit is colimiting,
provided the cocones used in its construction are.
Equations
- category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_colimit s t hs ht t₁ t₂ hi = {desc := λ (q : category_theory.limits.cocone F), hi.desc (category_theory.limits.cofork.of_π (t₂.desc (category_theory.limits.cofan.mk q.X (λ (j : J), q.ι.app j))) _), fac' := _, uniq' := _}
noncomputable
def
category_theory.limits.colimit_cocone_of_coequalizer_and_coproduct
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_colimit (category_theory.discrete.functor F.obj)]
[category_theory.limits.has_colimit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.fst))]
[category_theory.limits.has_coequalizers C] :
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
- category_theory.limits.colimit_cocone_of_coequalizer_and_coproduct F = {cocone := category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.map f.snd ≫ category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.snd})) (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.fst})) _ _ (category_theory.limits.colimit.cocone (category_theory.limits.parallel_pair (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.map f.snd ≫ category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.snd})) (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.fst})))), is_colimit := category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_colimit (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.map f.snd ≫ category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.snd})) (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.fst})) _ _ (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.fst))) (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor F.obj)) (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.map f.snd ≫ category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.snd})) (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.fst}))))}
theorem
category_theory.limits.has_colimit_of_coequalizer_and_coproduct
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_colimit (category_theory.discrete.functor F.obj)]
[category_theory.limits.has_colimit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.fst))]
[category_theory.limits.has_coequalizers C] :
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}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
[category_theory.limits.has_colimits_of_size C]
(F : J ⥤ C) :
(∐ λ (j : J), F.obj j) ⟶ category_theory.limits.colimit F
A colimit can be realised as a quotient of a coproduct.
Equations
- category_theory.limits.colimit_quotient_coproduct F = category_theory.limits.coequalizer.π (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.map f.snd ≫ category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.snd})) (category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.colimit.ι (category_theory.discrete.functor F.obj) {as := f.fst.fst})) ≫ (category_theory.limits.colimit.iso_colimit_cocone (category_theory.limits.colimit_cocone_of_coequalizer_and_coproduct F)).inv
Instances for category_theory.limits.colimit_quotient_coproduct
@[protected, instance]
theorem
category_theory.limits.has_colimits_of_has_coequalizers_and_coproducts
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_coequalizers C] :
Any category with coproducts and coequalizers has all colimits.
theorem
category_theory.limits.has_finite_colimits_of_has_coequalizers_and_finite_coproducts
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.limits.has_coequalizers C] :
Any category with finite coproducts and coequalizers has all finite colimits.
noncomputable
def
category_theory.limits.preserves_colimit_of_preserves_coequalizers_and_coproduct
{C : Type u}
[category_theory.category C]
{J : Type w}
[category_theory.small_category J]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete J) C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete (Σ (p : J × J), p.fst ⟶ p.snd)) C]
[category_theory.limits.has_coequalizers C]
(G : C ⥤ D)
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_parallel_pair G]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) G]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete (Σ (p : J × J), p.fst ⟶ p.snd)) G] :
If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits.
Equations
- category_theory.limits.preserves_colimit_of_preserves_coequalizers_and_coproduct G = {preserves_colimit := λ (K : J ⥤ C), let P : C := ∐ K.obj, Q : C := ∐ λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.obj f.fst.fst, s : Q ⟶ P := category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.map f.snd ≫ category_theory.limits.colimit.ι (category_theory.discrete.functor K.obj) {as := f.fst.snd}), t : Q ⟶ P := category_theory.limits.sigma.desc (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.colimit.ι (category_theory.discrete.functor K.obj) {as := f.fst.fst}), I : C := category_theory.limits.coequalizer s t, i : P ⟶ I := category_theory.limits.coequalizer.π s t in category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_colimit s t _ _ (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.obj f.fst.fst))) (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor K.obj)) (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair s t))) ((category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_colimit (G.map s) (G.map t) _ _ (category_theory.limits.is_colimit_of_has_coproduct_of_preserves_colimit G (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), K.obj f.fst.fst)) (category_theory.limits.is_colimit_of_has_coproduct_of_preserves_colimit G K.obj) (category_theory.limits.is_colimit_cofork_map_of_is_colimit G _ (category_theory.limits.coequalizer_is_coequalizer s t))).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl (category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_colimit (G.map s) (G.map t) _ _ (category_theory.limits.cofork.of_π (G.map i) _)).X) _))}
noncomputable
def
category_theory.limits.preserves_finite_colimits_of_preserves_coequalizers_and_finite_coproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_coequalizers C]
[category_theory.limits.has_finite_coproducts C]
(G : C ⥤ D)
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_parallel_pair G]
[Π (J : Type) [_inst_8 : fintype J], category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) G] :
If G preserves coequalizers and finite coproducts, it preserves finite colimits.
Equations
- category_theory.limits.preserves_finite_colimits_of_preserves_coequalizers_and_finite_coproducts G = {preserves_finite_colimits := λ (_x : Type) (_x_1 : category_theory.small_category _x) (_x_2 : category_theory.fin_category _x), category_theory.limits.preserves_colimit_of_preserves_coequalizers_and_coproduct G}
noncomputable
def
category_theory.limits.preserves_colimits_of_preserves_coequalizers_and_coproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_coequalizers C]
[category_theory.limits.has_coproducts C]
(G : C ⥤ D)
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_parallel_pair G]
[Π (J : Type w), category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) G] :
If G preserves coequalizers and coproducts, it preserves all colimits.
noncomputable
def
category_theory.limits.preserves_finite_colimits_of_preserves_initial_and_pushouts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_initial C]
[category_theory.limits.has_pushouts C]
(G : C ⥤ D)
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete pempty) G]
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span G] :
If G preserves initial objects and pushouts, it preserves all finite colimits.