The ray basis of a standard basic algebra

Corollary 5.5 (mesh-deformations.tex): "Construction 2.8 and Proposition 4.14 give A ≅ A₀ ≅ kP, where P = ray A₀. This isomorphism preserves endpoint actions and the subspaces M(f,h) of Definition 3.4, and therefore identifies ray A with P. The ray basis is multiplicative, contains the primitive idempotents, and intersects every radical power in a basis by Corollary 3.3."

Here: the ray basis of A₀ (exists_hasRayBasis_A0) is transported along A ≅ A₀ (hasRayBasis_of_algEquiv) to the pulled-back vertex idempotents, and then, by conjugacy of complete sets of primitive idempotents in a basic algebra, to any given complete set F.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.comap {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] {B : Type u} [Ring B] [Algebra k B] (φ : A ≃ₐ[k] B) (F : PrimitiveIdempotents B) : PrimitiveIdempotents A

The idempotents pulled back along an algebra isomorphism.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.hasRayBasis_of_subsingleton {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [Subsingleton A] (F : PrimitiveIdempotents A) : HasRayBasis k F

A trivial algebra has a ray basis (there are no nonzero rays).

theorem MultiplicativeBasisDeformations.IndSkeleton.hasRayBasis_of_isStandard {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (hbasic : IsBasicAlgebra A) (hstd : S.IsStandard) (F : PrimitiveIdempotents A) : PrimitiveIdempotents.HasRayBasis k F

A standard basic algebra has a ray basis for every complete set of primitive orthogonal idempotents (Corollary 5.5).