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.
(Implementation) Given the appropriate product and equalizer cones, build the cone for F
which is
limiting if the given cones are also.
(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' := _}
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.)
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
- 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) _))}
If G preserves equalizers and finite products, it preserves finite limits.
If G preserves equalizers and products, it preserves all limits.