Monoidal structure on the arrow category of a cartesian closed category.

If C is a braided, cartesian closed category with pushouts and an initial object, then Arrow C has a symmetric monoidal category structure given by the pushout-product (the Leibniz construction given by the tensor product on C).

If C also has pullbacks, then Arrow C has a monoidal closed structure given by the pullback-hom (the Leibniz construction given by the internal hom on C).

@[instance_reducible]

noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instMonoidalCategoryStructArrowOfHasPushoutsOfHasInitialOfMonoidalClosedOfBraidedCategory {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] : MonoidalCategoryStruct (Arrow C)

The monoidal category instance induced by the pushout-product.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorHom_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X₁ Y₁ X₂ Y₂ : Arrow C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorHom f g = CategoryStruct.comp ((fun {X₁ X₂ : Arrow C} (f : X₁ ⟶ X₂) (X : Arrow C) => (pushoutProduct.map f).app X) f X₂) ((fun (X x x_1 : Arrow C) (f : x ⟶ x_1) => (pushoutProduct.obj X).map f) Y₁ X₂ Y₂ g)

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X : Arrow C) : MonoidalCategoryStruct.rightUnitor X = rightUnitor X

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (x✝ x✝¹ x✝² : Arrow C) : MonoidalCategoryStruct.associator x✝ x✝¹ x✝² = associator x✝ x✝¹ x✝²

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorObj_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X Y : Arrow C) : tensorObj X Y = (pushoutProduct.obj X).obj Y

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorUnit_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] : tensorUnit (Arrow C) = Arrow.mk (Limits.initial.to (tensorUnit C))

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X : Arrow C) : MonoidalCategoryStruct.leftUnitor X = leftUnitor X

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRight_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X₁✝ X₂✝ : Arrow C} (f : X₁✝ ⟶ X₂✝) (X : Arrow C) : whiskerRight f X = (pushoutProduct.map f).app X

@[simp]

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeft_def {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X x✝ x✝¹ : Arrow C) (f : x✝ ⟶ x✝¹) : whiskerLeft X f = (pushoutProduct.obj X).map f

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorHom_comp_tensorHom {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_naturality {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor_naturality {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X Y : Arrow C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerLeft (tensorUnit (Arrow C)) f) (MonoidalCategoryStruct.leftUnitor Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom f

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor_naturality {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X Y : Arrow C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerRight f (tensorUnit (Arrow C))) (MonoidalCategoryStruct.rightUnitor Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom f

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.pentagon {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (W X Y Z : Arrow C) : CategoryStruct.comp (whiskerRight (MonoidalCategoryStruct.associator W X Y).hom Z) (CategoryStruct.comp (MonoidalCategoryStruct.associator W (tensorObj X Y) Z).hom (whiskerLeft W (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (tensorObj W X) Y Z).hom (MonoidalCategoryStruct.associator W X (tensorObj Y Z)).hom

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.triangle {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X Y : Arrow C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X (tensorUnit (Arrow C)) Y).hom (whiskerLeft X (MonoidalCategoryStruct.leftUnitor Y).hom) = whiskerRight (MonoidalCategoryStruct.rightUnitor X).hom Y

@[instance_reducible]

noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instArrow {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] : MonoidalCategory (Arrow C)

The monoidal category instance induced by the pushout-product.

Equations

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

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hexagon_forward {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X Y Z : Arrow C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (braiding X (tensorObj Y Z)).hom (MonoidalCategoryStruct.associator Y Z X).hom) = CategoryStruct.comp (whiskerRight (braiding X Y).hom Z) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y X Z).hom (whiskerLeft Y (braiding X Z).hom))

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hexagon_reverse {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X Y Z : Arrow C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (braiding (tensorObj X Y) Z).hom (MonoidalCategoryStruct.associator Z X Y).inv) = CategoryStruct.comp (whiskerLeft X (braiding Y Z).hom) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Z Y).inv (whiskerRight (braiding X Z).hom Y))

@[instance_reducible]

noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braidedCategory {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] : BraidedCategory (Arrow C)

The braided category instance induced by the pushout-product.

Equations

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

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braidedCategory_braiding {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X₁ X₂ : Arrow C) : β_ X₁ X₂ = braiding X₁ X₂

@[instance_reducible]

noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] : SymmetricCategory (Arrow C)

The symmetric category instance induced by the pushout-product.

Equations

• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory = { toBraidedCategory := CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braidedCategory, symmetry := ⋯ }

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_inv_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X₁ X₂ : Arrow C) : (β_ X₁ X₂).inv.right = (β_ X₁.right X₂.right).inv

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_hom_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X₁ X₂ : Arrow C) : (β_ X₁ X₂).hom.left = CategoryStruct.comp (Limits.pushoutSymmetry (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)).hom (Limits.HasColimit.isoOfNatIso (Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).hom

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_inv_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X₁ X₂ : Arrow C) : (β_ X₁ X₂).inv.left = CategoryStruct.comp (Limits.HasColimit.isoOfNatIso (Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).inv (Limits.pushoutSymmetry (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)).inv

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_hom_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X₁ X₂ : Arrow C) : (β_ X₁ X₂).hom.right = (β_ X₁.right X₂.right).hom

@[instance_reducible]

noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instMonoidalClosedArrowOfHasPullbacks {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] [Limits.HasPullbacks C] : MonoidalClosed (Arrow C)

The monoidal closed instance induced by the pushout-product and pullback-hom.

Equations

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