The Dialectica category is symmetric monoidal

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

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

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

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

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.

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

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

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 := ⊤ }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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)

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

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)

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

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

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

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