Documentation

Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor

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.{v_1, u_1} C] [MonoidalCategory C] :

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_obj_map (C : Type u_1) [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_map_app_app (C : Type u_1) [Category.{v_1, 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_obj (C : Type u_1) [Category.{v_1, 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_map_app (C : Type u_1) [Category.{v_1, 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)

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

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_obj_map (C : Type u_1) [Category.{v_1, 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₂ φ)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_map_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_map_app_app (C : Type u_1) [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_map_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.{v_1, 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)

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

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

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

(((functor₂₃₁' C).obj G).obj H).obj K = MonoidalCategoryStruct.tensorObj H (MonoidalCategoryStruct.tensorObj K G)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_obj_map (C : Type u_1) [Category.{v_1, 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.{v_1, 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.{v_1, 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)

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

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_map_app_app (C : Type u_1) [Category.{v_1, 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_obj_obj (C : Type u_1) [Category.{v_1, 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.{v_1, 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)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_map_app (C : Type u_1) [Category.{v_1, 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₃

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

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_map_app (C : Type u_1) [Category.{v_1, 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_obj (C : Type u_1) [Category.{v_1, 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₂₁₃'_obj_obj_map (C : Type u_1) [Category.{v_1, 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₂₁₃'_map_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_map_app_app (C : Type u_1) [Category.{v_1, 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)

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_obj_map (C : Type u_1) [Category.{v_1, 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_map_app (C : Type u_1) [Category.{v_1, 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_obj (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] (G k j : C) :

(((functor₃₁₂' C).obj G).obj k).obj j = MonoidalCategoryStruct.tensorObj j (MonoidalCategoryStruct.tensorObj G k)

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

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_obj_map (C : Type u_1) [Category.{v_1, 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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_map_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] (G k j : C) :

(((functor₃₁₂ C).obj G).obj k).obj j = MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj j G) k

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

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_map_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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₁₃₂'_obj_map_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Functor C (Functor C (Functor C C))

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

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_map_app_app (C : Type u_1) [Category.{v_1, 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

@[simp]

theorem CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_obj_obj (C : Type u_1) [Category.{v_1, 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_map_app (C : Type u_1) [Category.{v_1, 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_map (C : Type u_1) [Category.{v_1, 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)

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

            functor₁₂₃                        (X₁ ⊗ X₂) ⊗ X₃
associator /          \ secondMap₁             /           \
          v            v                      v             v
     functor₁₂₃'    functor₂₁₃          X₁ ⊗ (X₂ ⊗ X₃)    (X₂ ⊗ X₁) ⊗ X₃
firstMap₂ |            |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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂_app_app_app {C : Type u_1} [Category.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Hexagon.functor₂₃₁ C ⟶ Hexagon.functor₂₃₁' C

The bottom left map in the forward hexagon identity.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃_app_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁_app_app_app {C : Type u_1} [Category.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Hexagon.functor₂₁₃ C ⟶ Hexagon.functor₂₁₃' C

The middle right map in the forward hexagon identity.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂_app_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app {C : Type u_1} [Category.{v_1, 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₃).

            functor₁₂₃'                       X₁ ⊗ (X₂ ⊗ X₃)
associator /          \ secondMap₁             /           \
          v            v                      v             v
     functor₁₂₃    functor₁₃₂'          (X₁ ⊗ X₂) ⊗ X₃    X₁ ⊗ (X₃ ⊗ X₂)
firstMap₂ |            |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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app {C : Type u_1} [Category.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Hexagon.functor₃₁₂' C ⟶ Hexagon.functor₃₁₂ C

The bottom left map in the reverse hexagon identity.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁_app_app_app {C : Type u_1} [Category.{v_1, 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.{v_1, u_1} C] [MonoidalCategory C] :

Hexagon.functor₁₃₂' C ⟶ Hexagon.functor₁₃₂ C

The middle right map in the reverse hexagon identity.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂_app_app_app (C : Type u_1) [Category.{v_1, 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.{v_1, 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.

Instances For

@[simp]

theorem CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app {C : Type u_1} [Category.{v_1, 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

@[implicit_reducible]

def CategoryTheory.BraidedCategory.ofBifunctor {C : Type u_1} [Category.{v_1, 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.

Instances For

@[implicit_reducible]

def CategoryTheory.SymmetricCategory.ofCurried {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] (h : CategoryStruct.comp (BraidedCategory.curriedBraidingNatIso C).hom ((flipFunctor C C C).map (BraidedCategory.curriedBraidingNatIso C).hom) = CategoryStruct.id (MonoidalCategory.curriedTensor C)) :

SymmetricCategory C

Alternative constructor for symmetric categories, where the symmetry of the braiding is phrased as an equality of natural transformation of bifunctors.

Instances For