Complete sets of primitive orthogonal idempotents

Every idempotent of a finite-dimensional algebra is a sum of pairwise orthogonal primitive idempotents: split a nonprimitive idempotent f as g + (f - g) with g an idempotent of the corner fAf, and induct on dim fA. In particular a finite-dimensional algebra has a complete set of primitive orthogonal idempotents (exists_primitive_decomposition), as used in Lemma 2.1 (graded-category.tex).

def MultiplicativeBasisDeformations.leftIdealSpace {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (f : A) : Submodule k A

The subspace fA.

theorem MultiplicativeBasisDeformations.mem_leftIdealSpace {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {f x : A} : x ∈ leftIdealSpace f ↔ ∃ (a : A), f * a = x

theorem MultiplicativeBasisDeformations.leftIdealSpace_lt {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] {f g : A} (hf : IsIdempotentElem f) (hg : IsIdempotentElem g) (hfg : f * g = g) (hgf : g * f = g) (hne : g ≠ f) : leftIdealSpace g < leftIdealSpace f

def MultiplicativeBasisDeformations.IsPrimDecomp {A : Type v} [Ring A] (f : A) (l : List A) : Prop

The data of a decomposition of f into orthogonal primitive idempotents.

theorem MultiplicativeBasisDeformations.exists_primDecomp_aux (k : Type u) [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (d : ℕ) (f : A) : IsIdempotentElem f → Module.finrank k ↥(leftIdealSpace f) = d → ∃ (l : List A), IsPrimDecomp f l

theorem MultiplicativeBasisDeformations.exists_primitive_decomposition (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] [FiniteDimensional k A] : ∃ (n : ℕ) (e : Fin n → A), CompleteOrthogonalIdempotents e ∧ ∀ (i : Fin n), IsPrimitiveIdempotent (e i)

A finite-dimensional algebra has a complete set of primitive orthogonal idempotents.