The Dialectica category is symmetric monoidal

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

def CategoryTheory.Dial.tensorObj {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : 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.

@[simp]

theorem CategoryTheory.Dial.tensorObj_rel {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.tensorObj Y).rel = (Subobject.pullback (Limits.prod.map Limits.prod.fst Limits.prod.fst)).obj X.rel ⊓ (Subobject.pullback (Limits.prod.map Limits.prod.snd Limits.prod.snd)).obj Y.rel

@[simp]

theorem CategoryTheory.Dial.tensorObj_tgt {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.tensorObj Y).tgt = (X.tgt ⨯ Y.tgt)

@[simp]

theorem CategoryTheory.Dial.tensorObj_src {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.tensorObj Y).src = (X.src ⨯ Y.src)

def CategoryTheory.Dial.tensorHom {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁ X₂ Y₁ Y₂ : 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.

@[simp]

theorem CategoryTheory.Dial.tensorHom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁ X₂ Y₁ Y₂ : Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (tensorHom f g).f = Limits.prod.map f.f g.f

@[simp]

theorem CategoryTheory.Dial.tensorHom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁ X₂ Y₁ Y₂ : Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (tensorHom f g).F = Limits.prod.lift (CategoryStruct.comp (Limits.prod.map Limits.prod.fst Limits.prod.fst) f.F) (CategoryStruct.comp (Limits.prod.map Limits.prod.snd Limits.prod.snd) g.F)

def CategoryTheory.Dial.tensorUnit {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] : Dial C

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

Equations

• CategoryTheory.Dial.tensorUnit = { src := ⊤_ C, tgt := ⊤_ C, rel := ⊤ }

@[simp]

theorem CategoryTheory.Dial.tensorUnit_tgt {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] : tensorUnit.tgt = ⊤_ C

@[simp]

theorem CategoryTheory.Dial.tensorUnit_src {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] : tensorUnit.src = ⊤_ C

@[simp]

theorem CategoryTheory.Dial.tensorUnit_rel {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] : tensorUnit.rel = ⊤

def CategoryTheory.Dial.leftUnitor {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : tensorUnit.tensorObj X ≅ X

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

Equations

• X.leftUnitor = CategoryTheory.Dial.isoMk (CategoryTheory.Limits.prod.leftUnitor X.src) (CategoryTheory.Limits.prod.leftUnitor X.tgt) ⋯

@[simp]

theorem CategoryTheory.Dial.leftUnitor_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.leftUnitor.inv.f = Limits.prod.lift (Limits.terminal.from X.src) (CategoryStruct.id X.src)

@[simp]

theorem CategoryTheory.Dial.leftUnitor_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.leftUnitor.inv.F = CategoryStruct.comp Limits.prod.snd Limits.prod.snd

@[simp]

theorem CategoryTheory.Dial.leftUnitor_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.leftUnitor.hom.f = Limits.prod.snd

@[simp]

theorem CategoryTheory.Dial.leftUnitor_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.leftUnitor.hom.F = Limits.prod.lift (Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt)) Limits.prod.snd

def CategoryTheory.Dial.rightUnitor {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.tensorObj tensorUnit ≅ X

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

Equations

• X.rightUnitor = CategoryTheory.Dial.isoMk (CategoryTheory.Limits.prod.rightUnitor X.src) (CategoryTheory.Limits.prod.rightUnitor X.tgt) ⋯

@[simp]

theorem CategoryTheory.Dial.rightUnitor_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.rightUnitor.hom.F = Limits.prod.lift Limits.prod.snd (Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))

@[simp]

theorem CategoryTheory.Dial.rightUnitor_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.rightUnitor.hom.f = Limits.prod.fst

@[simp]

theorem CategoryTheory.Dial.rightUnitor_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.rightUnitor.inv.F = CategoryStruct.comp Limits.prod.snd Limits.prod.fst

@[simp]

theorem CategoryTheory.Dial.rightUnitor_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.rightUnitor.inv.f = Limits.prod.lift (CategoryStruct.id X.src) (Limits.terminal.from X.src)

def CategoryTheory.Dial.associator {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : 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

• X.associator Y Z = CategoryTheory.Dial.isoMk (CategoryTheory.Limits.prod.associator X.src Y.src Z.src) (CategoryTheory.Limits.prod.associator X.tgt Y.tgt Z.tgt) ⋯

@[simp]

theorem CategoryTheory.Dial.associator_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associator Y Z).hom.F = Limits.prod.lift (Limits.prod.lift (CategoryStruct.comp Limits.prod.snd Limits.prod.fst) (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.snd Limits.prod.fst))) (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.snd Limits.prod.snd))

@[simp]

theorem CategoryTheory.Dial.associator_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associator Y Z).inv.F = Limits.prod.lift (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.fst Limits.prod.fst)) (Limits.prod.lift (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.fst Limits.prod.snd)) (CategoryStruct.comp Limits.prod.snd Limits.prod.snd))

@[simp]

theorem CategoryTheory.Dial.associator_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associator Y Z).inv.f = Limits.prod.lift (Limits.prod.lift Limits.prod.fst (CategoryStruct.comp Limits.prod.snd Limits.prod.fst)) (CategoryStruct.comp Limits.prod.snd Limits.prod.snd)

@[simp]

theorem CategoryTheory.Dial.associator_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associator Y Z).hom.f = Limits.prod.lift (CategoryStruct.comp Limits.prod.fst Limits.prod.fst) (Limits.prod.lift (CategoryStruct.comp Limits.prod.fst Limits.prod.snd) Limits.prod.snd)

instance CategoryTheory.Dial.instMonoidalCategoryStruct {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : MonoidalCategoryStruct (Dial C)

Equations

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

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.rightUnitor X).hom.f = Limits.prod.fst

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorUnit_tgt {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : (𝟙_ (Dial C)).tgt = ⊤_ C

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.leftUnitor X).inv.F = CategoryStruct.comp Limits.prod.snd Limits.prod.snd

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.rightUnitor X).hom.F = Limits.prod.lift Limits.prod.snd (Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (MonoidalCategoryStruct.associator X Y Z).hom.f = Limits.prod.lift (CategoryStruct.comp Limits.prod.fst Limits.prod.fst) (Limits.prod.lift (CategoryStruct.comp Limits.prod.fst Limits.prod.snd) Limits.prod.snd)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.rightUnitor X).inv.f = Limits.prod.lift (CategoryStruct.id X.src) (Limits.terminal.from X.src)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.leftUnitor X).hom.f = Limits.prod.snd

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerRight_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁✝ X₂✝ : Dial C} (f : X₁✝ ⟶ X₂✝) (Y : Dial C) : (MonoidalCategoryStruct.whiskerRight f Y).F = Limits.prod.lift (CategoryStruct.comp (Limits.prod.map Limits.prod.fst Limits.prod.fst) f.F) (CategoryStruct.comp Limits.prod.snd Limits.prod.snd)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorObj_tgt {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (MonoidalCategoryStruct.tensorObj X Y).tgt = (X.tgt ⨯ Y.tgt)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.leftUnitor X).inv.f = Limits.prod.lift (Limits.terminal.from X.src) (CategoryStruct.id X.src)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorHom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Dial C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (MonoidalCategoryStruct.tensorHom f g).F = Limits.prod.lift (CategoryStruct.comp (Limits.prod.map Limits.prod.fst Limits.prod.fst) f.F) (CategoryStruct.comp (Limits.prod.map Limits.prod.snd Limits.prod.snd) g.F)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerLeft_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X x✝ x✝¹ : Dial C) (f : x✝ ⟶ x✝¹) : (MonoidalCategoryStruct.whiskerLeft X f).F = Limits.prod.lift (CategoryStruct.comp Limits.prod.snd Limits.prod.fst) (CategoryStruct.comp (Limits.prod.map Limits.prod.snd Limits.prod.snd) f.F)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorUnit_src {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : (𝟙_ (Dial C)).src = ⊤_ C

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (MonoidalCategoryStruct.associator X Y Z).inv.F = Limits.prod.lift (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.fst Limits.prod.fst)) (Limits.prod.lift (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.fst Limits.prod.snd)) (CategoryStruct.comp Limits.prod.snd Limits.prod.snd))

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_leftUnitor_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.leftUnitor X).hom.F = Limits.prod.lift (Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt)) Limits.prod.snd

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorUnit_rel {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : (𝟙_ (Dial C)).rel = ⊤

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorObj_src {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (MonoidalCategoryStruct.tensorObj X Y).src = (X.src ⨯ Y.src)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (MonoidalCategoryStruct.associator X Y Z).hom.F = Limits.prod.lift (Limits.prod.lift (CategoryStruct.comp Limits.prod.snd Limits.prod.fst) (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.snd Limits.prod.fst))) (CategoryStruct.comp Limits.prod.snd (CategoryStruct.comp Limits.prod.snd Limits.prod.snd))

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerLeft_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X x✝ x✝¹ : Dial C) (f : x✝ ⟶ x✝¹) : (MonoidalCategoryStruct.whiskerLeft X f).f = Limits.prod.map (CategoryStruct.id X.src) f.f

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorObj_rel {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (MonoidalCategoryStruct.tensorObj X Y).rel = (Subobject.pullback (Limits.prod.map Limits.prod.fst Limits.prod.fst)).obj X.rel ⊓ (Subobject.pullback (Limits.prod.map Limits.prod.snd Limits.prod.snd)).obj Y.rel

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_associator_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (MonoidalCategoryStruct.associator X Y Z).inv.f = Limits.prod.lift (Limits.prod.lift Limits.prod.fst (CategoryStruct.comp Limits.prod.snd Limits.prod.fst)) (CategoryStruct.comp Limits.prod.snd Limits.prod.snd)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_whiskerRight_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁✝ X₂✝ : Dial C} (f : X₁✝ ⟶ X₂✝) (Y : Dial C) : (MonoidalCategoryStruct.whiskerRight f Y).f = Limits.prod.map f.f (CategoryStruct.id Y.src)

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_tensorHom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Dial C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (MonoidalCategoryStruct.tensorHom f g).f = Limits.prod.map f.f g.f

@[simp]

theorem CategoryTheory.Dial.instMonoidalCategoryStruct_rightUnitor_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : (MonoidalCategoryStruct.rightUnitor X).inv.F = CategoryStruct.comp Limits.prod.snd Limits.prod.fst

theorem CategoryTheory.Dial.tensor_id {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X₁ X₂ : Dial C) : MonoidalCategoryStruct.tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X₁ X₂)

theorem CategoryTheory.Dial.tensor_comp {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂) = CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂)

theorem CategoryTheory.Dial.associator_naturality {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Dial C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (Y₁.associator Y₂ Y₃).hom = CategoryStruct.comp (X₁.associator X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

theorem CategoryTheory.Dial.leftUnitor_naturality {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X Y : Dial C} (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (𝟙_ (Dial C))) f) (MonoidalCategoryStruct.leftUnitor Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom f

theorem CategoryTheory.Dial.rightUnitor_naturality {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X Y : Dial C} (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id (𝟙_ (Dial C)))) (MonoidalCategoryStruct.rightUnitor Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom f

theorem CategoryTheory.Dial.pentagon {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (W X Y Z : Dial C) : CategoryStruct.comp (tensorHom (W.associator X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (W.associator (X.tensorObj Y) Z).hom (tensorHom (CategoryStruct.id W) (X.associator Y Z).hom)) = CategoryStruct.comp ((W.tensorObj X).associator Y Z).hom (W.associator X (Y.tensorObj Z)).hom

theorem CategoryTheory.Dial.triangle {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : CategoryStruct.comp (X.associator (𝟙_ (Dial C)) Y).hom (tensorHom (CategoryStruct.id X) Y.leftUnitor.hom) = tensorHom X.rightUnitor.hom (CategoryStruct.id Y)

instance CategoryTheory.Dial.instMonoidalCategory {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : MonoidalCategory (Dial C)

Equations

• CategoryTheory.Dial.instMonoidalCategory = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def CategoryTheory.Dial.braiding {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : X.tensorObj Y ≅ Y.tensorObj X

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

Equations

• X.braiding Y = CategoryTheory.Dial.isoMk (CategoryTheory.Limits.prod.braiding X.src Y.src) (CategoryTheory.Limits.prod.braiding X.tgt Y.tgt) ⋯

@[simp]

theorem CategoryTheory.Dial.braiding_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.braiding Y).inv.F = Limits.prod.lift (CategoryStruct.comp Limits.prod.snd Limits.prod.snd) (CategoryStruct.comp Limits.prod.snd Limits.prod.fst)

@[simp]

theorem CategoryTheory.Dial.braiding_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.braiding Y).inv.f = Limits.prod.lift Limits.prod.snd Limits.prod.fst

@[simp]

theorem CategoryTheory.Dial.braiding_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.braiding Y).hom.F = Limits.prod.lift (CategoryStruct.comp Limits.prod.snd Limits.prod.snd) (CategoryStruct.comp Limits.prod.snd Limits.prod.fst)

@[simp]

theorem CategoryTheory.Dial.braiding_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.braiding Y).hom.f = Limits.prod.lift Limits.prod.snd Limits.prod.fst

theorem CategoryTheory.Dial.symmetry {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : CategoryStruct.comp (X.braiding Y).hom (Y.braiding X).hom = CategoryStruct.id (X.tensorObj Y)

theorem CategoryTheory.Dial.braiding_naturality_right {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) {Y Z : Dial C} (f : Y ⟶ Z) : CategoryStruct.comp (tensorHom (CategoryStruct.id X) f) (X.braiding Z).hom = CategoryStruct.comp (X.braiding Y).hom (tensorHom f (CategoryStruct.id X))

theorem CategoryTheory.Dial.braiding_naturality_left {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] {X Y : Dial C} (f : X ⟶ Y) (Z : Dial C) : CategoryStruct.comp (tensorHom f (CategoryStruct.id Z)) (Y.braiding Z).hom = CategoryStruct.comp (X.braiding Z).hom (tensorHom (CategoryStruct.id Z) f)

theorem CategoryTheory.Dial.hexagon_forward {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : CategoryStruct.comp (X.associator Y Z).hom (CategoryStruct.comp (X.braiding (MonoidalCategoryStruct.tensorObj Y Z)).hom (Y.associator Z X).hom) = CategoryStruct.comp (tensorHom (X.braiding Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (Y.associator X Z).hom (tensorHom (CategoryStruct.id Y) (X.braiding Z).hom))

theorem CategoryTheory.Dial.hexagon_reverse {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : CategoryStruct.comp (X.associator Y Z).inv (CategoryStruct.comp ((MonoidalCategoryStruct.tensorObj X Y).braiding Z).hom (Z.associator X Y).inv) = CategoryStruct.comp (tensorHom (CategoryStruct.id X) (Y.braiding Z).hom) (CategoryStruct.comp (X.associator Z Y).inv (tensorHom (X.braiding Z).hom (CategoryStruct.id Y)))

instance CategoryTheory.Dial.instSymmetricCategory {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : SymmetricCategory (Dial C)

Equations

• CategoryTheory.Dial.instSymmetricCategory = CategoryTheory.SymmetricCategory.mk ⋯