Atomic idempotents in semisimple complex algebras

Every finite-dimensional semisimple ℂ-algebra has a complete orthogonal family of idempotents whose corners are the scalar lines they span: pull back the diagonal matrix units through Wedderburn–Artin. These are the atoms along which Karoubi objects split into simples.

structure RS.IsAtomicIdempotent {A : Type u} [Ring A] [Algebra ℂ A] (e : A) : Prop

An idempotent is atomic if it is nonzero and its corner is the scalar line it spans.

• idem : IsIdempotentElem e
• ne_zero : e ≠ 0
• corner_scalar (x : A) : ∃ (c : ℂ), e * x * e = c • e

theorem RS.exists_completeOrthogonal_atomic {A : Type u} [Ring A] [Algebra ℂ A] [FiniteDimensional ℂ A] [IsSemisimpleRing A] : ∃ (ι : Type) (x : Fintype ι) (e : ι → A), CompleteOrthogonalIdempotents e ∧ ∀ (i : ι), IsAtomicIdempotent (e i)

Atomic decomposition of a finite-dimensional semisimple complex algebra: the identity splits into a complete orthogonal family of atomic idempotents.