Normed multiplicative bases and basic algebras

Definition 1.1 of the manuscript (main.tex): a basis 𝓑 of a finite-dimensional algebra A is multiplicative if bc ∈ 𝓑 ∪ {0} for all b, c ∈ 𝓑; it is normed if it contains a complete set of primitive orthogonal idempotents and 𝓑 ∩ (rad A)^n is a basis of (rad A)^n for every n ≥ 1.

The algebra radical rad A is Mathlib's Jacobson radical Ring.jacobson A (the intersection of the maximal left ideals), regarded as a k-subspace. Its powers are products of k-subspaces, which agree with the ideal powers because rad A is a two-sided ideal.

def MultiplicativeBasisDeformations.algebraRadical (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] : Submodule k A

The algebra radical rad A, as a k-subspace of A.

def MultiplicativeBasisDeformations.algebraRadicalPow (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] (n : ℕ) : Submodule k A

The radical power (rad A)^n, as a k-subspace of A.

def MultiplicativeBasisDeformations.IsPrimitiveIdempotent {A : Type v} [Ring A] (e : A) : Prop

A primitive idempotent: a nonzero idempotent e such that the only idempotents of the corner eAe are 0 and e.

def MultiplicativeBasisDeformations.IsMultiplicativeBasis {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {ι : Type u_1} (b : Module.Basis ι k A) : Prop

A basis is multiplicative if the product of two basis elements is zero or a basis element.

structure MultiplicativeBasisDeformations.IsNormedMultiplicativeBasis {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {ι : Type u_1} (b : Module.Basis ι k A) : Prop

Definition 1.1 (def:normed-multiplicative-basis). A normed multiplicative basis: multiplicative, containing a complete set of primitive orthogonal idempotents, and meeting every radical power (rad A)^n, n ≥ 1, in a basis of that power.

• multiplicative : IsMultiplicativeBasis b
• idempotents : ∃ (E : Finset ι), (CompleteOrthogonalIdempotents fun (i : ↥E) => b ↑i) ∧ ∀ i ∈ E, IsPrimitiveIdempotent (b i)
• radicalPow (n : ℕ) : 1 ≤ n → Submodule.span k (⇑b '' {i : ι | b i ∈ algebraRadicalPow k A n}) = algebraRadicalPow k A n

def MultiplicativeBasisDeformations.HasNormedMultiplicativeBasis (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] : Prop

A has a normed multiplicative basis.

def MultiplicativeBasisDeformations.IsBasicAlgebra (A : Type v) [Ring A] : Prop

A is basic: it has a complete set of primitive orthogonal idempotents whose principal right ideals e_i A are pairwise nonisomorphic. Here e_i A ≅ e_j A is expressed by elements x ∈ e_i A e_j, y ∈ e_j A e_i with xy = e_i and yx = e_j.