Proposition 4.14: A₀ ≅ kP with P = ray A₀

scalar-normalization.tex (prop:scalar-normalization): "For A₀ of Construction 2.8 and P = ray A₀, there is an isomorphism A₀ ≅ kP preserving the labelled primitive idempotents and homogeneous ray lines. In particular A₀ has a normed multiplicative basis."

The table A0Mult of the normed ray basis basisR is the ray table of A₀ in the sense of Definition 3.9: it presents the rays of A₀ (A0Mult_rayPres; each ray contains a unique homogeneous line, Proposition 3.8, and homogeneous lines are the lines of basisR, eq_smul_basisR). With thetaA0 : kP ≃ A₀ (b_t ↦ basisR t, identities to the labelled idempotents) this is the proposition (scalarNormalization).

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.smul_mem_ray_self {k : Type u} [Field k] [IsAlgClosed k] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (F : PrimitiveIdempotents B) {x y : Fin F.m} {f : B} (hf : f ∈ F.corner x y) {t : k} (ht : t ≠ 0) : t • f ∈ F.ray x y f

Nonzero multiples stay in the ray.

theorem MultiplicativeBasisDeformations.MeshWalk.finiteDimensional_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)ᵐᵒᵖ) : FiniteDimensional k (CatAlg.Alg D.F0)ᵐᵒᵖ

theorem MultiplicativeBasisDeformations.MeshWalk.A0Mult_rayPres {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)ᵐᵒᵖ) : (FpA0 D v₀ hF).IsRayPres (A0Mult D v₀ hF) (idxA0 D v₀ hF) ⇑(basisR D v₀ hF)

P = ray A₀: the table of the normed ray basis presents the rays of A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.scalarNormalization {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)ᵐᵒᵖ) : (FpA0 D v₀ hF).IsRayPres (A0Mult D v₀ hF) (idxA0 D v₀ hF) ⇑(basisR D v₀ hF) ∧ (∀ (t : RayA0 D v₀), (thetaA0 D v₀ hF) ((A0Tab D v₀ hF).b k t) = (basisR D v₀ hF) t) ∧ (∀ (x : D.PV), (thetaA0 D v₀ hF) ((A0Tab D v₀ hF).b k ((A0Tab D v₀ hF).e x)) = MulOpposite.op (CatAlg.unitM x x (CategoryTheory.CategoryStruct.id (D.F0 x)))) ∧ (∀ (t : RayA0 D v₀), (lenA0 D ⋯).IsHom (dA D v₀ t) ((basisR D v₀ hF) t)) ∧ HasNormedMultiplicativeBasis k (CatAlg.Alg D.F0)ᵐᵒᵖ

Proposition 4.14 (prop:scalar-normalization): A₀ ≅ kP for P = ray A₀, preserving the labelled primitive idempotents and the homogeneous ray lines; A₀ has a normed multiplicative basis.