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.

@[implicit_reducible]

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 (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (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 (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (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 (CategoryStruct.comp (snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (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 (CategoryStruct.comp (snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (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 (CategoryStruct.comp (snd R.hom S.hom) 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 (CategoryStruct.comp (fst S.hom R.hom) 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 (CategoryStruct.comp (fst R.hom T.hom) 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 (CategoryStruct.comp (snd R.hom T.hom) 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 (CategoryStruct.id (Over.mk (SemiCartesianMonoidalCategory.snd X✝ (Over.mk f)).left)).left ((CategoryStruct.comp ((((((Over.map f).leftUnitor.symm.homCongr ((Over.mk f).iteratedSliceBackward.comp (Over.forget (Over.mk f))).rightUnitor.symm).trans (TwoSquare.equivNatTrans (Functor.id (Over Y)) ((Over.mk f).iteratedSliceBackward.comp (Over.forget (Over.mk f))) (Over.map f) (Functor.id (Over X))).symm).trans (mateEquiv ((Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp (forgetAdjToOver (Over.mk f))) (ChosenPullbacksAlong.mapPullbackAdj f))).trans (TwoSquare.equivNatTrans ((toOver (Over.mk f)).comp (Over.mk f).iteratedSliceForward) (Functor.id (Over X)) (Functor.id (Over Y)) (ChosenPullbacksAlong.pullback f))) (eqToHom ⋯)) (ChosenPullbacksAlong.pullback f).leftUnitor.hom).app X✝).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 (CategoryStruct.id ((ChosenPullbacksAlong.pullback f).obj X✝)).left ((CategoryStruct.comp (((((((Over.mk f).iteratedSliceBackward.comp (Over.forget (Over.mk f))).leftUnitor.symm.homCongr (Over.map f).rightUnitor.symm).trans (TwoSquare.equivNatTrans (Functor.id (Over Y)) (Over.map f) ((Over.mk f).iteratedSliceBackward.comp (Over.forget (Over.mk f))) (Functor.id (Over X))).symm).trans (mateEquiv (ChosenPullbacksAlong.mapPullbackAdj f) ((Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp (forgetAdjToOver (Over.mk f))))).trans (TwoSquare.equivNatTrans (ChosenPullbacksAlong.pullback f) (Functor.id (Over X)) (Functor.id (Over Y)) ((toOver (Over.mk f)).comp (Over.mk f).iteratedSliceForward))) (eqToHom ⋯)) ((toOver (Over.mk f)).comp (Over.mk f).iteratedSliceForward).leftUnitor.hom).app X✝).left