Products in the over category #
Shows that products in the over category can be derived from wide pullbacks in the base category.
The main result is over_product_of_wide_pullback, which says that if C has J-indexed wide
pullbacks, then over B has J-indexed products.
@[reducible]
def
category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Implementation)
Given a product diagram in C/B, construct the corresponding wide pullback diagram
in C.
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_obj_π_app
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F)
(X : category_theory.limits.wide_pullback_shape J) :
def
category_theory.over.construct_products.cones_equiv_inverse_obj
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F) :
(Impl) A preliminary definition to avoid timeouts.
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_obj_X
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F) :
def
category_theory.over.construct_products.cones_equiv_inverse
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_inverse B F = {obj := category_theory.over.construct_products.cones_equiv_inverse_obj B F, map := λ (c₁ c₂ : category_theory.limits.cone F) (f : c₁ ⟶ c₂), {hom := f.hom.left, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_obj_2
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_map_hom
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c₁ c₂ : category_theory.limits.cone F)
(f : c₁ ⟶ c₂) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_map_hom
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c₁ c₂ : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))
(f : c₁ ⟶ c₂) :
def
category_theory.over.construct_products.cones_equiv_functor
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_functor B F = {obj := λ (c : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)), {X := category_theory.over.mk (c.π.app option.none), π := {app := λ (_x : category_theory.discrete J), category_theory.over.construct_products.cones_equiv_functor._match_1 B F c _x, naturality' := _}}, map := λ (c₁ c₂ : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)) (f : c₁ ⟶ c₂), {hom := category_theory.over.hom_mk f.hom _, w' := _}, map_id' := _, map_comp' := _}
- category_theory.over.construct_products.cones_equiv_functor._match_1 B F c {as := j} = category_theory.over.hom_mk (c.π.app (option.some j)) _
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_obj_X
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_obj_π_app
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type w}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))
(_x : category_theory.discrete J) :
((category_theory.over.construct_products.cones_equiv_functor B F).obj c).π.app _x = category_theory.over.construct_products.cones_equiv_functor._match_1 B F c _x
@[simp]
def
category_theory.over.construct_products.cones_equiv_unit_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_unit_iso B F = category_theory.nat_iso.of_components (λ (_x : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)), category_theory.limits.cones.ext {hom := 𝟙 ((𝟭 (category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))).obj _x).X, inv := 𝟙 ((category_theory.over.construct_products.cones_equiv_functor B F ⋙ category_theory.over.construct_products.cones_equiv_inverse B F).obj _x).X, hom_inv_id' := _, inv_hom_id' := _} _) _
@[simp]
def
category_theory.over.construct_products.cones_equiv_counit_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_counit_iso B F = category_theory.nat_iso.of_components (λ (_x : category_theory.limits.cone F), category_theory.limits.cones.ext {hom := category_theory.over.hom_mk (𝟙 ((category_theory.over.construct_products.cones_equiv_inverse B F ⋙ category_theory.over.construct_products.cones_equiv_functor B F).obj _x).X.left) _, inv := category_theory.over.hom_mk (𝟙 ((𝟭 (category_theory.limits.cone F)).obj _x).X.left) _, hom_inv_id' := _, inv_hom_id' := _} _) _
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_2
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
def
category_theory.over.construct_products.cones_equiv
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) Establish an equivalence between the category of cones for F and for the "grown" F.
Equations
- category_theory.over.construct_products.cones_equiv B F = {functor := category_theory.over.construct_products.cones_equiv_functor B F, inverse := category_theory.over.construct_products.cones_equiv_inverse B F, unit_iso := category_theory.over.construct_products.cones_equiv_unit_iso B F, counit_iso := category_theory.over.construct_products.cones_equiv_counit_iso B F, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_counit_iso_2
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_unit_iso_2
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_2
{J : Type w}
{C : Type u}
[category_theory.category C]
(B : C)
(F : category_theory.discrete J ⥤ category_theory.over B) :
theorem
category_theory.over.construct_products.has_over_limit_discrete_of_wide_pullback_limit
{J : Type w}
{C : Type u}
[category_theory.category C]
{B : C}
(F : category_theory.discrete J ⥤ category_theory.over B)
[category_theory.limits.has_limit (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)] :
Use the above equivalence to prove we have a limit.
theorem
category_theory.over.construct_products.over_product_of_wide_pullback
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.limits.wide_pullback_shape J) C]
{B : C} :
Given a wide pullback in C, construct a product in C/B.
theorem
category_theory.over.construct_products.over_binary_product_of_pullback
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{B : C} :
Given a pullback in C, construct a binary product in C/B.
theorem
category_theory.over.construct_products.over_products_of_wide_pullbacks
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_wide_pullbacks C]
{B : C} :
Given all wide pullbacks in C, construct products in C/B.
theorem
category_theory.over.construct_products.over_finite_products_of_finite_wide_pullbacks
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_wide_pullbacks C]
{B : C} :
Given all finite wide pullbacks in C, construct finite products in C/B.
Construct terminal object in the over category. This isn't an instance as it's not typically the
way we want to define terminal objects.
(For instance, this gives a terminal object which is different from the generic one given by
over_product_of_wide_pullback above.)