Monoidal, braided, additive, and linear structure on Mat_.embedding C

When C is a monoidal preadditive category, the embedding functor Mat_.embedding C : C ⥤ Mat_ C is strong monoidal, braided (when C is braided), additive, and ℂ-linear (when C is linear).

The key observation is that the embedding sends X to the one-by-one matrix ⟨PUnit, fun _ => X⟩, so all index types in sight are products of PUnit (hence subsingletons). Every structural morphism is therefore a single-entry diagonal matrix carrying the identity of the appropriate tensor product, and all coherence proofs collapse immediately.

We use Functor.CoreMonoidal to avoid manually proving the oplax coherence conditions: from εIso, μIso, and the lax axioms, mathlib automatically derives the full Functor.Monoidal structure including the OplaxMonoidal fields.

The embedding is additive

Mathlib already provides (Mat_.embedding C).Additive.

The embedding is ℂ-linear

instance RS.matEmbeddingLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] : CategoryTheory.Functor.Linear ℂ (CategoryTheory.Mat_.embedding C)

The embedding into the matrix category is ℂ-linear.

Naturality and coherence lemmas

Associativity

Unitality

The CoreMonoidal structure and Monoidal instance

noncomputable def RS.matEmbCoreMonoidal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : (CategoryTheory.Mat_.embedding C).CoreMonoidal

The CoreMonoidal structure on Mat_.embedding C, providing isomorphisms εIso : 𝟙_ (Mat_ C) ≅ (Mat_.embedding C).obj (𝟙_ C), the identity since these coincide, and μIso X Y : emb X ⊗ emb Y ≅ emb (X ⊗ Y) from matEmbTensorIso.

Equations

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

@[instance_reducible]

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

The embedding Mat_.embedding C is strong monoidal. The full Monoidal structure, OplaxMonoidal coherence included, comes from CoreMonoidal.

Equations

• RS.matEmbeddingMonoidal = RS.matEmbCoreMonoidal.toMonoidal

The braided structure on Mat_.embedding C

@[instance_reducible]

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

The embedding Mat_.embedding C is braided when C is braided.

Equations

• RS.matEmbeddingBraided = { toMonoidal := RS.matEmbeddingMonoidal, braided := ⋯ }