Normed bases of basic algebras in characteristic two (given Corollary 10.5)

The proof of Proposition 8.3(1) in characteristic two (main-theorems.tex), for a basic representation-finite algebra A: the rows of Proposition 6.1 with their dual mesh weights (residual_dual), the filtered structure of A over A₀ (posFiltA), and the characteristic-two step on A₀ (char2_A0). Corollary 10.5 is a hypothesis here; it is discharged by cor105Hyp in FinalBasis.lean.

theorem MultiplicativeBasisDeformations.IndSkeleton.arDegOne {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) : MeshWalk.DegOne (S.arMeshData b)

The mesh maps of Γ_A have degree one.

def MultiplicativeBasisDeformations.IndSkeleton.Cor105AR {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) : Prop

Corollary 10.5 for the algebra A₀ of A, for every choice of rows and dual weights.

def MultiplicativeBasisDeformations.IndSkeleton.rayA0AR {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) : Type

The rays of A₀ for the Auslander–Reiten mesh data.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.A0MultAR {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) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) : RaySys.Mult (S.arMeshData b).PV (S.rayA0AR b v₀)

The ray table of A₀ for the Auslander–Reiten mesh data.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_normedRayBasis_char2 {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) (h2 : 2 = 0) (hA : IsRepresentationFinite k A) {n : ℕ} {e : Fin n → A} (he : CompleteOrthogonalIdempotents e) (hprim : ∀ (i : Fin n), IsPrimitiveIdempotent (e i)) (hbasic : ∀ (i j : Fin n), (∃ (x : A) (y : A), e i * x * e j = x ∧ e j * y * e i = y ∧ x * y = e i ∧ y * x = e j) → i = j) (hn : n ≠ 0) (hcor : S.Cor105AR b) : ∃ (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) (F : PrimitiveIdempotents A) (bF : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsNormedMultiplicativeBasis bF ∧ F.IsRayTransversal ⇑bF ∧ ∃ (ι : (S.arMeshData b).PV ≃ Fin F.m) (β : S.rayA0AR b v₀ → A), F.IsRayPres (S.A0MultAR b v₀ hF) ι β

A basic algebra in characteristic two has a normed multiplicative ray basis, given Corollary 10.5 for its algebra A₀ (proof of Proposition 8.3(1), main-theorems.tex).