Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Over

CartesianMonoidalCategory for Over X #

We provide a CartesianMonoidalCategory (Over X) instance via pullbacks, and provide simp lemmas for the induced MonoidalCategory (Over X) instance.

source
@[reducible, inline]
noncomputable abbrev CategoryTheory.Over.cartesianMonoidalCategory {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (X : C) :
CartesianMonoidalCategory (Over X)

A choice of finite products of Over X given by Limits.pullback.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[deprecated CategoryTheory.Over.cartesianMonoidalCategory (since := "2025-05-15")]
    def CategoryTheory.Over.chosenFiniteProducts {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (X : C) :
    CartesianMonoidalCategory (Over X)

    Alias of CategoryTheory.Over.cartesianMonoidalCategory.

    A choice of finite products of Over X given by Limits.pullback.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev CategoryTheory.Over.braidedCategory {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (X : C) :
      BraidedCategory (Over X)

      Over X is braided wrt the cartesian monoidal structure given by Limits.pullback.

      Equations
      Instances For
        source
        theorem CategoryTheory.Over.tensorObj_ext {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X R : C} {S T : Over X} (f₁ f₂ : R ⟶ (MonoidalCategoryStruct.tensorObj S T).left) (e₁ : CategoryStruct.comp f₁ (Limits.pullback.fst S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.fst S.hom T.hom)) (e₂ : CategoryStruct.comp f₁ (Limits.pullback.snd S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.snd S.hom T.hom)) :
        f₁ = f₂
        source
        theorem CategoryTheory.Over.tensorObj_ext_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X R : C} {S T : Over X} {f₁ f₂ : R ⟶ (MonoidalCategoryStruct.tensorObj S T).left} :
        f₁ = f₂ ↔ CategoryStruct.comp f₁ (Limits.pullback.fst S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.fst S.hom T.hom) ∧ CategoryStruct.comp f₁ (Limits.pullback.snd S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.snd S.hom T.hom)
        source
        @[simp]
        theorem CategoryTheory.Over.tensorObj_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S : Over X) :
        (MonoidalCategoryStruct.tensorObj R S).left = Limits.pullback R.hom S.hom
        source
        @[simp]
        theorem CategoryTheory.Over.tensorObj_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S : Over X) :
        (MonoidalCategoryStruct.tensorObj R S).hom = CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom
        source
        @[simp]
        theorem CategoryTheory.Over.tensorUnit_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} :
        (MonoidalCategoryStruct.tensorUnit (Over X)).left = X
        source
        @[simp]
        theorem CategoryTheory.Over.tensorUnit_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} :
        (MonoidalCategoryStruct.tensorUnit (Over X)).hom = CategoryStruct.id X
        source
        @[simp]
        theorem CategoryTheory.Over.lift_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : R ⟶ S) (g : R ⟶ T) :
        (CartesianMonoidalCategory.lift f g).left = Limits.pullback.lift f.left g.left ⋯
        source
        @[simp]
        theorem CategoryTheory.Over.toUnit_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R : Over X} :
        (CartesianMonoidalCategory.toUnit R).left = R.hom
        source
        @[simp]
        theorem CategoryTheory.Over.associator_hom_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (Limits.pullback.fst R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (Limits.pullback.fst R.hom S.hom)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_hom_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.fst R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) h) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) h)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_hom_left_snd_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (Limits.pullback.fst S.hom T.hom)) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (Limits.pullback.snd R.hom S.hom)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_hom_left_snd_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) h)) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) h)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_hom_left_snd_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (Limits.pullback.snd S.hom T.hom)) = Limits.pullback.snd (MonoidalCategoryStruct.tensorObj R S).hom T.hom
        source
        @[simp]
        theorem CategoryTheory.Over.associator_hom_left_snd_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (CategoryStruct.comp (Limits.pullback.snd S.hom T.hom) h)) = CategoryStruct.comp (Limits.pullback.snd (MonoidalCategoryStruct.tensorObj R S).hom T.hom) h
        source
        @[simp]
        theorem CategoryTheory.Over.associator_inv_left_fst_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (Limits.pullback.fst R.hom S.hom)) = Limits.pullback.fst R.hom (MonoidalCategoryStruct.tensorObj S T).hom
        source
        @[simp]
        theorem CategoryTheory.Over.associator_inv_left_fst_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) h)) = CategoryStruct.comp (Limits.pullback.fst R.hom (MonoidalCategoryStruct.tensorObj S T).hom) h
        source
        @[simp]
        theorem CategoryTheory.Over.associator_inv_left_fst_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (Limits.pullback.snd R.hom S.hom)) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (Limits.pullback.fst S.hom T.hom)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_inv_left_fst_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) h)) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) h)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_inv_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (Limits.pullback.snd (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (Limits.pullback.snd S.hom T.hom)
        source
        @[simp]
        theorem CategoryTheory.Over.associator_inv_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.snd (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) h) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (CategoryStruct.comp (Limits.pullback.snd S.hom T.hom) h)
        source
        @[simp]
        theorem CategoryTheory.Over.leftUnitor_hom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
        (MonoidalCategoryStruct.leftUnitor Y).hom.left = Limits.pullback.snd (MonoidalCategoryStruct.tensorUnit (Over X)).hom Y.hom
        source
        @[simp]
        theorem CategoryTheory.Over.leftUnitor_inv_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (Limits.pullback.fst (CategoryStruct.id X) Y.hom) = Y.hom
        source
        @[simp]
        theorem CategoryTheory.Over.leftUnitor_inv_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : X ⟶ Z) :
        CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.id X) Y.hom) h) = CategoryStruct.comp Y.hom h
        source
        @[simp]
        theorem CategoryTheory.Over.leftUnitor_inv_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (Limits.pullback.snd (CategoryStruct.id X) Y.hom) = CategoryStruct.id Y.left
        source
        @[simp]
        theorem CategoryTheory.Over.leftUnitor_inv_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : Y.left ⟶ Z) :
        CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.snd (CategoryStruct.id X) Y.hom) h) = h
        source
        @[simp]
        theorem CategoryTheory.Over.rightUnitor_hom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
        (MonoidalCategoryStruct.rightUnitor Y).hom.left = Limits.pullback.fst Y.hom (CategoryStruct.id X)
        source
        @[simp]
        theorem CategoryTheory.Over.rightUnitor_inv_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (Limits.pullback.fst Y.hom (CategoryStruct.id X)) = CategoryStruct.id Y.left
        source
        @[simp]
        theorem CategoryTheory.Over.rightUnitor_inv_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : Y.left ⟶ Z) :
        CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.fst Y.hom (CategoryStruct.id X)) h) = h
        source
        @[simp]
        theorem CategoryTheory.Over.rightUnitor_inv_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
        CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (Limits.pullback.snd Y.hom (CategoryStruct.id X)) = Y.hom
        source
        @[simp]
        theorem CategoryTheory.Over.rightUnitor_inv_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : X ⟶ Z) :
        CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.snd Y.hom (CategoryStruct.id X)) h) = CategoryStruct.comp Y.hom h
        source
        theorem CategoryTheory.Over.whiskerLeft_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
        (MonoidalCategoryStruct.whiskerLeft R f).left = Limits.pullback.map R.hom S.hom R.hom T.hom (CategoryStruct.id ((Functor.id C).obj R.left)) f.left (CategoryStruct.id ((Functor.fromPUnit X).obj R.right)) ⋯ ⋯
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerLeft_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
        CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (Limits.pullback.fst R.hom T.hom) = Limits.pullback.fst R.hom S.hom
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerLeft_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.fst R.hom T.hom) h) = CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) h
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerLeft_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
        CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (Limits.pullback.snd R.hom T.hom) = CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) f.left
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerLeft_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.snd R.hom T.hom) h) = CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) (CategoryStruct.comp f.left h)
        source
        theorem CategoryTheory.Over.whiskerRight_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
        (MonoidalCategoryStruct.whiskerRight f R).left = Limits.pullback.map S.hom R.hom T.hom R.hom f.left (CategoryStruct.id ((Functor.id C).obj R.left)) (CategoryStruct.id ((Functor.fromPUnit X).obj S.right)) ⋯ ⋯
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerRight_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
        CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (Limits.pullback.fst T.hom R.hom) = CategoryStruct.comp (Limits.pullback.fst S.hom R.hom) f.left
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerRight_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.fst T.hom R.hom) h) = CategoryStruct.comp (Limits.pullback.fst S.hom R.hom) (CategoryStruct.comp f.left h)
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerRight_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
        CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (Limits.pullback.snd T.hom R.hom) = Limits.pullback.snd S.hom R.hom
        source
        @[simp]
        theorem CategoryTheory.Over.whiskerRight_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.snd T.hom R.hom) h) = CategoryStruct.comp (Limits.pullback.snd S.hom R.hom) h
        source
        theorem CategoryTheory.Over.tensorHom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) :
        (MonoidalCategoryStruct.tensorHom f g).left = Limits.pullback.map R.hom T.hom S.hom U.hom f.left g.left (CategoryStruct.id ((Functor.fromPUnit X).obj R.right)) ⋯ ⋯
        source
        @[simp]
        theorem CategoryTheory.Over.tensorHom_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) :
        CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (Limits.pullback.fst S.hom U.hom) = CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) f.left
        source
        @[simp]
        theorem CategoryTheory.Over.tensorHom_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.fst S.hom U.hom) h) = CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) (CategoryStruct.comp f.left h)
        source
        @[simp]
        theorem CategoryTheory.Over.tensorHom_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) :
        CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (Limits.pullback.snd S.hom U.hom) = CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) g.left
        source
        @[simp]
        theorem CategoryTheory.Over.tensorHom_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks 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 (Limits.pullback.snd S.hom U.hom) h) = CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) (CategoryStruct.comp g.left h)
        source
        @[simp]
        theorem CategoryTheory.Over.braiding_hom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} :
        (β_ R S).hom.left = (Limits.pullbackSymmetry R.hom S.hom).hom
        source
        @[simp]
        theorem CategoryTheory.Over.braiding_inv_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} :
        (β_ R S).inv.left = (Limits.pullbackSymmetry S.hom R.hom).hom