Cartesian monoidal structure on slices induced by chosen pullbacks

Main declarations

• cartesianMonoidalCategoryOver provides a cartesian monoidal structure on the slice categories Over X for all objects X : C, induced by chosen pullbacks in the base category C. This is the computable analogue of the noncomputable instance CategoryTheory.Over.cartesianMonoidalCategory.

• For a cartesian monoidal category C, and for any object X of C, toOver X is a functor from C to Over X which maps an object A : C to the projection A ⊗ X ⟶ X in Over X. This is the computable analogue of the functor Over.star.

Main results

• cartesianMonoidalCategoryOver proves that the slices of a category with chosen pullbacks are cartesian monoidal.

• toOverPullbackIsoToOver shows that in a category with chosen pullbacks, for any morphism f : Y ⟶ X, the functors toOver X ⋙ pullback f and toOver Y are naturally isomorphic.

• toOverIteratedSliceForwardIsoPullback shows that in a category with chosen pullbacks the functor pullback f : Over X ⥤ Over Y is naturally isomorphic to toOver (Over.mk f) : Over X ⥤ Over (Over.mk f) post-composed with the iterated slice equivalence Over (Over.mk f) ⥤ Over Y. Note that the functor toOver (Over.mk f) exists by the result cartesianMonoidalCategoryOver.

TODO

• Show that the functors pullback f are monoidal with respect to the cartesian monoidal structures on slices.

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacksAlong.binaryFan {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (Y Z : Over X) [ChosenPullbacksAlong Z.hom] : Limits.BinaryFan Y Z

The binary fan provided by fst' and snd'.

def CategoryTheory.ChosenPullbacksAlong.binaryFanIsBinaryProduct {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (Y Z : Over X) [ChosenPullbacksAlong Z.hom] : Limits.IsLimit (binaryFan Y Z)

The binary fan provided by fst' and snd' is a binary product in Over X.

def CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] (X : C) : CartesianMonoidalCategory (Over X)

A computable instance of CartesianMonoidalCategory for Over X when C has chosen pullbacks. Contrast this with the noncomputable instance provided by CategoryTheory.Over.cartesianMonoidalCategory.

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_ext {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X A : C} {Y Z : Over X} (f₁ f₂ : A ⟶ (MonoidalCategoryStruct.tensorObj Y Z).left) (e₁ : CategoryStruct.comp f₁ (fst Y.hom Z.hom) = CategoryStruct.comp f₂ (fst Y.hom Z.hom)) (e₂ : CategoryStruct.comp f₁ (snd Y.hom Z.hom) = CategoryStruct.comp f₂ (snd Y.hom Z.hom)) : f₁ = f₂

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X A : C} {Y Z : Over X} {f₁ f₂ : A ⟶ (MonoidalCategoryStruct.tensorObj Y Z).left} : f₁ = f₂ ↔ CategoryStruct.comp f₁ (fst Y.hom Z.hom) = CategoryStruct.comp f₂ (fst Y.hom Z.hom) ∧ CategoryStruct.comp f₁ (snd Y.hom Z.hom) = CategoryStruct.comp f₂ (snd Y.hom Z.hom)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y Z : Over X) : (MonoidalCategoryStruct.tensorObj Y Z).left = pullbackObj Y.hom Z.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_hom {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y Z : Over X) : (MonoidalCategoryStruct.tensorObj Y Z).hom = CategoryStruct.comp (snd Y.hom Z.hom) Z.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} : (MonoidalCategoryStruct.tensorUnit (Over X)).left = X

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_hom {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} : (MonoidalCategoryStruct.tensorUnit (Over X)).hom = CategoryStruct.id X

theorem CategoryTheory.ChosenPullbacksAlong.Over.fst_eq_fst' {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y Z : Over X) : SemiCartesianMonoidalCategory.fst Y Z = fst' Y.hom Z.hom

theorem CategoryTheory.ChosenPullbacksAlong.Over.snd_eq_snd' {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y Z : Over X) : SemiCartesianMonoidalCategory.snd Y Z = snd' Y.hom Z.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.lift_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {W Y Z : Over X} (f : W ⟶ Y) (g : W ⟶ Z) : (CartesianMonoidalCategory.lift f g).left = lift f.left g.left ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.toUnit_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {Z : Over X} : (SemiCartesianMonoidalCategory.toUnit Z).left = Z.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (fst R.hom (CategoryStruct.comp (snd S.hom T.hom) T.hom)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (fst R.hom S.hom)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : R.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (fst R.hom (CategoryStruct.comp (snd S.hom T.hom) T.hom)) h) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (CategoryStruct.comp (fst R.hom S.hom) h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (snd R.hom (CategoryStruct.comp (snd S.hom T.hom) T.hom)) (fst S.hom T.hom)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (snd R.hom S.hom)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : S.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (snd R.hom (CategoryStruct.comp (snd S.hom T.hom) T.hom)) (CategoryStruct.comp (fst S.hom T.hom) h)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (CategoryStruct.comp (snd R.hom S.hom) h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (snd R.hom (CategoryStruct.comp (snd S.hom T.hom) T.hom)) (snd S.hom T.hom)) = snd (MonoidalCategoryStruct.tensorObj R S).hom T.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : T.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (snd R.hom (CategoryStruct.comp (snd S.hom T.hom) T.hom)) (CategoryStruct.comp (snd S.hom T.hom) h)) = CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorObj R S).hom T.hom) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (fst (CategoryStruct.comp (snd R.hom S.hom) S.hom) T.hom) (fst R.hom S.hom)) = fst R.hom (MonoidalCategoryStruct.tensorObj S T).hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : R.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (fst (CategoryStruct.comp (snd R.hom S.hom) S.hom) T.hom) (CategoryStruct.comp (fst R.hom S.hom) h)) = CategoryStruct.comp (fst R.hom (MonoidalCategoryStruct.tensorObj S T).hom) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (fst (CategoryStruct.comp (snd R.hom S.hom) S.hom) T.hom) (snd R.hom S.hom)) = CategoryStruct.comp (snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (fst S.hom T.hom)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : S.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (fst (CategoryStruct.comp (snd R.hom S.hom) S.hom) T.hom) (CategoryStruct.comp (snd R.hom S.hom) h)) = CategoryStruct.comp (snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (CategoryStruct.comp (fst S.hom T.hom) h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (snd (CategoryStruct.comp (snd R.hom S.hom) S.hom) T.hom) = CategoryStruct.comp (snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (snd S.hom T.hom)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : T.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (snd (CategoryStruct.comp (snd R.hom S.hom) S.hom) T.hom) h) = CategoryStruct.comp (snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (CategoryStruct.comp (snd S.hom T.hom) h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_hom_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Z : Over X) : (MonoidalCategoryStruct.leftUnitor Z).hom.left = snd (MonoidalCategoryStruct.tensorUnit (Over X)).hom Z.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Z : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).inv.left (fst (CategoryStruct.id X) Z.hom) = Z.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Z : Over X) {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).inv.left (CategoryStruct.comp (fst (CategoryStruct.id X) Z.hom) h) = CategoryStruct.comp Z.hom h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (snd (CategoryStruct.id X) Y.hom) = CategoryStruct.id Y.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) {Z : C} (h : Y.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (CategoryStruct.comp (snd (CategoryStruct.id X) Y.hom) h) = h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_hom_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) : (MonoidalCategoryStruct.rightUnitor Y).hom.left = fst Y.hom (CategoryStruct.id X)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (fst Y.hom (CategoryStruct.id X)) = CategoryStruct.id Y.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) {Z : C} (h : Y.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (CategoryStruct.comp (fst Y.hom (CategoryStruct.id X)) h) = h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (snd Y.hom (CategoryStruct.id X)) = Y.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} (Y : Over X) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (CategoryStruct.comp (snd Y.hom (CategoryStruct.id X)) h) = CategoryStruct.comp Y.hom h

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) : (MonoidalCategoryStruct.whiskerLeft R f).left = pullbackMap R.hom T.hom R.hom S.hom (CategoryStruct.id ((Functor.id C).obj R.left)) f.left (CategoryStruct.id ((Functor.fromPUnit X).obj R.right)) ⋯ ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (fst R.hom T.hom) = fst R.hom S.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (CategoryStruct.comp (fst R.hom T.hom) h) = CategoryStruct.comp (fst R.hom S.hom) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (snd R.hom T.hom) = CategoryStruct.comp (snd R.hom S.hom) f.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (CategoryStruct.comp (snd R.hom T.hom) h) = CategoryStruct.comp (snd R.hom S.hom) (CategoryStruct.comp f.left h)

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) : (MonoidalCategoryStruct.whiskerRight f R).left = pullbackMap T.hom R.hom S.hom R.hom f.left (CategoryStruct.id ((Functor.id C).obj R.left)) (CategoryStruct.id ((Functor.fromPUnit X).obj S.right)) ⋯ ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (fst T.hom R.hom) = CategoryStruct.comp (fst S.hom R.hom) f.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (CategoryStruct.comp (fst T.hom R.hom) h) = CategoryStruct.comp (fst S.hom R.hom) (CategoryStruct.comp f.left h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (snd T.hom R.hom) = snd S.hom R.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (CategoryStruct.comp (snd T.hom R.hom) h) = CategoryStruct.comp (snd S.hom R.hom) h

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) : (MonoidalCategoryStruct.tensorHom f g).left = pullbackMap S.hom U.hom R.hom T.hom f.left g.left (CategoryStruct.id ((Functor.fromPUnit X).obj R.right)) ⋯ ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (fst S.hom U.hom) = CategoryStruct.comp (fst R.hom T.hom) f.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) {Z : C} (h : S.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (CategoryStruct.comp (fst S.hom U.hom) h) = CategoryStruct.comp (fst R.hom T.hom) (CategoryStruct.comp f.left h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (snd S.hom U.hom) = CategoryStruct.comp (snd R.hom T.hom) g.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) {Z : C} (h : U.left ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (CategoryStruct.comp (snd S.hom U.hom) h) = CategoryStruct.comp (snd R.hom T.hom) (CategoryStruct.comp g.left h)

def CategoryTheory.toOver {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : Functor C (Over X)

The functor which maps an object A in C to the projection A ⊗ X ⟶ X in Over X. This is the computable analogue of the functor Over.star.

@[simp]

theorem CategoryTheory.toOver_obj_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X A : C) : ((toOver X).obj A).hom = SemiCartesianMonoidalCategory.snd A X

@[simp]

theorem CategoryTheory.toOver_map_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((toOver X).map f).left = MonoidalCategoryStruct.whiskerRight f X

@[simp]

theorem CategoryTheory.toOver_obj_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X A : C) : ((toOver X).obj A).left = MonoidalCategoryStruct.tensorObj A X

@[simp]

theorem CategoryTheory.toOver_map {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X A A' : C} (f : A ⟶ A') : (toOver X).map f = Over.homMk (MonoidalCategoryStruct.whiskerRight f X) ⋯

def CategoryTheory.toOverUnit (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : Functor C (Over (MonoidalCategoryStruct.tensorUnit C))

The functor from C to Over (𝟙_ C) which sends X : C to Over.mk <| toUnit X.

@[simp]

theorem CategoryTheory.toOverUnit_obj_hom (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : ((toOverUnit C).obj X).hom = SemiCartesianMonoidalCategory.toUnit X

@[simp]

theorem CategoryTheory.toOverUnit_obj_left (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : ((toOverUnit C).obj X).left = X

@[simp]

theorem CategoryTheory.toOverUnit_map_left (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((toOverUnit C).map f).left = f

def CategoryTheory.equivToOverUnit (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : Over (MonoidalCategoryStruct.tensorUnit C) ≌ C

The slice category over the terminal unit object is equivalent to the original category.

@[simp]

theorem CategoryTheory.equivToOverUnit_inverse (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : (equivToOverUnit C).inverse = toOverUnit C

@[simp]

theorem CategoryTheory.equivToOverUnit_functor (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : (equivToOverUnit C).functor = Over.forget (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.equivToOverUnit_unitIso (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : (equivToOverUnit C).unitIso = NatIso.ofComponents (fun (X : Over (MonoidalCategoryStruct.tensorUnit C)) => Over.isoMk (Iso.refl ((Functor.id (Over (MonoidalCategoryStruct.tensorUnit C))).obj X).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.equivToOverUnit_counitIso (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : (equivToOverUnit C).counitIso = NatIso.ofComponents (fun (X : C) => Iso.refl (((toOverUnit C).comp (Over.forget (MonoidalCategoryStruct.tensorUnit C))).obj X)) ⋯

def CategoryTheory.toOverUnitPullback {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : (toOverUnit C).comp (ChosenPullbacksAlong.pullback (SemiCartesianMonoidalCategory.toUnit X)) ≅ toOver X

The isomorphism of functors toOverUnit C ⋙ ChosenPullbacksAlong.pullback (toUnit X) and toOver X.

@[simp]

theorem CategoryTheory.toOverUnitPullback_hom_app_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X X✝ : C) : ((toOverUnitPullback X).hom.app X✝).left = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝ X)

@[simp]

theorem CategoryTheory.toOverUnitPullback_inv_app_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X X✝ : C) : ((toOverUnitPullback X).inv.app X✝).left = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝ X)

def CategoryTheory.forgetAdjToOver {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : Over.forget X ⊣ toOver X

The functor toOver X is the right adjoint to the functor Over.forget X.

@[simp]

theorem CategoryTheory.forgetAdjToOver_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Z : C) : (forgetAdjToOver X).counit.app Z = SemiCartesianMonoidalCategory.fst Z X

@[simp]

theorem CategoryTheory.forgetAdjToOver_unit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) (Z : Over X) : (forgetAdjToOver X).unit.app Z = Over.homMk (CartesianMonoidalCategory.lift (CategoryStruct.id Z.left) Z.hom) ⋯

theorem CategoryTheory.forgetAdjToOver.homEquiv_symm {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (Z : Over X) (A : C) (f : Z ⟶ (toOver X).obj A) : ((forgetAdjToOver X).homEquiv Z A).symm f = CategoryStruct.comp f.left (SemiCartesianMonoidalCategory.fst A X)

def CategoryTheory.toOverIsoToOverUnit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : toOver (MonoidalCategoryStruct.tensorUnit C) ≅ toOverUnit C

The isomorphism of functors toOver (𝟙_ C) and toOverUnit C.

@[simp]

theorem CategoryTheory.toOverIsoToOverUnit_inv_app_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : (toOverIsoToOverUnit.inv.app X).left = CategoryStruct.comp ((equivToOverUnit C).counit.app X) (MonoidalCategoryStruct.rightUnitor X).inv

@[simp]

theorem CategoryTheory.toOverIsoToOverUnit_hom_app_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) : (toOverIsoToOverUnit.hom.app X).left = CategoryStruct.comp ((equivToOverUnit C).unit.app ((toOver (MonoidalCategoryStruct.tensorUnit C)).obj X)).left (SemiCartesianMonoidalCategory.fst X (MonoidalCategoryStruct.tensorUnit C))

def CategoryTheory.toOverPullbackIsoToOver {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X Y : C} (f : Y ⟶ X) [ChosenPullbacksAlong f] : (toOver X).comp (ChosenPullbacksAlong.pullback f) ≅ toOver Y

A natural isomorphism between the functors toOver Y and toOver X ⋙ pullback f for any morphism f : X ⟶ Y.

@[simp]

theorem CategoryTheory.toOverPullbackIsoToOver_hom_app_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X Y : C} (f : Y ⟶ X) [ChosenPullbacksAlong f] (X✝ : C) : ((toOverPullbackIsoToOver f).hom.app X✝).left = CartesianMonoidalCategory.lift (CategoryStruct.comp ((Over.mapForget f).hom.app ((ChosenPullbacksAlong.pullback f).obj ((toOver X).obj X✝))) (CategoryStruct.comp ((ChosenPullbacksAlong.mapPullbackAdj f).counit.app ((toOver X).obj X✝)).left (SemiCartesianMonoidalCategory.fst X✝ X))) ((ChosenPullbacksAlong.pullback f).obj ((toOver X).obj X✝)).hom

@[simp]

theorem CategoryTheory.toOverPullbackIsoToOver_inv_app_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X Y : C} (f : Y ⟶ X) [ChosenPullbacksAlong f] (X✝ : C) : ((toOverPullbackIsoToOver f).inv.app X✝).left = CategoryStruct.comp ((ChosenPullbacksAlong.mapPullbackAdj f).unit.app ((toOver Y).obj X✝)).left (CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map (Over.homMk (CartesianMonoidalCategory.lift (CategoryStruct.id (MonoidalCategoryStruct.tensorObj X✝ Y)) (CategoryStruct.comp (SemiCartesianMonoidalCategory.snd X✝ Y) f)) ⋯)).left (CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map (Over.homMk (MonoidalCategoryStruct.whiskerRight ((Over.mapForget f).inv.app ((toOver Y).obj X✝)) X) ⋯)).left ((ChosenPullbacksAlong.pullback f).map (Over.homMk (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.fst X✝ Y) X) ⋯)).left))

def CategoryTheory.toOverIteratedSliceForwardIsoPullback {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X Y : C} (f : Y ⟶ X) : (toOver (Over.mk f)).comp (Over.mk f).iteratedSliceForward ≅ ChosenPullbacksAlong.pullback f

The functor pullback f : Over X ⥤ Over Y is naturally isomorphic to toOver : Over X ⥤ Over (Over.mk f) post-composed with the iterated slice equivalence Over (Over.mk f) ⥤ Over Y.

@[simp]

theorem CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X Y : C} (f : Y ⟶ X) (X✝ : Over X) : ((toOverIteratedSliceForwardIsoPullback f).hom.app X✝).left = CategoryStruct.comp ((ChosenPullbacksAlong.mapPullbackAdj f).unit.app (Over.mk (SemiCartesianMonoidalCategory.snd X✝ (Over.mk f)).left)).left (CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map ((Over.mk f).iteratedSliceEquiv.unitInv.app ((toOver (Over.mk f)).obj X✝)).left).left ((ChosenPullbacksAlong.pullback f).map (SemiCartesianMonoidalCategory.fst X✝ (Over.mk f))).left)

@[simp]

theorem CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] {X Y : C} (f : Y ⟶ X) (X✝ : Over X) : ((toOverIteratedSliceForwardIsoPullback f).inv.app X✝).left = CategoryStruct.comp ((Over.mk f).iteratedSliceEquiv.counitInv.app ((ChosenPullbacksAlong.pullback f).obj X✝)).left (CategoryStruct.comp (ChosenPullbacksAlong.lift (CategoryStruct.id ((ChosenPullbacksAlong.pullback f).obj X✝).left) ((ChosenPullbacksAlong.pullback f).obj X✝).hom ⋯) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.id ((Over.map f).obj ((ChosenPullbacksAlong.pullback f).obj X✝))) (Over.mk f)).left (MonoidalCategoryStruct.whiskerRight ((ChosenPullbacksAlong.mapPullbackAdj f).counit.app X✝) (Over.mk f)).left))