Constructing braided categories from natural transformations between multifunctors

This file provides an alternative constructor for braided categories, given a braiding β : -₁ ⊗ -₂ ≅ -₂ ⊗ -₁ as a natural isomorphism between bifunctors. The hexagon identities are phrased as equalities of natural transformations between trifunctors (-₁ ⊗ -₂) ⊗ -₃ ⟶ -₂ ⊗ (-₃ ⊗ -₁) and -₁ ⊗ (-₂ ⊗ -₃) ⟶ (-₃ ⊗ -₁) ⊗ -₂.

def CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ (X₁ ⊗ X₂) ⊗ X₃

Equations

• CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C = CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensor C)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ : C) {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C) : (((functor₁₂₃ C).obj X₁).map φ).app X₃ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerRight φ X₃)) (MonoidalCategoryStruct.associator X₁ Y₂ X₃).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : C) : (((functor₁₂₃ C).obj X₁).obj X₂).obj X₃ = MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X₁ X₂) X₃

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X₁ Y₁ : C} (φ : X₁ ⟶ Y₁) (X₂ X₃ : C) : (((functor₁₂₃ C).map φ).app X₂).app X₃ = MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight φ X₂) X₃

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ : C) {x✝ x✝¹ : C} (φ : x✝ ⟶ x✝¹) : (((functor₁₂₃ C).obj X₁).obj X₂).map φ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ x✝).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerLeft X₂ φ)) (MonoidalCategoryStruct.associator X₁ X₂ x✝¹).inv)

def CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ X₁ ⊗ (X₂ ⊗ X₃)

Equations

• CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C = CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensor C)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ : C) {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C) : (((functor₁₂₃' C).obj X₁).map φ).app X₃ = MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerRight φ X₃)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : C) : (((functor₁₂₃' C).obj X₁).obj X₂).obj X₃ = MonoidalCategoryStruct.tensorObj X₁ (MonoidalCategoryStruct.tensorObj X₂ X₃)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X₁ Y₁ : C} (φ : X₁ ⟶ Y₁) (X₂ X₃ : C) : (((functor₁₂₃' C).map φ).app X₂).app X₃ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₂ X₃).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight φ X₂) X₃) (MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ : C) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : (((functor₁₂₃' C).obj X₁).obj X₂).map φ = MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerLeft X₂ φ)

def CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ (X₂ ⊗ X₃) ⊗ X₁

Equations

• CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C = CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.curriedTensor C).flip (CategoryTheory.MonoidalCategory.curriedTensor C)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ : C) {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C) : (((functor₂₃₁ C).obj X₁).map φ).app X₃ = MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight φ X₃) X₁

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : C) : (((functor₂₃₁ C).obj X₁).obj X₂).obj X₃ = MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X₂ X₃) X₁

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ : C) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : (((functor₂₃₁ C).obj X₁).obj X₂).map φ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ X✝ X₁).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₂ (MonoidalCategoryStruct.whiskerRight φ X₁)) (MonoidalCategoryStruct.associator X₂ Y✝ X₁).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X₁ Y₁ : C} (φ : X₁ ⟶ Y₁) (X₂ X₃ : C) : (((functor₂₃₁ C).map φ).app X₂).app X₃ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ X₃ X₁).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₂ (MonoidalCategoryStruct.whiskerLeft X₃ φ)) (MonoidalCategoryStruct.associator X₂ X₃ Y₁).inv)

def CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ X₂ ⊗ (X₃ ⊗ X₁)

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G H : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (((functor₂₃₁' C).obj G).obj H).map f = MonoidalCategoryStruct.whiskerLeft H (MonoidalCategoryStruct.whiskerRight f G)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G : C) {X✝ Y✝ : C} (g : X✝ ⟶ Y✝) (X : C) : (((functor₂₃₁' C).obj G).map g).app X = CategoryStruct.comp (MonoidalCategoryStruct.associator X✝ X G).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight g X) G) (MonoidalCategoryStruct.associator Y✝ X G).hom)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : C} (h : X✝ ⟶ Y✝) (X Y : C) : (((functor₂₃₁' C).map h).app X).app Y = MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerLeft Y h)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G H K : C) : (((functor₂₃₁' C).obj G).obj H).obj K = MonoidalCategoryStruct.tensorObj H (MonoidalCategoryStruct.tensorObj K G)

def CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ (X₂ ⊗ X₁) ⊗ X₃

Equations

• CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C = CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C).flip (CategoryTheory.MonoidalCategory.curriedTensor C)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : C) : (((functor₂₁₃ C).obj X₁).obj X₂).obj X₃ = MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X₂ X₁) X₃

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X₁ Y₁ : C} (φ : X₁ ⟶ Y₁) (X₂ X₃ : C) : (((functor₂₁₃ C).map φ).app X₂).app X₃ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ X₁ X₃).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₂ (MonoidalCategoryStruct.whiskerRight φ X₃)) (MonoidalCategoryStruct.associator X₂ Y₁ X₃).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ : C) {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C) : (((functor₂₁₃ C).obj X₁).map φ).app X₃ = MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight φ X₁) X₃

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ : C) {x✝ x✝¹ : C} (φ : x✝ ⟶ x✝¹) : (((functor₂₁₃ C).obj X₁).obj X₂).map φ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ X₁ x✝).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X₂ (MonoidalCategoryStruct.whiskerLeft X₁ φ)) (MonoidalCategoryStruct.associator X₂ X₁ x✝¹).inv)

def CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ X₂ ⊗ (X₁ ⊗ X₃)

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X₃ : C) : (((functor₂₁₃' C).obj k).map f).app X₃ = CategoryStruct.comp (MonoidalCategoryStruct.associator X✝ k X₃).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight f k) X₃) (MonoidalCategoryStruct.associator Y✝ k X₃).hom)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (k j : C) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : (((functor₂₁₃' C).obj k).obj j).map φ = MonoidalCategoryStruct.whiskerLeft j (MonoidalCategoryStruct.whiskerLeft k φ)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (k j X₃ : C) : (((functor₂₁₃' C).obj k).obj j).obj X₃ = MonoidalCategoryStruct.tensorObj j (MonoidalCategoryStruct.tensorObj k X₃)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j X₃ : C) : (((functor₂₁₃' C).map f).app j).app X₃ = MonoidalCategoryStruct.whiskerLeft j (MonoidalCategoryStruct.whiskerRight f X₃)

def CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ X₃ ⊗ (X₁ ⊗ X₂)

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : C) : (((functor₃₁₂' C).obj G).map f).app j = MonoidalCategoryStruct.whiskerLeft j (MonoidalCategoryStruct.whiskerLeft G f)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (((functor₃₁₂' C).obj G).obj k).map f = CategoryStruct.comp (MonoidalCategoryStruct.associator X✝ G k).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight f G) k) (MonoidalCategoryStruct.associator Y✝ G k).hom)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G k j : C) : (((functor₃₁₂' C).obj G).obj k).obj j = MonoidalCategoryStruct.tensorObj j (MonoidalCategoryStruct.tensorObj G k)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y X : C) : (((functor₃₁₂' C).map f).app Y).app X = MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerRight f Y)

def CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ (X₃ ⊗ X₁) ⊗ X₂

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y X : C) : (((functor₃₁₂ C).map f).app Y).app X = CategoryStruct.comp (MonoidalCategoryStruct.associator X X✝ Y).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerRight f Y)) (MonoidalCategoryStruct.associator X Y✝ Y).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : C) : (((functor₃₁₂ C).obj G).map f).app j = CategoryStruct.comp (MonoidalCategoryStruct.associator j G X✝).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft j (MonoidalCategoryStruct.whiskerLeft G f)) (MonoidalCategoryStruct.associator j G Y✝).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G k j : C) : (((functor₃₁₂ C).obj G).obj k).obj j = MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj j G) k

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (((functor₃₁₂ C).obj G).obj k).map f = MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight f G) k

def CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ X₁ ⊗ (X₃ ⊗ X₂)

Equations

• CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C = CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensor C).flip

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ : C) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : (((functor₁₃₂' C).obj X₁).obj X₂).map φ = MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerRight φ X₂)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X₁ Y₁ : C} (φ : X₁ ⟶ Y₁) (X₂ X₃ : C) : (((functor₁₃₂' C).map φ).app X₂).app X₃ = CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ X₃ X₂).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight φ X₃) X₂) (MonoidalCategoryStruct.associator Y₁ X₃ X₂).hom)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ : C) {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C) : (((functor₁₃₂' C).obj X₁).map φ).app X₃ = MonoidalCategoryStruct.whiskerLeft X₁ (MonoidalCategoryStruct.whiskerLeft X₃ φ)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : C) : (((functor₁₃₂' C).obj X₁).obj X₂).obj X₃ = MonoidalCategoryStruct.tensorObj X₁ (MonoidalCategoryStruct.tensorObj X₃ X₂)

def CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor C (Functor C (Functor C C))

The trifunctor `X₁ X₂ X₃ ↦ (X₁ ⊗ X₃) ⊗ X₂

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : C) : (((functor₁₃₂ C).obj G).map f).app j = CategoryStruct.comp (MonoidalCategoryStruct.associator G j X✝).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G (MonoidalCategoryStruct.whiskerLeft j f)) (MonoidalCategoryStruct.associator G j Y✝).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G k j : C) : (((functor₁₃₂ C).obj G).obj k).obj j = MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj G j) k

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (G k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (((functor₁₃₂ C).obj G).obj k).map f = CategoryStruct.comp (MonoidalCategoryStruct.associator G X✝ k).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G (MonoidalCategoryStruct.whiskerRight f k)) (MonoidalCategoryStruct.associator G Y✝ k).inv)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_map_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y X : C) : (((functor₁₃₂ C).map f).app Y).app X = MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight f X) Y

The forward hexagon identity

Given a braiding in the form of a natural isomorphism of bifunctors β : curriedTensor C ≅ (curriedTensor C).flip (i.e. (β.app X₁).app X₂ : X₁ ⊗ X₂ ≅ X₂ ⊗ X₁), we phrase the forward hexagon identity as an equality of natural transformations between trifunctors (the hexagon on the left is the diagram we require to commute, the hexagon on the right is the same on the object level on three objects X₁ X₂ X₃).

            funtor₁₂₃                         (X₁ ⊗ X₂) ⊗ X₃
associtator/          \ secondMap₁             /           \
          v            v                      v             v
     functor₁₂₃'    functor₂₁₃          X₁ ⊗ (X₂ ⊗ X₃)    (X₂ ⊗ X₁) ⊗ X₃
 firsMap₂ |            |secondMap₂            |             |
          v            v                      v             v
     functor₂₃₁     functor₂₁₃'         (X₂ ⊗ X₃) ⊗ X₁    X₂ ⊗ (X₁ ⊗ X₃)
  firstMap₃\           / secondMap₃            \            /
            v         v                         v          v
             functor₂₃₁'                        X₂ ⊗ (X₃ ⊗ X₁)

def CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂ {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) : Hexagon.functor₁₂₃' C ⟶ Hexagon.functor₂₃₁ C

The middle left map in the forward hexagon identity.

Equations

• CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂ β = (CategoryTheory.bifunctorComp₂₃Functor.map β.hom).app (CategoryTheory.MonoidalCategory.curriedTensor C)

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂_app_app_app {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (X₁ X₂ X₃ : C) : (((firstMap₂ β).app X₁).app X₂).app X₃ = (β.hom.app X₁).app (MonoidalCategoryStruct.tensorObj X₂ X₃)

def CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Hexagon.functor₂₃₁ C ⟶ Hexagon.functor₂₃₁' C

The bottom left map in the forward hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃_app_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (x✝ x✝¹ x✝² : C) : (((firstMap₃ C).app x✝).app x✝¹).app x✝² = (MonoidalCategoryStruct.associator x✝¹ x✝² x✝).hom

def CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁ {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) : Hexagon.functor₁₂₃ C ⟶ Hexagon.functor₂₁₃ C

The top right map in the forward hexagon identity.

Equations

• CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁ β = (CategoryTheory.bifunctorComp₁₂Functor.map β.hom).app (CategoryTheory.MonoidalCategory.curriedTensor C)

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁_app_app_app {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (X₁ X₂ X₃ : C) : (((secondMap₁ β).app X₁).app X₂).app X₃ = MonoidalCategoryStruct.whiskerRight ((β.hom.app X₁).app X₂) X₃

def CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Hexagon.functor₂₁₃ C ⟶ Hexagon.functor₂₁₃' C

The middle right map in the forward hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂_app_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (x✝ x✝¹ x✝² : C) : (((secondMap₂ C).app x✝).app x✝¹).app x✝² = (MonoidalCategoryStruct.associator x✝¹ x✝ x✝²).hom

def CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃ {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) : Hexagon.functor₂₁₃' C ⟶ Hexagon.functor₂₃₁' C

The bottom right map in the forward hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (X Y Z : C) : (((secondMap₃ β).app X).app Y).app Z = MonoidalCategoryStruct.whiskerLeft Y ((β.hom.app X).app Z)

The reverse hexagon identity

Given a braiding in the form of a natural isomorphism of bifunctors β : curriedTensor C ≅ (curriedTensor C).flip (i.e. (β.app X₁).app X₂ : X₁ ⊗ X₂ ≅ X₂ ⊗ X₁), we phrase the reverse hexagon identity as an equality of natural transformations between trifunctors (the hexagon on the left is the diagram we require to commute, the hexagon on the right is the same on the object level on three objects X₁ X₂ X₃).

            funtor₁₂₃'                        X₁ ⊗ (X₂ ⊗ X₃)
associtator/          \ secondMap₁             /           \
          v            v                      v             v
     functor₁₂₃    functor₁₃₂'          (X₁ ⊗ X₂) ⊗ X₃    X₁ ⊗ (X₃ ⊗ X₂)
 firsMap₂ |            |secondMap₂            |             |
          v            v                      v             v
     functor₃₁₂'    functor₁₃₂          X₃ ⊗ (X₁ ⊗ X₂)    (X₁ ⊗ X₃) ⊗ X₂
  firstMap₃\           / secondMap₃            \            /
            v         v                         v          v
             functor₃₁₂                        (X₃ ⊗ X₁) ⊗ X₂

def CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂ {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) : Hexagon.functor₁₂₃ C ⟶ Hexagon.functor₃₁₂' C

The middle left map in the reverse hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (X Y Z : C) : (((firstMap₂ β).app X).app Y).app Z = (β.hom.app (MonoidalCategoryStruct.tensorObj X Y)).app Z

def CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Hexagon.functor₃₁₂' C ⟶ Hexagon.functor₃₁₂ C

The bottom left map in the reverse hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y Z : C) : (((firstMap₃ C).app X).app Y).app Z = (MonoidalCategoryStruct.associator Z X Y).inv

def CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁ {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) : Hexagon.functor₁₂₃' C ⟶ Hexagon.functor₁₃₂' C

The top right map in the reverse hexagon identity.

Equations

• CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁ β = (CategoryTheory.bifunctorComp₂₃Functor.obj (CategoryTheory.MonoidalCategory.curriedTensor C)).map β.hom

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁_app_app_app {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (X₁ X₂ X₃ : C) : (((secondMap₁ β).app X₁).app X₂).app X₃ = MonoidalCategoryStruct.whiskerLeft X₁ ((β.hom.app X₂).app X₃)

def CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂ (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Hexagon.functor₁₃₂' C ⟶ Hexagon.functor₁₃₂ C

The middle right map in the reverse hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂_app_app_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (x✝ x✝¹ x✝² : C) : (((secondMap₂ C).app x✝).app x✝¹).app x✝² = (MonoidalCategoryStruct.associator x✝ x✝² x✝¹).inv

def CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃ {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) : Hexagon.functor₁₃₂ C ⟶ Hexagon.functor₃₁₂ C

The bottom right map in the reverse hexagon identity.

Equations

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

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (X Y Z : C) : (((secondMap₃ β).app X).app Y).app Z = MonoidalCategoryStruct.whiskerRight ((β.hom.app X).app Z) Y

def CategoryTheory.BraidedCategory.ofBifunctor {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (β : MonoidalCategory.curriedTensor C ≅ (MonoidalCategory.curriedTensor C).flip) (hexagon_forward : CategoryStruct.comp (MonoidalCategory.curriedAssociatorNatIso C).hom (CategoryStruct.comp (ofBifunctor.Forward.firstMap₂ β) (ofBifunctor.Forward.firstMap₃ C)) = CategoryStruct.comp (ofBifunctor.Forward.secondMap₁ β) (CategoryStruct.comp (ofBifunctor.Forward.secondMap₂ C) (ofBifunctor.Forward.secondMap₃ β))) (hexagon_reverse : CategoryStruct.comp (MonoidalCategory.curriedAssociatorNatIso C).inv (CategoryStruct.comp (ofBifunctor.Reverse.firstMap₂ β) (ofBifunctor.Reverse.firstMap₃ C)) = CategoryStruct.comp (ofBifunctor.Reverse.secondMap₁ β) (CategoryStruct.comp (ofBifunctor.Reverse.secondMap₂ C) (ofBifunctor.Reverse.secondMap₃ β))) : BraidedCategory C

Given a braiding β : curriedTensor C ≅ (curriedTensor C).flip as a natural isomorphism between bifunctors, and the two equalities hexagon_forward and hexagon_reverse of natural transformations between trifunctors, we obtain a braided category structure.

Equations

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