Documentation

Mathlib.CategoryTheory.Dialectica.Monoidal

The Dialectica category is symmetric monoidal #

We show that the category Dial has a symmetric monoidal category structure.

source
@[simp]
theorem CategoryTheory.Dial.tensorObj_rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
(X.tensorObj Y).rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj X.rel ⊓ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj Y.rel
source
@[simp]
theorem CategoryTheory.Dial.tensorObj_tgt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
(X.tensorObj Y).tgt = (X.tgt ⨯ Y.tgt)
source
@[simp]
theorem CategoryTheory.Dial.tensorObj_src {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
(X.tensorObj Y).src = (X.src ⨯ Y.src)
source
def CategoryTheory.Dial.tensorObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
CategoryTheory.Dial C

The object X ⊗ Y in the Dial C category just tuples the left and right components.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Dial.tensorHom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁ : CategoryTheory.Dial C} {X₂ : CategoryTheory.Dial C} {Y₁ : CategoryTheory.Dial C} {Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
    (CategoryTheory.Dial.tensorHom f g).f = CategoryTheory.Limits.prod.map f.f g.f
    source
    @[simp]
    theorem CategoryTheory.Dial.tensorHom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁ : CategoryTheory.Dial C} {X₂ : CategoryTheory.Dial C} {Y₁ : CategoryTheory.Dial C} {Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
    (CategoryTheory.Dial.tensorHom f g).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
    source
    def CategoryTheory.Dial.tensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁ : CategoryTheory.Dial C} {X₂ : CategoryTheory.Dial C} {Y₁ : CategoryTheory.Dial C} {Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
    X₁.tensorObj Y₁ ⟶ X₂.tensorObj Y₂

    The functorial action of X ⊗ Y in Dial C.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Dial.tensorUnit_tgt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] :
      CategoryTheory.Dial.tensorUnit.tgt = ⊤_ C
      source
      @[simp]
      theorem CategoryTheory.Dial.tensorUnit_src {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] :
      CategoryTheory.Dial.tensorUnit.src = ⊤_ C
      source
      @[simp]
      theorem CategoryTheory.Dial.tensorUnit_rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] :
      CategoryTheory.Dial.tensorUnit.rel = ⊤
      source
      def CategoryTheory.Dial.tensorUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] :
      CategoryTheory.Dial C

      The unit for the tensor X ⊗ Y in Dial C.

      Equations
      • CategoryTheory.Dial.tensorUnit = { src := ⊤_ C, tgt := ⊤_ C, rel := ⊤ }
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Dial.leftUnitor_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
        X.leftUnitor.inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
        source
        @[simp]
        theorem CategoryTheory.Dial.leftUnitor_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
        X.leftUnitor.hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt)) CategoryTheory.Limits.prod.snd
        source
        @[simp]
        theorem CategoryTheory.Dial.leftUnitor_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
        X.leftUnitor.hom.f = CategoryTheory.Limits.prod.snd
        source
        @[simp]
        theorem CategoryTheory.Dial.leftUnitor_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
        X.leftUnitor.inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X.src) (CategoryTheory.CategoryStruct.id X.src)
        source
        def CategoryTheory.Dial.leftUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
        CategoryTheory.Dial.tensorUnit.tensorObj X ≅ X

        Left unit cancellation 1 ⊗ X ≅ X in Dial C.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Dial.rightUnitor_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
          X.rightUnitor.hom.F = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))
          source
          @[simp]
          theorem CategoryTheory.Dial.rightUnitor_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
          X.rightUnitor.inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X.src) (CategoryTheory.Limits.terminal.from X.src)
          source
          @[simp]
          theorem CategoryTheory.Dial.rightUnitor_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
          X.rightUnitor.inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
          source
          @[simp]
          theorem CategoryTheory.Dial.rightUnitor_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
          X.rightUnitor.hom.f = CategoryTheory.Limits.prod.fst
          source
          def CategoryTheory.Dial.rightUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
          X.tensorObj CategoryTheory.Dial.tensorUnit ≅ X

          Right unit cancellation X ⊗ 1 ≅ X in Dial C.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Dial.associator_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
            (X.associator Y Z).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
            source
            @[simp]
            theorem CategoryTheory.Dial.associator_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
            (X.associator Y Z).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
            source
            @[simp]
            theorem CategoryTheory.Dial.associator_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
            (X.associator Y Z).hom.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
            source
            @[simp]
            theorem CategoryTheory.Dial.associator_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
            (X.associator Y Z).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
            source
            def CategoryTheory.Dial.associator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
            (X.tensorObj Y).tensorObj Z ≅ X.tensorObj (Y.tensorObj Z)

            The associator for tensor, (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z) in Dial C.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.rightUnitor X).hom.F = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.associator X Y Z).hom.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.rightUnitor X).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerLeft_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              ∀ (x x_1 : CategoryTheory.Dial C) (f : x ⟶ x_1), (CategoryTheory.MonoidalCategory.whiskerLeft X f).f = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X.src) f.f
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorUnit_tgt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              (𝟙_ (CategoryTheory.Dial C)).tgt = ⊤_ C
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.rightUnitor X).hom.f = CategoryTheory.Limits.prod.fst
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerRight_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              ∀ {X₁ X₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Dial C), (CategoryTheory.MonoidalCategory.whiskerRight f Y).f = CategoryTheory.Limits.prod.map f.f (CategoryTheory.CategoryStruct.id Y.src)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorUnit_src {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              (𝟙_ (CategoryTheory.Dial C)).src = ⊤_ C
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorObj_tgt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.tensorObj X Y).tgt = (X.tgt ⨯ Y.tgt)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerRight_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              ∀ {X₁ X₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Dial C), (CategoryTheory.MonoidalCategory.whiskerRight f Y).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerLeft_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              ∀ (x x_1 : CategoryTheory.Dial C) (f : x ⟶ x_1), (CategoryTheory.MonoidalCategory.whiskerLeft X f).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) f.F)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorHom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              ∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (CategoryTheory.MonoidalCategory.tensorHom f g).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorUnit_rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              (𝟙_ (CategoryTheory.Dial C)).rel = ⊤
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.associator X Y Z).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.associator X Y Z).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.associator X Y Z).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.leftUnitor X).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.leftUnitor X).hom.f = CategoryTheory.Limits.prod.snd
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorObj_src {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.tensorObj X Y).src = (X.src ⨯ Y.src)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.leftUnitor X).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt)) CategoryTheory.Limits.prod.snd
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.leftUnitor X).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X.src) (CategoryTheory.CategoryStruct.id X.src)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.rightUnitor X).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X.src) (CategoryTheory.Limits.terminal.from X.src)
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorObj_rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (CategoryTheory.MonoidalCategory.tensorObj X Y).rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj X.rel ⊓ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj Y.rel
              source
              @[simp]
              theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorHom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              ∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (CategoryTheory.MonoidalCategory.tensorHom f g).f = CategoryTheory.Limits.prod.map f.f g.f
              source
              instance CategoryTheory.Dial.instMonoidalCategoryStruct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Dial C)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              theorem CategoryTheory.Dial.tensor_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X₁ : CategoryTheory.Dial C) (X₂ : CategoryTheory.Dial C) :
              CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)
              source
              theorem CategoryTheory.Dial.tensor_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁ : CategoryTheory.Dial C} {Y₁ : CategoryTheory.Dial C} {Z₁ : CategoryTheory.Dial C} {X₂ : CategoryTheory.Dial C} {Y₂ : CategoryTheory.Dial C} {Z₂ : CategoryTheory.Dial C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
              CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom f₁ f₂) (CategoryTheory.Dial.tensorHom g₁ g₂)
              source
              theorem CategoryTheory.Dial.associator_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁ : CategoryTheory.Dial C} {X₂ : CategoryTheory.Dial C} {X₃ : CategoryTheory.Dial C} {Y₁ : CategoryTheory.Dial C} {Y₂ : CategoryTheory.Dial C} {Y₃ : CategoryTheory.Dial C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (CategoryTheory.Dial.tensorHom f₁ f₂) f₃) (Y₁.associator Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (X₁.associator X₂ X₃).hom (CategoryTheory.Dial.tensorHom f₁ (CategoryTheory.Dial.tensorHom f₂ f₃))
              source
              theorem CategoryTheory.Dial.leftUnitor_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (f : X ⟶ Y) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Dial C))) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f
              source
              theorem CategoryTheory.Dial.rightUnitor_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (f : X ⟶ Y) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Dial C)))) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f
              source
              theorem CategoryTheory.Dial.pentagon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (W : CategoryTheory.Dial C) (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (W.associator X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (W.associator (X.tensorObj Y) Z).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id W) (X.associator Y Z).hom)) = CategoryTheory.CategoryStruct.comp ((W.tensorObj X).associator Y Z).hom (W.associator X (Y.tensorObj Z)).hom
              source
              theorem CategoryTheory.Dial.triangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              CategoryTheory.CategoryStruct.comp (X.associator (𝟙_ (CategoryTheory.Dial C)) Y).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id X) Y.leftUnitor.hom) = CategoryTheory.Dial.tensorHom X.rightUnitor.hom (CategoryTheory.CategoryStruct.id Y)
              source
              instance CategoryTheory.Dial.instMonoidalCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
              CategoryTheory.MonoidalCategory (CategoryTheory.Dial C)
              Equations
              source
              @[simp]
              theorem CategoryTheory.Dial.braiding_inv_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (X.braiding Y).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
              source
              @[simp]
              theorem CategoryTheory.Dial.braiding_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (X.braiding Y).inv.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
              source
              @[simp]
              theorem CategoryTheory.Dial.braiding_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (X.braiding Y).hom.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
              source
              @[simp]
              theorem CategoryTheory.Dial.braiding_hom_F {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              (X.braiding Y).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
              source
              def CategoryTheory.Dial.braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
              X.tensorObj Y ≅ Y.tensorObj X

              The braiding isomorphism X ⊗ Y ≅ Y ⊗ X in Dial C.

              Equations
              Instances For
                source
                theorem CategoryTheory.Dial.symmetry {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) :
                CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (Y.braiding X).hom = CategoryTheory.CategoryStruct.id (X.tensorObj Y)
                source
                theorem CategoryTheory.Dial.braiding_naturality_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) {Y : CategoryTheory.Dial C} {Z : CategoryTheory.Dial C} (f : Y ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id X) f) (X.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (CategoryTheory.Dial.tensorHom f (CategoryTheory.CategoryStruct.id X))
                source
                theorem CategoryTheory.Dial.braiding_naturality_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X : CategoryTheory.Dial C} {Y : CategoryTheory.Dial C} (f : X ⟶ Y) (Z : CategoryTheory.Dial C) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (Y.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Z).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id Z) f)
                source
                theorem CategoryTheory.Dial.hexagon_forward {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
                CategoryTheory.CategoryStruct.comp (X.associator Y Z).hom (CategoryTheory.CategoryStruct.comp (X.braiding (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (Y.associator Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (X.braiding Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (Y.associator X Z).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id Y) (X.braiding Z).hom))
                source
                theorem CategoryTheory.Dial.hexagon_reverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) (Y : CategoryTheory.Dial C) (Z : CategoryTheory.Dial C) :
                CategoryTheory.CategoryStruct.comp (X.associator Y Z).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorObj X Y).braiding Z).hom (Z.associator X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id X) (Y.braiding Z).hom) (CategoryTheory.CategoryStruct.comp (X.associator Z Y).inv (CategoryTheory.Dial.tensorHom (X.braiding Z).hom (CategoryTheory.CategoryStruct.id Y)))
                source
                instance CategoryTheory.Dial.instSymmetricCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] :
                CategoryTheory.SymmetricCategory (CategoryTheory.Dial C)
                Equations