The dimension induction (Proposition 8.3) in characteristic two

main-theorems.tex. The induction is run on representation-finite ray tables T (Definition 3.9: kT is its own ray linearization). Its conclusion is the weight lifting property of T (Proposition 8.3(3), in the form hW used by Theorem 9.1):

• a disconnected table splits into two unions of components with fewer rays;
• for a connected table, B = kT is basic and representation-finite; the characteristic-two step (exists_normedRayBasis_char2) presents B by the ray table P of its algebra A₀ (Proposition 8.3(2)), and T presents B as well (self_rayPres); so the two tables are isomorphic (Lemma 3.6), P is connected, and its weights lift by Proposition 7.2.

Corollary 10.5 enters the characteristic-two step and itself uses the induction hypothesis (through Lemma 9.2 and Theorem 9.1); here it is the hypothesis Cor105Hyp.

def MultiplicativeBasisDeformations.LiftBelow (k : Type u) [Field k] (n : ℕ) : Prop

Weight lifting for every representation-finite ray table with fewer than n rays.

def MultiplicativeBasisDeformations.Cor105Hyp (k : Type u) [Field k] [IsAlgClosed k] : Prop

Corollary 10.5 under the induction hypothesis, for every basic representation-finite algebra.

theorem MultiplicativeBasisDeformations.ne_zero_of_complete {B : Type u} [Ring B] [Nontrivial B] {n : ℕ} {e : Fin n → B} (he : CompleteOrthogonalIdempotents e) : n ≠ 0

theorem MultiplicativeBasisDeformations.lift2_conn {k : Type u} [Field k] [IsAlgClosed k] (h2 : 2 = 0) (hcor : Cor105Hyp 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) (hIH : LiftBelow k (Fintype.card R)) : T.Lift2

The connected case of the induction.

theorem MultiplicativeBasisDeformations.LiftBelow.mono {k : Type u} [Field k] [IsAlgClosed k] {m n : ℕ} (h : LiftBelow k n) (hmn : m ≤ n) : LiftBelow k m

theorem MultiplicativeBasisDeformations.lift2_all {k : Type u} [Field k] [IsAlgClosed k] (h2 : 2 = 0) (hcor : Cor105Hyp k) (n : ℕ) : LiftBelow k n

Proposition 8.3(3) for all representation-finite ray tables, by strong induction on the number of rays, given Corollary 10.5 under the induction hypothesis.

theorem MultiplicativeBasisDeformations.exists_normedRayBasis_basic_char2 {k : Type u} [Field k] [IsAlgClosed k] (h2 : 2 = 0) (hcor : Cor105Hyp 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) (bF : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsNormedMultiplicativeBasis bF ∧ F.IsRayTransversal ⇑bF

Normed multiplicative ray bases of basic algebras in characteristic two, given Corollary 10.5 (Proposition 8.3(1)).