# Documentation

Mathlib.CategoryTheory.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_widePullback, which says that if C has J-indexed wide pullbacks, then Over B has J-indexed products.

@[reducible]

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

Instances For
@[simp]
theorem CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt {C : Type u} (B : C) {J : Type w} (c : ) :
= c.pt.left
@[simp]
theorem CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_π_app {C : Type u} (B : C) {J : Type w} (c : ) :
.app X = Option.casesOn X c.pt.hom fun j => (c.app { as := j }).left

(Impl) A preliminary definition to avoid timeouts.

Instances For
@[simp]
theorem CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom {C : Type u} (B : C) {J : Type w} :
∀ {X Y : } (f : X Y), ().hom = f.hom.left
@[simp]

(Impl) A preliminary definition to avoid timeouts.

Instances For
@[simp]
theorem CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app {C : Type u} (B : C) {J : Type w} :
∀ (x : ), ().π.app x = match x with | { as := j } => CategoryTheory.Over.homMk (c.app (some j))
@[simp]
@[simp]
theorem CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom {C : Type u} (B : C) {J : Type w} :
∀ {X Y : } (f : X Y), ().hom =

(Impl) A preliminary definition to avoid timeouts.

Instances For

(Impl) A preliminary definition to avoid timeouts.

Instances For

(Impl) A preliminary definition to avoid timeouts.

Instances For

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

Instances For

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 CategoryTheory.Over.over_hasTerminal {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_widePullback above.)