CartesianMonoidalCategory for Over X

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

@[reducible, inline]

abbrev CategoryTheory.Over.cartesianMonoidalCategory {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] (X : C) : CartesianMonoidalCategory (Over X)

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

@[reducible, inline]

abbrev CategoryTheory.Over.braidedCategory {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] (X : C) : BraidedCategory (Over X)

Over X is braided w.r.t. the Cartesian monoidal structure given by Limits.pullback.

theorem CategoryTheory.Over.tensorObj_ext {C : Type u_1} [Category.{v_1, 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₂

theorem CategoryTheory.Over.tensorObj_ext_iff {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.tensorObj_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} (R S : Over X) : (MonoidalCategoryStruct.tensorObj R S).left = Limits.pullback R.hom S.hom

@[simp]

theorem CategoryTheory.Over.tensorObj_hom {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.tensorUnit_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} : (MonoidalCategoryStruct.tensorUnit (Over X)).left = X

@[simp]

theorem CategoryTheory.Over.tensorUnit_hom {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} : (MonoidalCategoryStruct.tensorUnit (Over X)).hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Over.lift_left {C : Type u_1} [Category.{v_1, 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 ⋯

@[simp]

theorem CategoryTheory.Over.fst_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} : (SemiCartesianMonoidalCategory.fst R S).left = Limits.pullback.fst R.hom S.hom

@[simp]

theorem CategoryTheory.Over.snd_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} : (SemiCartesianMonoidalCategory.snd R S).left = Limits.pullback.snd R.hom S.hom

@[simp]

theorem CategoryTheory.Over.toUnit_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} {R : Over X} : (SemiCartesianMonoidalCategory.toUnit R).left = R.hom

@[simp]

theorem CategoryTheory.Over.associator_hom_left_fst {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_hom_left_fst_assoc {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_hom_left_snd_fst {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_hom_left_snd_fst_assoc {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_hom_left_snd_snd {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.associator_hom_left_snd_snd_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.associator_inv_left_fst_fst {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.associator_inv_left_fst_fst_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.associator_inv_left_fst_snd {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_inv_left_fst_snd_assoc {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_inv_left_snd {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.associator_inv_left_snd_assoc {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.leftUnitor_hom_left {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.leftUnitor_inv_left_fst {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.leftUnitor_inv_left_fst_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.leftUnitor_inv_left_snd {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.leftUnitor_inv_left_snd_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.rightUnitor_hom_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) : (MonoidalCategoryStruct.rightUnitor Y).hom.left = Limits.pullback.fst Y.hom (CategoryStruct.id X)

@[simp]

theorem CategoryTheory.Over.rightUnitor_inv_left_fst {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.rightUnitor_inv_left_fst_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.rightUnitor_inv_left_snd {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.rightUnitor_inv_left_snd_assoc {C : Type u_1} [Category.{v_1, 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

theorem CategoryTheory.Over.whiskerLeft_left {C : Type u_1} [Category.{v_1, 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)) ⋯ ⋯

@[simp]

theorem CategoryTheory.Over.whiskerLeft_left_fst {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.whiskerLeft_left_fst_assoc {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.whiskerLeft_left_snd {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.whiskerLeft_left_snd_assoc {C : Type u_1} [Category.{v_1, 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)

theorem CategoryTheory.Over.whiskerRight_left {C : Type u_1} [Category.{v_1, 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)) ⋯ ⋯

@[simp]

theorem CategoryTheory.Over.whiskerRight_left_fst {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.whiskerRight_left_fst_assoc {C : Type u_1} [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.Over.whiskerRight_left_snd {C : Type u_1} [Category.{v_1, 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

@[simp]

theorem CategoryTheory.Over.whiskerRight_left_snd_assoc {C : Type u_1} [Category.{v_1, 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

theorem CategoryTheory.Over.tensorHom_left {C : Type u_1} [Category.{v_1, 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)) ⋯ ⋯

@[simp]

theorem CategoryTheory.Over.tensorHom_left_fst {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (Limits.pullback.fst fS fU) = CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) f.left

@[simp]

theorem CategoryTheory.Over.tensorHom_left_fst_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (CategoryStruct.comp (Limits.pullback.fst fS fU) h) = CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) (CategoryStruct.comp f.left h)

@[simp]

theorem CategoryTheory.Over.tensorHom_left_snd {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (Limits.pullback.snd fS fU) = CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) g.left

@[simp]

theorem CategoryTheory.Over.tensorHom_left_snd_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) {Z : C} (h : U ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (CategoryStruct.comp (Limits.pullback.snd fS fU) h) = CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) (CategoryStruct.comp g.left h)

@[simp]

theorem CategoryTheory.Over.braiding_hom_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} : (β_ R S).hom.left = (Limits.pullbackSymmetry R.hom S.hom).hom

@[simp]

theorem CategoryTheory.Over.braiding_inv_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} : (β_ R S).inv.left = (Limits.pullbackSymmetry S.hom R.hom).hom

instance CategoryTheory.Over.instBraidedPullback {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} : (pullback f).Braided

@[simp]

theorem CategoryTheory.Over.η_pullback_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} : (Functor.OplaxMonoidal.η (pullback f)).left = Limits.pullback.snd (CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.Over.ε_pullback_left {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} : (Functor.LaxMonoidal.ε (pullback f)).left = inv (Limits.pullback.snd (CategoryStruct.id X) f)

theorem CategoryTheory.Over.μ_pullback_left_fst_fst {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} (R✝ S : Over X) : CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback f) R✝ S).left (CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R✝ S).hom f) (Limits.pullback.fst R✝.hom S.hom)) = CategoryStruct.comp (Limits.pullback.fst ((pullback f).obj R✝).hom ((pullback f).obj S).hom) (Limits.pullback.fst R✝.hom f)

theorem CategoryTheory.Over.μ_pullback_left_fst_snd {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} (R✝ S : Over X) : CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback f) R✝ S).left (CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R✝ S).hom f) (Limits.pullback.snd R✝.hom S.hom)) = CategoryStruct.comp (Limits.pullback.snd ((pullback f).obj R✝).hom ((pullback f).obj S).hom) (Limits.pullback.fst S.hom f)

theorem CategoryTheory.Over.μ_pullback_left_snd {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} (R✝ S : Over X) : CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback f) R✝ S).left (Limits.pullback.snd (MonoidalCategoryStruct.tensorObj R✝ S).hom f) = CategoryStruct.comp (Limits.pullback.snd ((pullback f).obj R✝).hom ((pullback f).obj S).hom) (Limits.pullback.snd S.hom f)

@[simp]

theorem CategoryTheory.Over.μ_pullback_left_fst_fst' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback f) (mk g₁) (mk g₂)).left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst g₁ g₂) g₁) f) (Limits.pullback.fst g₁ g₂)) = CategoryStruct.comp (Limits.pullback.fst ((pullback f).obj (mk g₁)).hom ((pullback f).obj (mk g₂)).hom) (Limits.pullback.fst (mk g₁).hom f)

@[simp]

theorem CategoryTheory.Over.μ_pullback_left_fst_snd' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback f) (mk g₁) (mk g₂)).left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst g₁ g₂) g₁) f) (Limits.pullback.snd g₁ g₂)) = CategoryStruct.comp (Limits.pullback.snd ((pullback f).obj (mk g₁)).hom ((pullback f).obj (mk g₂)).hom) (Limits.pullback.fst (mk g₂).hom f)

@[simp]

theorem CategoryTheory.Over.μ_pullback_left_snd' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback f) (mk g₁) (mk g₂)).left (Limits.pullback.snd (CategoryStruct.comp (Limits.pullback.fst g₁ g₂) g₁) f) = CategoryStruct.comp (Limits.pullback.snd ((pullback f).obj (mk g₁)).hom ((pullback f).obj (mk g₂)).hom) (Limits.pullback.snd (mk g₂).hom f)

@[simp]

theorem CategoryTheory.Over.preservesTerminalIso_pullback {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {R S : C} (f : R ⟶ S) : CartesianMonoidalCategory.preservesTerminalIso (pullback f) = isoMk (asIso (Limits.pullback.snd (CategoryStruct.id S) f)) ⋯

@[simp]

theorem CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (A B : Over Y) : CategoryStruct.comp (CartesianMonoidalCategory.prodComparisonIso (pullback f) A B).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst A.hom B.hom) A.hom) f) (Limits.pullback.fst A.hom B.hom)) = CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.snd A.hom f) (Limits.pullback.snd B.hom f)) (Limits.pullback.fst A.hom f)

@[simp]

theorem CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : CategoryStruct.comp (CartesianMonoidalCategory.prodComparisonIso (pullback f) (mk gA) (mk gB)).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst gA gB) gA) f) (Limits.pullback.fst gA gB)) = CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.snd gA f) (Limits.pullback.snd gB f)) (Limits.pullback.fst gA f)

@[simp]

theorem CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : CategoryStruct.comp (CartesianMonoidalCategory.prodComparisonIso (pullback f) (mk gA) (mk gB)).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst gA gB) gA) f) (Limits.pullback.snd gA gB)) = CategoryStruct.comp (Limits.pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom) (Limits.pullback.fst (mk gB).hom f)

@[simp]

theorem CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd' {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : CategoryStruct.comp (CartesianMonoidalCategory.prodComparisonIso (pullback f) (mk gA) (mk gB)).inv.left (Limits.pullback.snd (CategoryStruct.comp (Limits.pullback.fst gA gB) gA) f) = CategoryStruct.comp (Limits.pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom) (Limits.pullback.snd (mk gB).hom f)

@[reducible, inline]

abbrev CategoryTheory.Over.monObjMkPullbackSnd {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [MonObj (mk f)] : MonObj (mk (Limits.pullback.snd f g))

The pullback of a monoid object is a monoid object.

theorem CategoryTheory.Over.monObjMkPullbackSnd_mul {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [MonObj (mk f)] : MonObj.mul = CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback g) (mk f) (mk f)) ((pullback g).map MonObj.mul)

theorem CategoryTheory.Over.monObjMkPullbackSnd_one {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [MonObj (mk f)] : MonObj.one = CategoryStruct.comp (Functor.LaxMonoidal.ε (pullback g)) ((pullback g).map MonObj.one)

instance CategoryTheory.Over.isCommMonObj_mk_pullbackSnd {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [MonObj (mk f)] [IsCommMonObj (mk f)] : IsCommMonObj (mk (Limits.pullback.snd f g))

@[reducible, inline]

abbrev CategoryTheory.Over.grpObjMkPullbackSnd {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [GrpObj (mk f)] : GrpObj (mk (Limits.pullback.snd f g))

The pullback of a monoid object is a monoid object.

theorem CategoryTheory.Over.grpObjMkPullbackSnd_mul {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [GrpObj (mk f)] : MonObj.mul = CategoryStruct.comp (Functor.LaxMonoidal.μ (pullback g) (mk f) (mk f)) ((pullback g).map MonObj.mul)

theorem CategoryTheory.Over.grpObjMkPullbackSnd_one {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [GrpObj (mk f)] : MonObj.one = CategoryStruct.comp (Functor.LaxMonoidal.ε (pullback g)) ((pullback g).map MonObj.one)

instance CategoryTheory.Over.isMonHom_pullbackFst_id_right {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} [MonObj (mk f)] : IsMonHom (homMk (Limits.pullback.fst f (CategoryStruct.id X)) ⋯)