The Dialectica category is symmetric monoidal

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

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

@[simp]

theorem CategoryTheory.Dial.tensorObjImpl_rel {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.tensorObjImpl 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.tensorObjImpl_tgt {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y : Dial C) : (X.tensorObjImpl Y).tgt = (X.tgt ⨯ Y.tgt)

noncomputable def CategoryTheory.Dial.tensorHomImpl {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₁.tensorObjImpl Y₁ ⟶ X₂.tensorObjImpl 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.tensorHomImpl_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₂) : (tensorHomImpl 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.tensorHomImpl_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₂) : (tensorHomImpl f g).f = Limits.prod.map f.f g.f

noncomputable def CategoryTheory.Dial.tensorUnitImpl {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.tensorUnitImpl = { src := ⊤_ C, tgt := ⊤_ C, rel := ⊤ }

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Dial.leftUnitorImpl {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : tensorUnitImpl.tensorObjImpl X ≅ X

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Dial.rightUnitorImpl {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X : Dial C) : X.tensorObjImpl tensorUnitImpl ≅ X

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Dial.associatorImpl {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.tensorObjImpl Y).tensorObjImpl Z ≅ X.tensorObjImpl (Y.tensorObjImpl Z)

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

Equations

• X.associatorImpl 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.associatorImpl_inv_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associatorImpl 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.associatorImpl_hom_F {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associatorImpl 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.associatorImpl_hom_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associatorImpl 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.associatorImpl_inv_f {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] (X Y Z : Dial C) : (X.associatorImpl 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)

@[instance_reducible]

noncomputable 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.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.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.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.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.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.tensorUnit_rel {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : (MonoidalCategoryStruct.tensorUnit (Dial C)).rel = ⊤

@[simp]

theorem CategoryTheory.Dial.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.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.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.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.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.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.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

@[simp]

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

@[simp]

theorem CategoryTheory.Dial.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.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.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.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.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.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.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.tensorUnit_src {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] [Limits.HasPullbacks C] : (MonoidalCategoryStruct.tensorUnit (Dial C)).src = ⊤_ C

@[simp]

theorem CategoryTheory.Dial.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.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

theorem CategoryTheory.Dial.id_tensorHom_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.tensorHom_comp_tensorHom {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₂) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f₁ f₂) (MonoidalCategoryStruct.tensorHom g₁ g₂) = MonoidalCategoryStruct.tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ 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 (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f₁ f₂) f₃) (MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (MonoidalCategoryStruct.tensorHom f₁ (MonoidalCategoryStruct.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 (MonoidalCategoryStruct.tensorUnit (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 (MonoidalCategoryStruct.tensorUnit (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 (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator W (MonoidalCategoryStruct.tensorObj X Y) Z).hom (MonoidalCategoryStruct.tensorHom (CategoryStruct.id W) (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (MonoidalCategoryStruct.tensorObj W X) Y Z).hom (MonoidalCategoryStruct.associator W X (MonoidalCategoryStruct.tensorObj Y 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 (MonoidalCategoryStruct.associator X (MonoidalCategoryStruct.tensorUnit (Dial C)) Y).hom (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X) (MonoidalCategoryStruct.leftUnitor Y).hom) = MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.rightUnitor X).hom (CategoryStruct.id Y)

@[instance_reducible]

noncomputable 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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

@[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

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 (MonoidalCategoryStruct.tensorObj X 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 (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X) f) (X.braiding Z).hom = CategoryStruct.comp (X.braiding Y).hom (MonoidalCategoryStruct.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 (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id Z)) (Y.braiding Z).hom = CategoryStruct.comp (X.braiding Z).hom (MonoidalCategoryStruct.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 (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (X.braiding (MonoidalCategoryStruct.tensorObj Y Z)).hom (MonoidalCategoryStruct.associator Y Z X).hom) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (X.braiding Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y X Z).hom (MonoidalCategoryStruct.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 (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp ((MonoidalCategoryStruct.tensorObj X Y).braiding Z).hom (MonoidalCategoryStruct.associator Z X Y).inv) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X) (Y.braiding Z).hom) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Z Y).inv (MonoidalCategoryStruct.tensorHom (X.braiding Z).hom (CategoryStruct.id Y)))

@[instance_reducible]

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

Equations

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