Semisimplicity of Karoubi endomorphism algebras

The endomorphism algebra of any object of the Karoubi envelope of the skein category is a corner e·End(n)·e, and the trace criterion restricts: corner-nilpotents are ambient-nilpotents, and cyclicity moves the idempotent across products, so ambient nondegeneracy restricts to the corner.

The endomorphism algebras of Karoubi objects

@[instance_reducible]

noncomputable instance RS.karoubiEndRing {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : Ring (CategoryTheory.End X)

Endomorphisms of a Karoubi object form a ring.

Equations

• RS.karoubiEndRing f X = inferInstance

@[instance_reducible]

noncomputable instance RS.karoubiEndAlgebra {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : Algebra ℂ (CategoryTheory.End X)

And a ℂ-algebra — the corner e·End(n)·e.

Equations

• RS.karoubiEndAlgebra f X = inferInstance

instance RS.karoubiEndFinite {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : FiniteDimensional ℂ (CategoryTheory.End X)

Finite-dimensional, as a subspace of the ambient skein endomorphisms.

theorem RS.karoubiEnd_isSemisimpleRing_of_nilpotent_trace {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) (hnil : ∀ (g : skeinEnd f X.X.arity), IsNilpotent g → skeinTrace f X.X.arity g = 0) : IsSemisimpleRing (CategoryTheory.End X)

The corner trace criterion, given nilpotent-trace vanishing in the ambient strand algebra.

theorem RS.karoubiEnd_isSemisimpleRing {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : IsSemisimpleRing (CategoryTheory.End X)

Semisimplicity of Karoubi endomorphism algebras, by the factorial trace obstruction.

theorem RS.karoubiEnd_isSemisimpleRing_factorial {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : IsSemisimpleRing (CategoryTheory.End X)

The mainline Karoubi semisimplicity theorem, with the factorial proof method explicit in its name.

Mixed-Hom nondegeneracy in the Karoubi envelope

theorem RS.karoubiHom_eq_zero_of_traces_vanish {R : ℕ} (f : EdgeRankParameter R) {X Y : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (a : X ⟶ Y) (ha : ∀ (b : Y ⟶ X), (HomSpace.traceMap f.val X.X.arity) (CategoryTheory.CategoryStruct.comp a.f b.f) = 0) : a = 0

A Karoubi morphism all of whose composite traces against reverse morphisms vanish is zero: the separation engine for the simples.