Propositions 3.8 and 4.14 for the algebra A₀ of Construction 2.8

prop:projective-ray-product (projective-rays.tex) and prop:scalar-normalization (scalar-normalization.tex) are stated for A₀, the projective corner of C = gr_J ind(mod A) ≅ k(Γ_A) for a basic representation-finite algebra A over an algebraically closed field. The general theorems (projectiveRayProduct for length-graded algebras with degree-zero local corners; MeshWalk.scalarNormalization for scalar mesh categories with mesh data) are instantiated here for the Auslander–Reiten mesh data of A (arMeshData), whose A₀ is representation-finite (isRepresentationFinite_A0).

theorem MultiplicativeBasisDeformations.IndSkeleton.projectiveRayProduct_A0 {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (v₀ : S.ARVertex) : have hF := ⋯; have F := MeshWalk.FpA0 (S.arMeshData b) v₀ hF; have G := MeshWalk.lenA0 (S.arMeshData b) ⋯; (∀ (x y : Fin F.m), ∀ f ∈ F.corner x y, f ≠ 0 → ∃ (g : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) (d : ℕ), G.IsHom d g ∧ g ≠ 0 ∧ g ∈ F.ray x y f ∧ ∀ g' ∈ F.ray x y f, ∀ (d' : ℕ), G.IsHom d' g' → g' ∈ k ∙ g) ∧ (∀ (x y z : Fin F.m) (f h : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) (p q : ℕ), G.IsHom p f → G.IsHom q h → (f * h ∈ F.insertionSpan x y z f h ↔ f * h = 0)) ∧ ∀ (x y z w : Fin F.m) (f g h : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ), f ∈ F.corner x y → f ≠ 0 → g ∈ F.corner y z → g ≠ 0 → h ∈ F.corner z w → h ≠ 0 → (f * g ∉ F.insertionSpan x y z f g ∧ f * g * h ∉ F.insertionSpan x z w (f * g) h ↔ g * h ∉ F.insertionSpan y z w g h ∧ f * (g * h) ∉ F.insertionSpan x y w f (g * h))

Proposition 3.8 for A₀ (prop:projective-ray-product): for A₀ of the Auslander–Reiten mesh category, with its length grading and labelled primitive idempotents, each nonzero ray contains a unique homogeneous line, products of homogeneous lines detect the ray products, and the ray table is associative.

theorem MultiplicativeBasisDeformations.IndSkeleton.scalarNormalization_A0 {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (v₀ : S.ARVertex) : have hF := ⋯; (MeshWalk.FpA0 (S.arMeshData b) v₀ hF).IsRayPres (MeshWalk.A0Mult (S.arMeshData b) v₀ hF) (MeshWalk.idxA0 (S.arMeshData b) v₀ hF) ⇑(MeshWalk.basisR (S.arMeshData b) v₀ hF) ∧ (∀ (t : MeshWalk.RayA0 (S.arMeshData b) v₀), (MeshWalk.thetaA0 (S.arMeshData b) v₀ hF) ((MeshWalk.A0Tab (S.arMeshData b) v₀ hF).b k t) = (MeshWalk.basisR (S.arMeshData b) v₀ hF) t) ∧ HasNormedMultiplicativeBasis k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ

Proposition 4.14 for A₀ (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.

theorem MultiplicativeBasisDeformations.IndSkeleton.projectiveEvaluation_equivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : (S.arMeshData b).evFunctor.IsEquivalence

Proposition 2.10(1) for A₀ (prop:projective-evaluation(1)): evaluation at the projective labels is an equivalence add C ≃ mod A₀ for the Auslander–Reiten mesh category.

theorem MultiplicativeBasisDeformations.IndSkeleton.gradedStandardForm_asStated {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (hbasic : IsBasicAlgebra A) (v₀ : S.ARVertex) : have hF := ⋯; IsRepresentationFinite k ↥((MeshWalk.A0Tab (S.arMeshData b) v₀ hF).Lin k) ∧ Nonempty (CatAlg.AddC (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b)) ≌ (CatAlg.MeshData.FGProp (↥((MeshWalk.A0Tab (S.arMeshData b) v₀ hF).Lin k))ᵐᵒᵖ).FullSubcategory) ∧ (S.IsStandard ↔ ∃ (b' : S.ArrowBases), Nonempty (A ≃ₐ[k] S.A0 b'))

Corollary 4.15 (cor:graded-standard-form) as stated: kP, for P = ray A₀, is representation-finite and add k(Γ_A) ≃ mod kP (evaluation, then A₀ ≅ kP); and A is standard if and only if A ≅ A₀.