Semisimplicity of the envelope

The Deligne semisimplicity hypothesis for the envelope: every object is a finite biproduct of simple objects. The endomorphism algebra is finite-dimensional and semisimple by the factorial trace obstruction, so the identity splits into a complete orthogonal family of atomic idempotents; each cuts out a corner object with scalar endomorphisms, which is simple because monomorphisms split in the envelope, and the object is the biproduct of its corners.

Corner cuts of Karoubi objects (general)

noncomputable def RS.karoubiCorner {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : CategoryTheory.Idempotents.Karoubi D

The corner object cut out of a Karoubi object by an idempotent endomorphism.

Equations

• RS.karoubiCorner X he = { X := X.X, p := e.f, idem := ⋯ }

noncomputable def RS.cornerIncl {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : karoubiCorner X he ⟶ X

The corner inclusion.

Equations

• RS.cornerIncl X he = { f := e.f, comm := ⋯ }

noncomputable def RS.cornerProj {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : X ⟶ karoubiCorner X he

The corner projection.

Equations

• RS.cornerProj X he = { f := e.f, comm := ⋯ }

theorem RS.cornerIncl_proj {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : CategoryTheory.CategoryStruct.comp (cornerIncl X he) (cornerProj X he) = CategoryTheory.CategoryStruct.id (karoubiCorner X he)

The corner is a retract: including then projecting is the identity on it.

theorem RS.cornerProj_incl {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : CategoryTheory.CategoryStruct.comp (cornerProj X he) (cornerIncl X he) = e

Projecting then including is the idempotent.

theorem RS.cornerIncl_absorb {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : CategoryTheory.CategoryStruct.comp (cornerIncl X he) e = cornerIncl X he

The inclusion is absorbed by the idempotent.

theorem RS.cornerProj_absorb {D : Type u} [CategoryTheory.Category.{v, u} D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) : CategoryTheory.CategoryStruct.comp e (cornerProj X he) = cornerProj X he

And so is the projection.

theorem RS.cornerIncl_proj_orthogonal {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] (X : CategoryTheory.Idempotents.Karoubi D) {e : CategoryTheory.End X} (he : IsIdempotentElem e) {e' : CategoryTheory.End X} (he' : IsIdempotentElem e') (horth : e' * e = 0) : CategoryTheory.CategoryStruct.comp (cornerIncl X he) (cornerProj X he') = 0

Cross-composites of distinct orthogonal corners vanish.

Scalar corners are simple in the envelope

theorem RS.env_simple_of_scalar_end {R : ℕ} (f : EdgeRankParameter R) (E : Env f) (hne : CategoryTheory.CategoryStruct.id E ≠ 0) (hsc : ∀ (x : CategoryTheory.End E), ∃ (c : ℂ), x = c • CategoryTheory.CategoryStruct.id E) : CategoryTheory.Simple E

An envelope object with scalar endomorphism algebra and nonzero identity is simple: monomorphisms split, and a split idempotent scalar is 0 or 1.

The atomic corners of an envelope object

theorem RS.env_corner_scalar {R : ℕ} (f : EdgeRankParameter R) (E : Env f) {e : CategoryTheory.End E} (he : IsAtomicIdempotent e) (x : CategoryTheory.End (karoubiCorner E ⋯)) : ∃ (c : ℂ), x = c • CategoryTheory.CategoryStruct.id (karoubiCorner E ⋯)

The corner cut by an atomic idempotent has scalar endomorphisms.

theorem RS.env_corner_id_ne_zero {R : ℕ} (f : EdgeRankParameter R) (E : Env f) {e : CategoryTheory.End E} (he : IsAtomicIdempotent e) : CategoryTheory.CategoryStruct.id (karoubiCorner E ⋯) ≠ 0

The corner cut by an atomic idempotent has nonzero identity.

The biproduct decomposition

theorem RS.env_deligneSemisimple {R : ℕ} (f : EdgeRankParameter R) : IsSemisimple (Env f)

Semisimplicity of the envelope: every object is a finite biproduct of simple objects.