The trace criterion on a Karoubi corner #
Nilpotence transports along the underlying-morphism map. Cyclicity sandwiches arbitrary ambient tests into the corner, so a nondegenerate trace that kills nilpotents proves semisimplicity of every corner endomorphism algebra.
theorem
RS.karoubiEnd_isNilpotent
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{P : CategoryTheory.Idempotents.Karoubi C}
{x : CategoryTheory.End P}
(hx : IsNilpotent x)
:
IsNilpotent
(have this := x.f;
this)
Nilpotent corner endomorphisms are nilpotent in the base category.
theorem
RS.karoubiEnd_isSemisimpleRing_of_trace
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear ℂ C]
(P : CategoryTheory.Idempotents.Karoubi C)
[FiniteDimensional ℂ (CategoryTheory.End P.X)]
(τ : CategoryTheory.End P.X →ₗ[ℂ] ℂ)
(hnil : ∀ (x : CategoryTheory.End P.X), IsNilpotent x → τ x = 0)
(hcyc :
∀ (a b : CategoryTheory.End P.X),
τ (CategoryTheory.CategoryStruct.comp a b) = τ (CategoryTheory.CategoryStruct.comp b a))
(hnd :
∀ (a : CategoryTheory.End P.X),
(∀ (b : CategoryTheory.End P.X), τ (CategoryTheory.CategoryStruct.comp a b) = 0) → a = 0)
:
A finite-dimensional ambient trace criterion restricts to a Karoubi corner.