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.
def
category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_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}
(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' := _}
theorem
category_theory.limits.has_limit_of_equalizer_and_product
{C : Type u}
[category_theory.category C]
{J : Type v}
[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.)
theorem
category_theory.limits.limits_from_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.finite_limits_from_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.
def
category_theory.limits.preserves_limit_of_preserves_equalizers_and_product
{C : Type u}
[category_theory.category C]
{J : Type v}
[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) 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) 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) _))}
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 v) [_inst_8 : fintype J], category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G]
(J : Type v)
[category_theory.small_category J]
[category_theory.fin_category J] :
If G preserves equalizers and finite products, it preserves finite limits.
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 v), category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G] :
If G preserves equalizers and products, it preserves all 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 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.
@[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) :
def
category_theory.limits.has_colimit_of_has_coproducts_of_has_coequalizers.build_is_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}
(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' := _}
theorem
category_theory.limits.has_colimit_of_coequalizer_and_coproduct
{C : Type u}
[category_theory.category C]
{J : Type v}
[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.)
theorem
category_theory.limits.colimits_from_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.finite_colimits_from_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.
def
category_theory.limits.preserves_colimit_of_preserves_coequalizers_and_coproduct
{C : Type u}
[category_theory.category C]
{J : Type v}
[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) 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) 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) _))}
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 v) [_inst_8 : fintype J], category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) G]
(J : Type v)
[category_theory.small_category J]
[category_theory.fin_category J] :
If G preserves coequalizers and finite coproducts, it preserves finite colimits.
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 v), category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) G] :
If G preserves coequalizers and coproducts, it preserves all colimits.