Monoidal structure on the matrix envelope

When C is a monoidal preadditive category (i.e. a preadditive category with a monoidal structure such that the tensor product is bilinear on morphisms), the matrix category Mat_ C inherits a monoidal structure:

• Objects: M ⊗ N = (M.ι × N.ι, fun p => M.X p.1 ⊗ N.X p.2).
• Morphisms: the Kronecker product — entry (i₁,i₂),(j₁,j₂) of f ⊗ₘ g is f i₁ j₁ ⊗ₘ g i₂ j₂.
• Unit: (PUnit, fun _ => 𝟙_ C).
• Structural isomorphisms: diagonal matrices carrying the componentwise associators/unitors of C, with index-type reindexing by Equiv.prodAssoc, Equiv.punitProd, Equiv.prodPUnit.

The interchange law (tensorHom_comp_tensorHom) holds because matrix multiplication turns into iterated sums that factor via tensor_sum and sum_tensor (the MonoidalPreadditive hypothesis). The pentagon and triangle identities reduce componentwise to the corresponding identities in C.

Tensor product data on Mat_ C

@[reducible]

def RS.matTensorObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (M N : CategoryTheory.Mat_ C) : CategoryTheory.Mat_ C

Tensor product of objects in Mat_ C: index by the product, with componentwise tensor in C.

Equations

• RS.matTensorObj M N = { ι := M.ι × N.ι, fintype := instFintypeProd M.ι N.ι, X := fun (p : M.ι × N.ι) => CategoryTheory.MonoidalCategoryStruct.tensorObj (M.X p.1) (N.X p.2) }

def RS.matTensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] {M₁ N₁ M₂ N₂ : CategoryTheory.Mat_ C} (f : M₁ ⟶ N₁) (g : M₂ ⟶ N₂) : matTensorObj M₁ M₂ ⟶ matTensorObj N₁ N₂

Tensor product of morphisms in Mat_ C: the Kronecker product.

Equations

• RS.matTensorHom f g (j₁, j₂) (j₁_1, j₂_1) = CategoryTheory.MonoidalCategoryStruct.tensorHom (f j₁ j₁_1) (g j₂ j₂_1)

@[reducible]

def RS.matTensorUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Mat_ C

The tensor unit in Mat_ C.

Equations

• RS.matTensorUnit = { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => CategoryTheory.MonoidalCategoryStruct.tensorUnit C }

Structural isomorphisms

The associator and unitors are "diagonal" morphisms: given an equivalence of index types, the entry at (i, e i) is the corresponding structural morphism of C, and all other entries are zero.

noncomputable def RS.matAssocHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M N K : CategoryTheory.Mat_ C) : matTensorObj (matTensorObj M N) K ⟶ matTensorObj M (matTensorObj N K)

The associator hom in Mat_ C.

Equations

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

noncomputable def RS.matAssocInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M N K : CategoryTheory.Mat_ C) : matTensorObj M (matTensorObj N K) ⟶ matTensorObj (matTensorObj M N) K

The associator inv in Mat_ C.

Equations

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

noncomputable def RS.matLeftUnitorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mat_ C) : matTensorObj matTensorUnit M ⟶ M

The left unitor hom in Mat_ C.

Equations

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

noncomputable def RS.matLeftUnitorInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mat_ C) : M ⟶ matTensorObj matTensorUnit M

The left unitor inv in Mat_ C.

Equations

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

noncomputable def RS.matRightUnitorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mat_ C) : matTensorObj M matTensorUnit ⟶ M

The right unitor hom in Mat_ C.

Equations

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

noncomputable def RS.matRightUnitorInv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mat_ C) : M ⟶ matTensorObj M matTensorUnit

The right unitor inv in Mat_ C.

Equations

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

Isomorphism proofs for the structural morphisms

Diagonal ≫ diagonal collapses to a single summand: all off-diagonal entries in the intermediate sum vanish. Finset.sum_eq_single_of_mem identifies the unique nonzero term, and the on-diagonal entry then simplifies.

noncomputable def RS.matAssociator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M N K : CategoryTheory.Mat_ C) : matTensorObj (matTensorObj M N) K ≅ matTensorObj M (matTensorObj N K)

The associator isomorphism in Mat_ C.

Equations

• RS.matAssociator M N K = { hom := RS.matAssocHom M N K, inv := RS.matAssocInv M N K, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.matLeftUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mat_ C) : matTensorObj matTensorUnit M ≅ M

The left unitor isomorphism in Mat_ C.

Equations

• RS.matLeftUnitor M = { hom := RS.matLeftUnitorHom M, inv := RS.matLeftUnitorInv M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.matRightUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mat_ C) : matTensorObj M matTensorUnit ≅ M

The right unitor isomorphism in Mat_ C.

Equations

• RS.matRightUnitor M = { hom := RS.matRightUnitorHom M, inv := RS.matRightUnitorInv M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

MonoidalCategoryStruct instance

@[instance_reducible]

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

The monoidal data on the matrix category: index products on objects, Kronecker products on morphisms.

Equations

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

MonoidalCategory instance

We use MonoidalCategory.ofTensorHom which requires proofs of the interchange law, naturality of structural isomorphisms, and the pentagon and triangle coherence identities. Each proof goes pointwise via Mat_.hom_ext, collapses diagonal sums via Finset.sum_eq_single_of_mem, and reduces to the corresponding axiom in C.

Pentagon and triangle coherences

Both proofs go pointwise via Mat_.hom_ext, fully unfold the structural morphisms to nested dite expressions, use dite_comp/comp_dite/ tensor_dite/dite_tensor to push compositions inside the dites, decompose product sums into iterated sums, and then collapse each sum via Finset.sum_dite_irrel + Fintype.sum_dite_eq'. After all sums are gone both sides reduce to the corresponding coherence in C.

@[instance_reducible]

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

The monoidal structure on Mat_ C induced by the componentwise tensor product and Kronecker product of morphisms.

Equations

• RS.matMonoidal = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem RS.mat_comp_XYZ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] {A D : CategoryTheory.Mat_ C} (X Y Z : CategoryTheory.Mat_ C) (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ D) (i : A.ι) (d : D.ι) : CategoryTheory.CategoryStruct.comp f g i d = ∑ ax : X.ι, ∑ ay : Y.ι, ∑ az : Z.ι, CategoryTheory.CategoryStruct.comp (f i (ax, ay, az)) (g (ax, ay, az) d)

Composition through a right-associated triple tensor, entry by entry.

theorem RS.mat_comp_XY_Z_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] {A D : CategoryTheory.Mat_ C} (X Y Z : CategoryTheory.Mat_ C) (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ⟶ D) (i : A.ι) (d : D.ι) : CategoryTheory.CategoryStruct.comp f g i d = ∑ ax : X.ι, ∑ ay : Y.ι, ∑ az : Z.ι, CategoryTheory.CategoryStruct.comp (f i ((ax, ay), az)) (g ((ax, ay), az) d)

And through a left-associated one — the two sides of the pentagon.

theorem RS.mat_comp_tensor_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] {A B₁ B₂ D : CategoryTheory.Mat_ C} (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B₁ B₂) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj B₁ B₂ ⟶ D) (i : A.ι) (k : D.ι) : CategoryTheory.CategoryStruct.comp f g i k = ∑ j₁ : B₁.ι, ∑ j₂ : B₂.ι, CategoryTheory.CategoryStruct.comp (f i (j₁, j₂)) (g (j₁, j₂) k)

Composition through a tensor of two objects, entry by entry.