Braided and symmetric structure on the matrix envelope

When C is a braided (resp. symmetric) monoidal preadditive category, so is Mat_ C. The braiding on Mat_ C is a "diagonal" matrix carrying the componentwise braidings of C, reindexed by the swap M.ι × N.ι ↔ N.ι × M.ι.

Componentwise access to the Mat_ C monoidal structure

Braiding data for Mat_ C

noncomputable def RS.matBraidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mat_ C) : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N M

The matrix morphism that swaps tensor factors using the component braidings.

Equations

• RS.matBraidHom M N (i₁, i₂) (j₁, j₂) = if hi : i₂ = j₁ then if hj : i₁ = j₂ then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (β_ (M.X j₂) (N.X j₁)).hom else 0 else 0

noncomputable def RS.matBraidInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mat_ C) : CategoryTheory.MonoidalCategoryStruct.tensorObj N M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M N

The inverse matrix morphism that swaps tensor factors by inverse braidings.

Equations

• RS.matBraidInv M N (j₁, j₂) (i₁, i₂) = if hj₁ : j₁ = i₂ then if hj₂ : j₂ = i₁ then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (β_ (M.X i₁) (N.X i₂)).inv else 0 else 0

Braiding iso

noncomputable def RS.matBraidIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mat_ C) : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj N M

The braiding isomorphism on matrix objects induced by the component braidings.

Equations

• RS.matBraidIso M N = { hom := RS.matBraidHom M N, inv := RS.matBraidInv M N, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Braiding naturality

Hexagon identities

BraidedCategory instance

@[instance_reducible]

noncomputable instance RS.matBraided {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory (CategoryTheory.Mat_ C)

The matrix category inherits a braiding: the componentwise braidings, reindexed by the swap of index products.

Equations

• RS.matBraided = { braiding := RS.matBraidIso, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }

SymmetricCategory instance

@[instance_reducible]

noncomputable instance RS.matSymmetric {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory (CategoryTheory.Mat_ C)

And a symmetric one stays symmetric.

Equations

• RS.matSymmetric = { toBraidedCategory := RS.matBraided, symmetry := ⋯ }