The matrix-envelope trace and semisimplicity

The diagonal trace on endomorphisms of matrix-envelope objects: linear, cyclic, and nondegenerate (entrywise, via single-entry test matrices). Semisimplicity of every End M follows from the trace criterion once nilpotents are known to have vanishing trace, which the atom decomposition supplies.

Linear structure on the matrix envelope

@[instance_reducible]

noncomputable instance RS.matHomSMul {R : ℕ} (f : EdgeRankParameter R) (M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : SMul ℂ (M ⟶ N)

Scaling a matrix of morphisms entrywise.

Equations

• RS.matHomSMul f M N = { smul := fun (c : ℂ) (φ : M ⟶ N) (i : M.ι) (j : N.ι) => c • φ i j }

@[instance_reducible]

noncomputable instance RS.matHomModule {R : ℕ} (f : EdgeRankParameter R) (M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : Module ℂ (M ⟶ N)

The matrix layer's hom-sets are ℂ-modules.

Equations

• RS.matHomModule f M N = { toSMul := RS.matHomSMul f M N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

noncomputable instance RS.matLinear {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Linear ℂ (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f)))

Hence the matrix layer is ℂ-linear.

Equations

• RS.matLinear f = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

The diagonal trace

noncomputable def RS.matTrace {R : ℕ} (f : EdgeRankParameter R) (M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : CategoryTheory.End M →ₗ[ℂ] ℂ

The diagonal trace on matrix-envelope endomorphisms.

Equations

• RS.matTrace f M = { toFun := fun (φ : CategoryTheory.End M) => ∑ i : M.ι, (RS.HomSpace.traceMap f.val (M.X i).X.arity) (φ i i).f, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.matTrace_comp_comm {R : ℕ} (f : EdgeRankParameter R) {M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (α : M ⟶ N) (β : N ⟶ M) : (matTrace f M) (CategoryTheory.CategoryStruct.comp α β) = (matTrace f N) (CategoryTheory.CategoryStruct.comp β α)

Cyclicity of the diagonal trace.

Single-entry tests and nondegeneracy

theorem RS.matEnd_eq_zero_of_traces_vanish {R : ℕ} (f : EdgeRankParameter R) {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (φ : CategoryTheory.End M) (hφ : ∀ (ψ : CategoryTheory.End M), (matTrace f M) (ψ * φ) = 0) : φ = 0

Nondegeneracy of the diagonal trace.

Finiteness and the semisimplicity criterion

instance RS.karoubiHomFinite {R : ℕ} (f : EdgeRankParameter R) (P Q : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : FiniteDimensional ℂ (P ⟶ Q)

Karoubi hom-spaces are finite-dimensional, being subspaces of the skein hom-spaces.

instance RS.matHomFinite {R : ℕ} (f : EdgeRankParameter R) (M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : FiniteDimensional ℂ (M ⟶ N)

So are matrix hom-spaces, being finite products of them.

instance RS.matEndFinite {R : ℕ} (f : EdgeRankParameter R) (M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : FiniteDimensional ℂ (CategoryTheory.End M)

In particular every matrix endomorphism algebra is finite-dimensional — the standing hypothesis of the trace criterion.