# mathlibdocumentation

category_theory.limits.constructions.over.products

# 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.

(Implementation) Given a product diagram in C/B, construct the corresponding wide pullback diagram in C.

Equations
@[simp]
theorem category_theory.over.construct_products.cones_equiv_inverse_obj_π_app {C : Type u} (B : C) {J : Type v}  :
= option.cases_on X c.X.hom (λ (j : J), (c.π.app j).left)
def category_theory.over.construct_products.cones_equiv_inverse_obj {C : Type u} (B : C) {J : Type v}  :

(Impl) A preliminary definition to avoid timeouts.

Equations
@[simp]
theorem category_theory.over.construct_products.cones_equiv_inverse_obj_X {C : Type u} (B : C) {J : Type v}  :

(Impl) A preliminary definition to avoid timeouts.

Equations
@[simp]
theorem category_theory.over.construct_products.cones_equiv_inverse_obj_2 {C : Type u} (B : C) {J : Type v}  :
@[simp]
theorem category_theory.over.construct_products.cones_equiv_inverse_map_hom {C : Type u} (B : C) {J : Type v} (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} (B : C) {J : Type v} (f : c₁ c₂) :

(Impl) A preliminary definition to avoid timeouts.

Equations
@[simp]
theorem category_theory.over.construct_products.cones_equiv_functor_obj_X {C : Type u} (B : C) {J : Type v}  :
@[simp]

(Impl) A preliminary definition to avoid timeouts.

Equations
@[simp]

(Impl) A preliminary definition to avoid timeouts.

Equations
@[simp]
theorem category_theory.over.construct_products.cones_equiv_inverse_2 {J : Type v} {C : Type u} (B : C)  :

(Impl) Establish an equivalence between the category of cones for F and for the "grown" F.

Equations
@[simp]
theorem category_theory.over.construct_products.cones_equiv_counit_iso_2 {J : Type v} {C : Type u} (B : C)  :
@[simp]
theorem category_theory.over.construct_products.cones_equiv_unit_iso_2 {J : Type v} {C : Type u} (B : C)  :
@[simp]
theorem category_theory.over.construct_products.cones_equiv_functor_2 {J : Type v} {C : Type u} (B : C)  :

Use the above equivalence to prove we have a limit.

Given a wide pullback in C, construct a product in C/B.

Given a pullback in C, construct a binary product in C/B.

Given all wide pullbacks in C, construct products in C/B.

Given all finite wide pullbacks in C, construct finite products in C/B.

theorem category_theory.over.over_has_terminal {C : Type u} (B : C) :

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.)