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.
TODO: provide the dual result.
@[simp]
def
category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[H₁ : category_theory.limits.has_limit (category_theory.discrete.functor F.obj)]
[H₂ : category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))] :
Corresponding to any functor F : J ⥤ C, we construct a new functor from the walking parallel
pair of morphisms to C, given by the diagram
s
∏_j F j ===> Π_{f : j ⟶ j'} F j'
t
where the two morphisms s and t are defined componentwise:
- The
s_fcomponent is the projection∏_j F j ⟶ F jfollowed byf. - The
t_fcomponent is the projection∏_j F j ⟶ F j'.
In a moment we prove that cones over F are isomorphic to cones over this new diagram.
Equations
- category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram F = let pi_obj : C := ∏ F.obj, pi_hom : C := ∏ λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd, s : pi_obj ⟶ pi_hom := category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.pi.π F.obj f.fst.fst ≫ F.map f.snd), t : pi_obj ⟶ pi_hom := category_theory.limits.pi.lift (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), category_theory.limits.pi.π F.obj f.fst.snd) in category_theory.limits.parallel_pair s t
@[simp]
def
category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_hom
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[H₁ : category_theory.limits.has_limit (category_theory.discrete.functor F.obj)]
[H₂ : category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))] :
The morphism from cones over the walking pair diagram diagram F to cones over
the original diagram F.
Equations
- category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_hom F = {app := λ (X : Cᵒᵖ) (c : (category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram F).cones.obj X), {app := λ (j : J), c.app category_theory.limits.walking_parallel_pair.zero ≫ category_theory.limits.pi.π F.obj j, naturality' := _}, naturality' := _}
@[simp]
def
category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_inv
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[H₁ : category_theory.limits.has_limit (category_theory.discrete.functor F.obj)]
[H₂ : category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))] :
The morphism from cones over the original diagram F to cones over the walking pair diagram
diagram F.
Equations
- category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_inv F = {app := λ (X : Cᵒᵖ) (c : F.cones.obj X), (category_theory.limits.fork.of_ι (category_theory.limits.pi.lift c.app) _).π, naturality' := _}
def
category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_iso
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[H₁ : category_theory.limits.has_limit (category_theory.discrete.functor F.obj)]
[H₂ : category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))] :
The natural isomorphism between cones over the
walking pair diagram diagram F and cones over the original diagram F.
Equations
def
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.
Equations
- category_theory.limits.limits_from_equalizers_and_products = {has_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ C), category_theory.limits.has_limit.of_cones_iso (category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram F) F (category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_iso F)}}
def
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.
Equations
- category_theory.limits.finite_limits_from_equalizers_and_finite_products = λ (J : Type v) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), {has_limit := λ (F : J ⥤ C), category_theory.limits.has_limit.of_cones_iso (category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram F) F (category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_iso F)}