Proposition 8.2 in every characteristic

local-ray-geometry.tex (prop:table-weight-lifting): "Let T be a weighted multiplication table whose linearization kT is representation-finite over the algebraically closed field k. Every additive weight T → ℤ/2 lifts to an additive weight T → ℤ."

The induction of Induction.lean proves this in characteristic two. Here, in every characteristic: a connected table presents kT (self_rayPres), and so does the ray table of the algebra A₀ of kT (rayA_eq_rayA0, Theorem 11.8(1)); the latter has the lifting property (A0Mult_lift2, W(P) free), which passes along the comparison of the two presentations (IsRayPres.lift2). Disconnected tables split along a component (lift2_of_split).

theorem MultiplicativeBasisDeformations.lift2_conn_any {k : Type u} [Field k] [IsAlgClosed k] {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (T : RaySys.Tab V R L) (hfin : IsRepresentationFinite k ↥(T.Lin k)) (hc : T.Conn) (hV : Nonempty V) : T.Lift2

The connected case, in every characteristic.

theorem MultiplicativeBasisDeformations.tableWeightLifting {k : Type u} [Field k] [IsAlgClosed k] {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (T : RaySys.Tab V R L) (hfin : IsRepresentationFinite k ↥(T.Lin k)) : T.Lift2

Proposition 8.2 (prop:table-weight-lifting), in every characteristic: every additive weight modulo two of a table with representation-finite linearization lifts to ℤ.

theorem MultiplicativeBasisDeformations.dimensionInduction {k : Type u} [Field k] [IsAlgClosed k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (hn : Nontrivial A) : (∀ (F : PrimitiveIdempotents A), ∃ (b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsNormedMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b) ∧ ∀ (S : IndSkeleton k A), ∃ (b : S.ArrowBases) (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) (F : PrimitiveIdempotents A) (ι : (S.arMeshData b).PV ≃ Fin F.m) (β : S.rayA0AR b v₀ → A), F.IsRayPres (S.A0MultAR b v₀ hF) ι β ∧ Module.Free ℤ (S.A0MultAR b v₀ hF).W

Proposition 8.3 (prop:dimension-induction), in every characteristic: for a basic representation-finite algebra A, (1) A has a normed multiplicative basis consisting of one representative of each nonzero ray (finalBasis_ray); (2) the initial-form bijection identifies the products in ray A and ray A₀ (rayA_initialForms); (3) ray A is presented by the table of A₀, whose weight group is free abelian (W_A0_free).