category_theory.monoidal.braided

@[class]

structure category_theory.braided_category (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

Type (max u v)

braiding : Π (X Y : C), X ⊗ Y ≅ Y ⊗ X
braiding_naturality' : (∀ {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (f ⊗ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ f)) . "obviously"
hexagon_forward' : (∀ (X Y Z : C), (α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = ((β_ X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (β_ X Z).hom)) . "obviously"
hexagon_reverse' : (∀ (X Y Z : C), (α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = (𝟙 X ⊗ (β_ Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((β_ X Z).hom ⊗ 𝟙 Y)) . "obviously"

A braided monoidal category is a monoidal category equipped with a braiding isomorphism β_ X Y : X ⊗ Y ≅ Y ⊗ X which is natural in both arguments, and also satisfies the two hexagon identities.

Instances of this typeclass

Instances of other typeclasses for category_theory.braided_category

category_theory.braided_category.has_sizeof_inst

source

@[simp]

theorem category_theory.braided_category.braiding_naturality {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.braided_category C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

(f ⊗ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ f)

source

@[simp]

theorem category_theory.braided_category.braiding_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.braided_category C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {X'_1 : C} (f' : Y' ⊗ Y ⟶ X'_1) :

(f ⊗ g) ≫ (β_ Y Y').hom ≫ f' = (β_ X X').hom ≫ (g ⊗ f) ≫ f'

source

theorem category_theory.braided_category.hexagon_forward {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.braided_category C] (X Y Z : C) :

(α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = ((β_ X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (β_ X Z).hom)

source

theorem category_theory.braided_category.hexagon_reverse {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.braided_category C] (X Y Z : C) :

(α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = (𝟙 X ⊗ (β_ Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((β_ X Z).hom ⊗ 𝟙 Y)

source

theorem category_theory.braided_category.hexagon_reverse_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.braided_category C] (X Y Z : C) {X' : C} (f' : (Z ⊗ X) ⊗ Y ⟶ X') :

(α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv ≫ f' = (𝟙 X ⊗ (β_ Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((β_ X Z).hom ⊗ 𝟙 Y) ≫ f'

source

theorem category_theory.braided_category.hexagon_forward_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.braided_category C] (X Y Z : C) {X' : C} (f' : Y ⊗ Z ⊗ X ⟶ X') :

(α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom ≫ f' = ((β_ X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (β_ X Z).hom) ≫ f'

source

def category_theory.braided_category_of_faithful {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.faithful F.to_lax_monoidal_functor.to_functor] [category_theory.braided_category D] (β : Π (X Y : C), X ⊗ Y ≅ Y ⊗ X) (w : ∀ (X Y : C), F.to_lax_monoidal_functor.μ X Y ≫ F.to_lax_monoidal_functor.to_functor.map (β X Y).hom = (β_ (F.to_lax_monoidal_functor.to_functor.obj X) (F.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ F.to_lax_monoidal_functor.μ Y X) :

category_theory.braided_category C

Verifying the axioms for a braiding by checking that the candidate braiding is sent to a braiding by a faithful monoidal functor.

Equations

category_theory.braided_category_of_faithful F β w = {braiding := β, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}

source

noncomputable def category_theory.braided_category_of_fully_faithful {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.full F.to_lax_monoidal_functor.to_functor] [category_theory.faithful F.to_lax_monoidal_functor.to_functor] [category_theory.braided_category D] :

category_theory.braided_category C

Pull back a braiding along a fully faithful monoidal functor.

Equations

source

theorem category_theory.braiding_left_unitor_aux₁ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(α_ (𝟙_ C) (𝟙_ C) X).hom ≫ (𝟙 (𝟙_ C) ⊗ (β_ X (𝟙_ C)).inv) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) = ((λ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ X (𝟙_ C)).inv

source

theorem category_theory.braiding_left_unitor_aux₂ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

((β_ X (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫ ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) = (ρ_ X).hom ⊗ 𝟙 (𝟙_ C)

source

@[simp]

theorem category_theory.braiding_left_unitor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom

source

theorem category_theory.braiding_right_unitor_aux₁ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(α_ X (𝟙_ C) (𝟙_ C)).inv ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) = (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv

source

theorem category_theory.braiding_right_unitor_aux₂ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) = 𝟙 (𝟙_ C) ⊗ (λ_ X).hom

source

@[simp]

theorem category_theory.braiding_right_unitor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom

source

@[simp]

theorem category_theory.left_unitor_inv_braiding (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv

source

@[simp]

theorem category_theory.right_unitor_inv_braiding (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv

source

@[class]

structure category_theory.symmetric_category (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

Type (max u v)

to_braided_category : category_theory.braided_category C
symmetry' : (∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)) . "obviously"

A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.

See https://stacks.math.columbia.edu/tag/0FFW.

Instances of this typeclass

Instances of other typeclasses for category_theory.symmetric_category

category_theory.symmetric_category.has_sizeof_inst

source

@[simp]

theorem category_theory.symmetric_category.symmetry {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.symmetric_category C] (X Y : C) :

(β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)

source

@[simp]

theorem category_theory.symmetric_category.symmetry_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [self : category_theory.symmetric_category C] (X Y : C) {X' : C} (f' : X ⊗ Y ⟶ X') :

(β_ X Y).hom ≫ (β_ Y X).hom ≫ f' = f'

source

structure category_theory.lax_braided_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] :

Type (max u₁ u₂ v₁ v₂)

to_lax_monoidal_functor : category_theory.lax_monoidal_functor C D
braided' : (∀ (X Y : C), self.to_lax_monoidal_functor.μ X Y ≫ self.to_lax_monoidal_functor.to_functor.map (β_ X Y).hom = (β_ (self.to_lax_monoidal_functor.to_functor.obj X) (self.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ self.to_lax_monoidal_functor.μ Y X) . "obviously"

A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.

Instances for category_theory.lax_braided_functor

category_theory.lax_braided_functor.has_sizeof_inst
category_theory.lax_braided_functor.inhabited
category_theory.lax_braided_functor.category_lax_braided_functor

source

theorem category_theory.lax_braided_functor.braided {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (self : category_theory.lax_braided_functor C D) (X Y : C) :

self.to_lax_monoidal_functor.μ X Y ≫ self.to_lax_monoidal_functor.to_functor.map (β_ X Y).hom = (β_ (self.to_lax_monoidal_functor.to_functor.obj X) (self.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ self.to_lax_monoidal_functor.μ Y X

source

@[simp]

theorem category_theory.lax_braided_functor.id_to_lax_monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(category_theory.lax_braided_functor.id C).to_lax_monoidal_functor = (category_theory.monoidal_functor.id C).to_lax_monoidal_functor

source

def category_theory.lax_braided_functor.id (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.lax_braided_functor C C

The identity lax braided monoidal functor.

Equations

category_theory.lax_braided_functor.id C = {to_lax_monoidal_functor := (category_theory.monoidal_functor.id C).to_lax_monoidal_functor, braided' := _}

source

@[protected, instance]

def category_theory.lax_braided_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

inhabited (category_theory.lax_braided_functor C C)

Equations

category_theory.lax_braided_functor.inhabited C = {default := category_theory.lax_braided_functor.id C _inst_3}

source

@[simp]

theorem category_theory.lax_braided_functor.comp_to_lax_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] [category_theory.braided_category E] (F : category_theory.lax_braided_functor C D) (G : category_theory.lax_braided_functor D E) :

(F.comp G).to_lax_monoidal_functor = F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor

source

def category_theory.lax_braided_functor.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] [category_theory.braided_category E] (F : category_theory.lax_braided_functor C D) (G : category_theory.lax_braided_functor D E) :

category_theory.lax_braided_functor C E

The composition of lax braided monoidal functors.

Equations

F.comp G = {to_lax_monoidal_functor := {to_functor := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).to_functor, ε := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).ε, μ := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, braided' := _}

source

@[protected, instance]

def category_theory.lax_braided_functor.category_lax_braided_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] :

category_theory.category (category_theory.lax_braided_functor C D)

Equations

category_theory.lax_braided_functor.category_lax_braided_functor = category_theory.induced_category.category category_theory.lax_braided_functor.to_lax_monoidal_functor

source

@[simp]

theorem category_theory.lax_braided_functor.comp_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G H : category_theory.lax_braided_functor C D} {α : F ⟶ G} {β : G ⟶ H} :

(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans

source

@[simp]

theorem category_theory.lax_braided_functor.mk_iso_inv {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G : category_theory.lax_braided_functor C D} (i : F.to_lax_monoidal_functor ≅ G.to_lax_monoidal_functor) :

(category_theory.lax_braided_functor.mk_iso i).inv = i.inv

source

def category_theory.lax_braided_functor.mk_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G : category_theory.lax_braided_functor C D} (i : F.to_lax_monoidal_functor ≅ G.to_lax_monoidal_functor) :

F ≅ G

Interpret a natural isomorphism of the underlyling lax monoidal functors as an isomorphism of the lax braided monoidal functors.

Equations

category_theory.lax_braided_functor.mk_iso i = {hom := i.hom, inv := i.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.lax_braided_functor.mk_iso_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G : category_theory.lax_braided_functor C D} (i : F.to_lax_monoidal_functor ≅ G.to_lax_monoidal_functor) :

(category_theory.lax_braided_functor.mk_iso i).hom = i.hom

source

structure category_theory.braided_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] :

Type (max u₁ u₂ v₁ v₂)

to_monoidal_functor : category_theory.monoidal_functor C D
braided' : (∀ (X Y : C), self.to_monoidal_functor.to_lax_monoidal_functor.to_functor.map (β_ X Y).hom = category_theory.inv (self.to_monoidal_functor.to_lax_monoidal_functor.μ X Y) ≫ (β_ (self.to_monoidal_functor.to_lax_monoidal_functor.to_functor.obj X) (self.to_monoidal_functor.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ self.to_monoidal_functor.to_lax_monoidal_functor.μ Y X) . "obviously"

A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.

Instances for category_theory.braided_functor

category_theory.braided_functor.has_sizeof_inst
category_theory.braided_functor.inhabited
category_theory.braided_functor.category_braided_functor

source

@[simp]

theorem category_theory.braided_functor.braided {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (self : category_theory.braided_functor C D) (X Y : C) :

self.to_monoidal_functor.to_lax_monoidal_functor.to_functor.map (β_ X Y).hom = category_theory.inv (self.to_monoidal_functor.to_lax_monoidal_functor.μ X Y) ≫ (β_ (self.to_monoidal_functor.to_lax_monoidal_functor.to_functor.obj X) (self.to_monoidal_functor.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ self.to_monoidal_functor.to_lax_monoidal_functor.μ Y X

source

def category_theory.symmetric_category_of_faithful {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] [category_theory.braided_category C] [category_theory.symmetric_category D] (F : category_theory.braided_functor C D) [category_theory.faithful F.to_monoidal_functor.to_lax_monoidal_functor.to_functor] :

category_theory.symmetric_category C

A braided category with a braided functor to a symmetric category is itself symmetric.

Equations

category_theory.symmetric_category_of_faithful F = {to_braided_category := _inst_14, symmetry' := _}

source

@[simp]

theorem category_theory.braided_functor.to_lax_braided_functor_to_lax_monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (F : category_theory.braided_functor C D) :

(category_theory.braided_functor.to_lax_braided_functor C D F).to_lax_monoidal_functor = F.to_monoidal_functor.to_lax_monoidal_functor

source

def category_theory.braided_functor.to_lax_braided_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (F : category_theory.braided_functor C D) :

category_theory.lax_braided_functor C D

Turn a braided functor into a lax braided functor.

Equations

category_theory.braided_functor.to_lax_braided_functor C D F = {to_lax_monoidal_functor := F.to_monoidal_functor.to_lax_monoidal_functor, braided' := _}

source

def category_theory.braided_functor.id (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.braided_functor C C

The identity braided monoidal functor.

Equations

category_theory.braided_functor.id C = {to_monoidal_functor := {to_lax_monoidal_functor := (category_theory.monoidal_functor.id C).to_lax_monoidal_functor, ε_is_iso := _, μ_is_iso := _}, braided' := _}

source

@[simp]

theorem category_theory.braided_functor.id_to_monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(category_theory.braided_functor.id C).to_monoidal_functor = category_theory.monoidal_functor.id C

source

@[protected, instance]

def category_theory.braided_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

inhabited (category_theory.braided_functor C C)

Equations

category_theory.braided_functor.inhabited C = {default := category_theory.braided_functor.id C _inst_3}

source

@[simp]

theorem category_theory.braided_functor.comp_to_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] [category_theory.braided_category E] (F : category_theory.braided_functor C D) (G : category_theory.braided_functor D E) :

(F.comp G).to_monoidal_functor = F.to_monoidal_functor ⊗⋙ G.to_monoidal_functor

source

def category_theory.braided_functor.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] [category_theory.braided_category E] (F : category_theory.braided_functor C D) (G : category_theory.braided_functor D E) :

category_theory.braided_functor C E

The composition of braided monoidal functors.

Equations

F.comp G = {to_monoidal_functor := {to_lax_monoidal_functor := (F.to_monoidal_functor ⊗⋙ G.to_monoidal_functor).to_lax_monoidal_functor, ε_is_iso := _, μ_is_iso := _}, braided' := _}

source

@[protected, instance]

def category_theory.braided_functor.category_braided_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] :

category_theory.category (category_theory.braided_functor C D)

Equations

category_theory.braided_functor.category_braided_functor = category_theory.induced_category.category category_theory.braided_functor.to_monoidal_functor

source

@[simp]

theorem category_theory.braided_functor.comp_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G H : category_theory.braided_functor C D} {α : F ⟶ G} {β : G ⟶ H} :

(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans

source

@[simp]

theorem category_theory.braided_functor.mk_iso_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G : category_theory.braided_functor C D} (i : F.to_monoidal_functor ≅ G.to_monoidal_functor) :

(category_theory.braided_functor.mk_iso i).hom = i.hom

source

@[simp]

theorem category_theory.braided_functor.mk_iso_inv {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G : category_theory.braided_functor C D} (i : F.to_monoidal_functor ≅ G.to_monoidal_functor) :

(category_theory.braided_functor.mk_iso i).inv = i.inv

source

def category_theory.braided_functor.mk_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] {F G : category_theory.braided_functor C D} (i : F.to_monoidal_functor ≅ G.to_monoidal_functor) :

F ≅ G

Interpret a natural isomorphism of the underlyling monoidal functors as an isomorphism of the braided monoidal functors.

Equations

category_theory.braided_functor.mk_iso i = {hom := i.hom, inv := i.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[protected, instance]

def category_theory.discrete.braided_category (M : Type u) [comm_monoid M] :

category_theory.braided_category (category_theory.discrete M)

Equations

category_theory.discrete.braided_category M = {braiding := λ (X Y : category_theory.discrete M), category_theory.discrete.eq_to_iso _, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}

source

def category_theory.discrete.braided_functor {M : Type u} [comm_monoid M] {N : Type u} [comm_monoid N] (F : M →* N) :

category_theory.braided_functor (category_theory.discrete M) (category_theory.discrete N)

A multiplicative morphism between commutative monoids gives a braided functor between the corresponding discrete braided monoidal categories.

Equations

category_theory.discrete.braided_functor F = {to_monoidal_functor := {to_lax_monoidal_functor := (category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor, ε_is_iso := _, μ_is_iso := _}, braided' := _}

source

@[simp]

theorem category_theory.discrete.braided_functor_to_monoidal_functor {M : Type u} [comm_monoid M] {N : Type u} [comm_monoid N] (F : M →* N) :

(category_theory.discrete.braided_functor F).to_monoidal_functor = category_theory.discrete.monoidal_functor F

source

def category_theory.tensor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X Y : C × C) :

(category_theory.monoidal_category.tensor C).obj X ⊗ (category_theory.monoidal_category.tensor C).obj Y ⟶ (category_theory.monoidal_category.tensor C).obj (X ⊗ Y)

The strength of the tensor product functor from C × C to C.

Equations

category_theory.tensor_μ C X Y = (α_ X.fst X.snd (Y.fst ⊗ Y.snd)).hom ≫ (𝟙 X.fst ⊗ (α_ X.snd Y.fst Y.snd).inv) ≫ (𝟙 X.fst ⊗ (β_ X.snd Y.fst).hom ⊗ 𝟙 Y.snd) ≫ (𝟙 X.fst ⊗ (α_ Y.fst X.snd Y.snd).hom) ≫ (α_ X.fst Y.fst (X.snd ⊗ Y.snd)).inv

source

theorem category_theory.tensor_μ_def₁ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ Y₁ Y₂ : C) :

category_theory.tensor_μ C (X₁, X₂) (Y₁, Y₂) ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).hom ≫ (𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).inv) = (α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ Y₁ Y₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ Y₁).hom ⊗ 𝟙 Y₂)

source

theorem category_theory.tensor_μ_def₂ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ Y₁ Y₂ : C) :

(𝟙 X₁ ⊗ (α_ X₂ Y₁ Y₂).hom) ≫ (α_ X₁ X₂ (Y₁ ⊗ Y₂)).inv ≫ category_theory.tensor_μ C (X₁, X₂) (Y₁, Y₂) = (𝟙 X₁ ⊗ (β_ X₂ Y₁).hom ⊗ 𝟙 Y₂) ≫ (𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).hom) ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv

source

theorem category_theory.tensor_μ_natural (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁) (g₂ : U₂ ⟶ V₂) :

((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ category_theory.tensor_μ C (Y₁, Y₂) (V₁, V₂) = category_theory.tensor_μ C (X₁, X₂) (U₁, U₂) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)

source

theorem category_theory.tensor_left_unitality (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :

(λ_ (X₁ ⊗ X₂)).hom = ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ category_theory.tensor_μ C (𝟙_ C _inst_2, 𝟙_ C _inst_2) (X₁, X₂) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)

source

theorem category_theory.tensor_right_unitality (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :

(ρ_ (X₁ ⊗ X₂)).hom = (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ category_theory.tensor_μ C (X₁, X₂) (𝟙_ C _inst_2, 𝟙_ C _inst_2) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)

source

theorem category_theory.tensor_associativity_aux (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (W X Y Z : C) :

((β_ W X).hom ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X W (Y ⊗ Z)).hom ≫ (𝟙 X ⊗ (α_ W Y Z).inv) ≫ (𝟙 X ⊗ (β_ (W ⊗ Y) Z).hom) ≫ (𝟙 X ⊗ (α_ Z W Y).inv) = (𝟙 (W ⊗ X) ⊗ (β_ Y Z).hom) ≫ (α_ (W ⊗ X) Z Y).inv ≫ ((α_ W X Z).hom ⊗ 𝟙 Y) ≫ ((β_ W (X ⊗ Z)).hom ⊗ 𝟙 Y) ≫ ((α_ X Z W).hom ⊗ 𝟙 Y) ≫ (α_ X (Z ⊗ W) Y).hom

source

theorem category_theory.tensor_associativity (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :

(category_theory.tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫ category_theory.tensor_μ C (X₁ ⊗ Y₁, X₂ ⊗ Y₂) (Z₁, Z₂) ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (𝟙 (X₁ ⊗ X₂) ⊗ category_theory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂)) ≫ category_theory.tensor_μ C (X₁, X₂) (Y₁ ⊗ Z₁, Y₂ ⊗ Z₂)

source

@[simp]

theorem category_theory.tensor_monoidal_to_lax_monoidal_functor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X Y : C × C) :

(category_theory.tensor_monoidal C).to_lax_monoidal_functor.μ X Y = category_theory.tensor_μ C X Y

source

def category_theory.tensor_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.monoidal_functor (C × C) C

The tensor product functor from C × C to C as a monoidal functor.

Equations

category_theory.tensor_monoidal C = {to_lax_monoidal_functor := {to_functor := {obj := (category_theory.monoidal_category.tensor C).obj, map := (category_theory.monoidal_category.tensor C).map, map_id' := _, map_comp' := _}, ε := (λ_ (𝟙_ C)).inv, μ := λ (X Y : C × C), category_theory.tensor_μ C X Y, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

source

@[simp]

theorem category_theory.tensor_monoidal_to_lax_monoidal_functor_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(category_theory.tensor_monoidal C).to_lax_monoidal_functor.ε = (λ_ (𝟙_ C)).inv

source

@[simp]

theorem category_theory.tensor_monoidal_to_lax_monoidal_functor_to_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(category_theory.tensor_monoidal C).to_lax_monoidal_functor.to_functor = category_theory.monoidal_category.tensor C

source

theorem category_theory.left_unitor_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :

(λ_ X₁).hom ⊗ (λ_ X₂).hom = category_theory.tensor_μ C (𝟙_ C _inst_2, X₁) (𝟙_ C _inst_2, X₂) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (λ_ (X₁ ⊗ X₂)).hom

source

theorem category_theory.right_unitor_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :

(ρ_ X₁).hom ⊗ (ρ_ X₂).hom = category_theory.tensor_μ C (X₁, 𝟙_ C _inst_2) (X₂, 𝟙_ C _inst_2) ≫ (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).hom) ≫ (ρ_ (X₁ ⊗ X₂)).hom

source

theorem category_theory.associator_monoidal_aux (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (W X Y Z : C) :

(𝟙 W ⊗ (β_ X (Y ⊗ Z)).hom) ≫ (𝟙 W ⊗ (α_ Y Z X).hom) ≫ (α_ W Y (Z ⊗ X)).inv ≫ ((β_ W Y).hom ⊗ 𝟙 (Z ⊗ X)) = (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ ((β_ (W ⊗ X) Y).hom ⊗ 𝟙 Z) ≫ ((α_ Y W X).inv ⊗ 𝟙 Z) ≫ (α_ (Y ⊗ W) X Z).hom ≫ (𝟙 (Y ⊗ W) ⊗ (β_ X Z).hom)

source

theorem category_theory.associator_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :

category_theory.tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫ (category_theory.tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫ category_theory.tensor_μ C (X₁, X₂ ⊗ X₃) (Y₁, Y₂ ⊗ Y₃) ≫ (𝟙 (X₁ ⊗ Y₁) ⊗ category_theory.tensor_μ C (X₂, X₃) (Y₂, Y₃))

mathlib3 documentation

Braided and symmetric monoidal categories #

Implementation note #

Future work #