Documentation

Mathlib.CategoryTheory.Monoidal.Arrow

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).

source
@[implicit_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.
Instances For
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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)
    source
    @[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))
    source
    @[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✝²
    source
    @[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 = X □ Y
    source
    @[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
    source
    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₂)
    source
    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₃))
    source
    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
    source
    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
    source
    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
    source
    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
    source
    @[implicit_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.
    Instances For
      source
      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))
      source
      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))
      source
      @[implicit_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.
      Instances For
        source
        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₂
        source
        @[implicit_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
        Instances For
          source
          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
          source
          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
          source
          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
          source
          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
          source
          @[implicit_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.
          Instances For