The ray basis of A₀

Proposition 3.8 and Proposition 4.14 for A₀: the homogeneous normed multiplicative basis of A₀ (A0Normed.lean) is, after reindexing by the nonzero rays, a ray transversal killing zero ray products. This is the ray table P = ray A₀ with A₀ ≅ kP (exists_hasRayBasis_A0).

theorem MultiplicativeBasisDeformations.MeshWalk.exists_hasRayBasis_A0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : ∃ (Fp : PrimitiveIdempotents (CatAlg.Alg D.F0)ᵐᵒᵖ), PrimitiveIdempotents.HasRayBasis k Fp

A₀ has a ray basis for its vertex idempotents.