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.

Note that the binary case is done separately to ensure defeqs with the pullback in the base category.

TODO

• Generalise from arbitrary products to arbitrary limits. This is done in Toric.
• Dualise to get the Under X results.

Binary products

In this section we construct binary products in Over X and binary coproducts in Under X explicitly as the pullbacks and pushouts of binary (co)fans in the base category.

For Over X, one could construct these binary products from the general theory of arbitrary products from the next section, i.e.

(Cone.postcomposeEquivalence (diagramIsoCospan _).symm).trans
  (Over.ConstructProducts.conesEquiv _ (pair (Over.mk f) (Over.mk g)))

but this gives worse defeqs.

For Under X, there is currently no general theory of arbitrary coproducts.

def CategoryTheory.Limits.pullbackConeEquivBinaryFan {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : PullbackCone f g ≌ BinaryFan (Over.mk f) (Over.mk g)

Pullback cones to X are the same thing as binary fans in Over X.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) : (pullbackConeEquivBinaryFan.functor.map a).hom = Over.homMk a.hom ⋯

@[simp]

theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} (c : BinaryFan (Over.mk f) (Over.mk g)) : pullbackConeEquivBinaryFan.inverse.obj c = PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯

@[simp]

theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} (c : PullbackCone f g) : pullbackConeEquivBinaryFan.functor.obj c = BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯)

@[simp]

theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) : (pullbackConeEquivBinaryFan.inverse.map a).hom = Over.Hom.left a.hom

@[simp]

theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : pullbackConeEquivBinaryFan.counitIso = NatIso.ofComponents (fun (X_1 : BinaryFan (Over.mk f) (Over.mk g)) => BinaryFan.ext (Over.isoMk (Iso.refl (({ obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) => PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯, map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) => { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : PullbackCone f g) => BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯), map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) => { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj X_1).pt.left) ⋯) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : pullbackConeEquivBinaryFan.unitIso = NatIso.ofComponents (fun (c : PullbackCone f g) => c.eta) ⋯

def CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : PullbackCone f g} (hc : IsLimit c) : IsLimit (pullbackConeEquivBinaryFan.functor.obj c)

A binary fan in Over X is a limit if its corresponding pullback cone to X is a limit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : PullbackCone f g} (hc : IsLimit c) (s : BinaryFan (Over.mk f) (Over.mk g)) : (hc.pullbackConeEquivBinaryFanFunctor.lift s).left = hc.lift (PullbackCone.mk (Over.Hom.left s.fst) (Over.Hom.left s.snd) ⋯)

def CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanInverse {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : BinaryFan (Over.mk f) (Over.mk g)} (hc : IsLimit c) : IsLimit (pullbackConeEquivBinaryFan.inverse.obj c)

A pullback cone to X is a limit if its corresponding binary fan in Over X is a limit.

Equations

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

def CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : PushoutCocone f g ≌ BinaryCofan (Under.mk f) (Under.mk g)

Pushout cocones from X are the same thing as binary cofans in Under X.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : pushoutCoconeEquivBinaryCofan.unitIso = NatIso.ofComponents (fun (c : PushoutCocone f g) => c.eta) ⋯

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) : (pushoutCoconeEquivBinaryCofan.inverse.map a).hom = Under.Hom.right a.hom

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : BinaryCofan (Under.mk f) (Under.mk g)) : pushoutCoconeEquivBinaryCofan.inverse.obj c = PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) : (pushoutCoconeEquivBinaryCofan.functor.map a).hom = Under.homMk a.hom ⋯

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : pushoutCoconeEquivBinaryCofan.functor.obj c = BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯)

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : pushoutCoconeEquivBinaryCofan.counitIso = NatIso.ofComponents (fun (X_1 : BinaryCofan (Under.mk f) (Under.mk g)) => BinaryCofan.ext (Under.isoMk (Iso.refl (({ obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) => PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯, map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) => { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : PushoutCocone f g) => BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯), map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) => { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj X_1).pt.right) ⋯) ⋯ ⋯) ⋯

def CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : PushoutCocone f g} (hc : IsColimit c) : IsColimit (pushoutCoconeEquivBinaryCofan.functor.obj c)

A binary cofan in Under X is a colimit if its corresponding pushout cocone from X is a colimit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : PushoutCocone f g} (hc : IsColimit c) (s : BinaryCofan (Under.mk f) (Under.mk g)) : (hc.pushoutCoconeEquivBinaryCofanFunctor.desc s).right = hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)

def CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanInverse {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : BinaryCofan (Under.mk f) (Under.mk g)} (hc : IsColimit c) : IsColimit (pushoutCoconeEquivBinaryCofan.inverse.obj c)

A pushout cocone from X is a colimit if its corresponding binary cofan in Under X is a colimit.

Equations

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

theorem CategoryTheory.Over.isPullback_of_binaryFan_isLimit {C : Type u} [Category.{v, u} C] {X : C} {Y Z : Over X} (c : Limits.BinaryFan Y Z) (hc : Limits.IsLimit c) : IsPullback (Hom.left c.fst) (Hom.left c.snd) Y.hom Z.hom

noncomputable def CategoryTheory.Over.prodLeftIsoPullback {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] : (Y ⨯ Z).left ≅ Limits.pullback Y.hom Z.hom

The product of Y and Z in Over X is isomorphic to Y ×ₓ Z.

Equations

• Y.prodLeftIsoPullback Z = ⋯.isoPullback

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_hom_fst {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] : CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (Limits.pullback.fst Y.hom Z.hom) = Hom.left Limits.prod.fst

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_hom_fst_assoc {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] {Z✝ : C} (h : Y.left ⟶ Z✝) : CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (CategoryStruct.comp (Limits.pullback.fst Y.hom Z.hom) h) = CategoryStruct.comp (Hom.left Limits.prod.fst) h

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_hom_snd {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] : CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (Limits.pullback.snd Y.hom Z.hom) = Hom.left Limits.prod.snd

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_hom_snd_assoc {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] {Z✝ : C} (h : Z.left ⟶ Z✝) : CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (CategoryStruct.comp (Limits.pullback.snd Y.hom Z.hom) h) = CategoryStruct.comp (Hom.left Limits.prod.snd) h

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_inv_fst {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] : CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv (Hom.left Limits.prod.fst) = Limits.pullback.fst Y.hom Z.hom

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_inv_fst_assoc {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] {Z✝ : C} (h : Y.left ⟶ Z✝) : CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv (CategoryStruct.comp (Hom.left Limits.prod.fst) h) = CategoryStruct.comp (Limits.pullback.fst Y.hom Z.hom) h

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_inv_snd {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] : CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv (Hom.left Limits.prod.snd) = Limits.pullback.snd Y.hom Z.hom

@[simp]

theorem CategoryTheory.Over.prodLeftIsoPullback_inv_snd_assoc {C : Type u} [Category.{v, u} C] {X : C} (Y Z : Over X) [Limits.HasPullback Y.hom Z.hom] [Limits.HasBinaryProduct Y Z] {Z✝ : C} (h : Z.left ⟶ Z✝) : CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv (CategoryStruct.comp (Hom.left Limits.prod.snd) h) = CategoryStruct.comp (Limits.pullback.snd Y.hom Z.hom) h

Arbitrary products

In this section, we prove that J-indexed products in Over X correspond to J-indexed pullbacks in C.

@[reducible, inline]

abbrev CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver {C : Type u} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) : Functor (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.

def CategoryTheory.Over.ConstructProducts.conesEquivInverseObj {C : Type u} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) (c : Limits.Cone F) : Limits.Cone (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.conesEquivInverseObj_pt {C : Type u} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) (c : Limits.Cone F) : (conesEquivInverseObj B F c).pt = c.pt.left

@[simp]

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

def CategoryTheory.Over.ConstructProducts.conesEquivInverse {C : Type u} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) : Functor (Limits.Cone F) (Limits.Cone (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} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) {X✝ Y✝ : Limits.Cone F} (f : X✝ ⟶ Y✝) : ((conesEquivInverse B F).map f).hom = Hom.left f.hom

@[simp]

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Over.ConstructProducts.conesEquivUnitIso {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) : Functor.id (Limits.Cone (widePullbackDiagramOfDiagramOver B F)) ≅ (conesEquivFunctor B F).comp (conesEquivInverse 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.conesEquivUnitIso_hom_app_hom {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) (X : Limits.Cone (widePullbackDiagramOfDiagramOver B F)) : ((conesEquivUnitIso B F).hom.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) (X : Limits.Cone (widePullbackDiagramOfDiagramOver B F)) : ((conesEquivUnitIso B F).inv.app X).hom = CategoryStruct.id X.pt

def CategoryTheory.Over.ConstructProducts.conesEquivCounitIso {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) : (conesEquivInverse B F).comp (conesEquivFunctor B F) ≅ Functor.id (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.conesEquivCounitIso_inv_app_hom_left {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) (X : Limits.Cone F) : ((conesEquivCounitIso B F).inv.app X).hom.left = CategoryStruct.id X.pt.left

@[simp]

theorem CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) (X : Limits.Cone F) : ((conesEquivCounitIso B F).hom.app X).hom.left = CategoryStruct.id X.pt.left

def CategoryTheory.Over.ConstructProducts.conesEquiv {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (F : Functor (Discrete J) (Over B)) : Limits.Cone (widePullbackDiagramOfDiagramOver B F) ≌ 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} (F : Functor (Discrete J) (Over B)) [Limits.HasLimit (widePullbackDiagramOfDiagramOver B F)] : 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} [Category.{v, u} C] [Limits.HasLimitsOfShape (Limits.WidePullbackShape J) C] {B : C} : Limits.HasLimitsOfShape (Discrete J) (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} [Category.{v, u} C] [Limits.HasPullbacks C] {B : C} : Limits.HasBinaryProducts (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} [Category.{v, u} C] [Limits.HasWidePullbacks C] {B : C} : Limits.HasProducts (Over B)

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

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

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

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