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]

def CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).pt = c.pt.left

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Limits.WidePullbackShape J) : (CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).π.app X = Option.casesOn X c.pt.hom fun (j : J) => (c.π.app { as := j }).left

def CategoryTheory.Over.ConstructProducts.conesEquivInverseObj {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)

(Impl) A preliminary definition to avoid timeouts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).map f).hom = f.hom.left

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).obj c = CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c

def CategoryTheory.Over.ConstructProducts.conesEquivInverse {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F))

(Impl) A preliminary definition to avoid timeouts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) : ∀ (x : CategoryTheory.Discrete J), ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).π.app x = match x with | { as := j } => CategoryTheory.Over.homMk (c.π.app (some j)) ⋯

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) : ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).pt = CategoryTheory.Over.mk (c.π.app none)

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : ∀ {X Y : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)} (f : X ⟶ Y), ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).map f).hom = CategoryTheory.Over.homMk f.hom ⋯

def CategoryTheory.Over.ConstructProducts.conesEquivFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) (CategoryTheory.Limits.Cone F)

(Impl) A preliminary definition to avoid timeouts.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Over.ConstructProducts.conesEquivUnitIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) ≅ CategoryTheory.Functor.comp (CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F) (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F)

(Impl) A preliminary definition to avoid timeouts.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Over.ConstructProducts.conesEquivCounitIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor.comp (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F) (CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)

(Impl) A preliminary definition to avoid timeouts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).counitIso = CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquiv_functor {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).functor = CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquiv_inverse {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).inverse = CategoryTheory.Over.ConstructProducts.conesEquivInverse B F

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).unitIso = CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F

def CategoryTheory.Over.ConstructProducts.conesEquiv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F) ≌ CategoryTheory.Limits.Cone F

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)] : CategoryTheory.Limits.HasLimit F

Use the above equivalence to prove we have a limit.

theorem CategoryTheory.Over.ConstructProducts.over_product_of_widePullback {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C] {B : C} : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Over B)

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

theorem CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {B : C} : CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over B)

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

theorem CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePullbacks C] {B : C} : CategoryTheory.Limits.HasProducts (CategoryTheory.Over B)

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

theorem CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {B : C} : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Over B)

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

theorem CategoryTheory.Over.over_hasTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) : CategoryTheory.Limits.HasTerminal (CategoryTheory.Over 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_widePullback above.)