Theorem 11.8(1): initial forms identify ray A with ray A₀

main-theorems.tex (thm:final-standardness(1)): for a basic representation-finite A, in every characteristic, "initial forms identify ray A with ray A₀. In particular ray A is associative, A₀ ≅ k ray A is representation-finite".

We state the identification as a ray presentation of A by the ray table of A₀ (rayA_eq_rayA0): the table is associative by construction, its linearization is A₀ (thetaA0), and A₀ is representation-finite (Proposition 2.10). In characteristic two the presentation is Proposition 8.3(2) (exists_normedRayBasis_char2); otherwise A ≅ A₀ (Theorem B with Corollary 4.15) and the fibre presentation of Proposition 11.3(3) with zero correction (exists_rayPres_A0).

Two ray presentations of one algebra have isomorphic tables

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.exists_tableIso {k : Type u} [Field k] [IsAlgClosed k] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (hB : IsRepresentationFinite k B) (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') : ∃ (m : R ≃ R') (ν : V ≃ V'), (∀ (r s : R), T'.mul (m r) (m s) = Option.map (⇑m) (T.mul r s)) ∧ ∀ (x : V), m (T.e x) = T'.e (ν x)

Lemma 3.6, as an isomorphism of tables: two ray presentations of one representation-finite algebra have isomorphic tables.

Definition 3.9

def MultiplicativeBasisDeformations.PrimitiveIdempotents.RayProductIndependent {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) : Prop

Representative independence of the ray products (Definition 3.9(3)); for a representation-finite algebra this is Lemma 3.6 (rayProductIndependent_of).

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.rayProductIndependent_of {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) [IsAlgClosed k] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : F.RayProductIndependent

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan_le_cornerRadical {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (F : PrimitiveIdempotents A) [IsAlgClosed k] [FiniteDimensional k A] {x y : Fin F.m} {f g : A} (hf : f ∈ F.corner x y) (hg : g ∈ F.corner y x) : F.insertionSpan x y x f g ≤ F.cornerRadical x

A middle-radical insertion M(f, g) with f ∈ A(x, y), g ∈ A(y, x) lies in rad R_x.

def MultiplicativeBasisDeformations.RaySys.Mult.IsSkeletal {V R : Type} (T : Mult V R) : Prop

The category with zero is skeletal: inverse morphisms are endomorphisms.

def MultiplicativeBasisDeformations.RaySys.Mult.IsFiniteRayCategory {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (T : Mult V R) (k : Type u) [Field k] : Prop

Definition 3.9(3): Q is a finite ray category: a finite skeletal category with zero whose identity vectors in kQ are primitive, whose ray products in kQ are representative-independent, and which r ↦ [r] identifies with the ray table of kQ.

theorem MultiplicativeBasisDeformations.RaySys.Mult.mul_eq_e_of_inverse {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {T : Mult V R} {k : Type u} [Field k] [IsAlgClosed k] {F : PrimitiveIdempotents ↥(T.Lin k)} {ι : V ≃ Fin F.m} (hFe : ∀ (x : V), F.e (ι x) = T.b k (T.e x)) (hind : F.RayProductIndependent) (hP : F.IsRayPres T ι (T.b k)) {i j : Fin F.m} {f g : ↥(T.Lin k)} (hf : f ∈ F.corner i j) (hg : g ∈ F.corner j i) (hfg : f * g = F.e i) {r s : R} (hr : ι (T.src r) = i ∧ ι (T.tgt r) = j ∧ f ∈ F.ray i j (T.b k r)) (hs : ι (T.src s) = j ∧ ι (T.tgt s) = i ∧ g ∈ F.ray j i (T.b k s)) : T.mul r s = some (T.e (T.src r))

In a ray presentation of kQ by Q, an inverse pair f g = e_i has identity ray product.

theorem MultiplicativeBasisDeformations.RaySys.Mult.isBasic_of_isFiniteRayCategory {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {T : Mult V R} {k : Type u} [Field k] [IsAlgClosed k] (hQ : T.IsFiniteRayCategory k) : IsBasicAlgebra ↥(T.Lin k)

The linearization of a finite ray category is basic (proof of Theorem 11.8).

theorem MultiplicativeBasisDeformations.MeshWalk.exists_rayPres_of_algEquiv {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)ᵐᵒᵖ) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (φ : B ≃ₐ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) : ∃ (F : PrimitiveIdempotents B) (ι : D.PV ≃ Fin F.m) (β : RayA0 D v₀ → B), F.IsRayPres (A0Mult D v₀ hF) ι β

An algebra isomorphic to A₀ is presented by the ray table of A₀.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_rayPres_A0 {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (φ : A ≃ₐ[k] S.A0 b) (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) ι β

An algebra isomorphic to A₀ is presented by the ray table of A₀.

theorem MultiplicativeBasisDeformations.rayA_eq_rayA0 (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) (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) ι β

Theorem 11.8(1) (thm:final-standardness): in every characteristic, a basic representation-finite algebra is presented by the ray table of its algebra A₀ (the initial-form identification ray A = ray A₀); A₀ ≅ k ray A₀ and A₀ is representation-finite.

theorem MultiplicativeBasisDeformations.RaySys.Mult.isStandard_of_isFiniteRayCategory {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {T : Mult V R} {k : Type u} [Field k] [IsAlgClosed k] (hQ : T.IsFiniteRayCategory k) (hfin : IsRepresentationFinite k ↥(T.Lin k)) : IsStandard k ↥(T.Lin k)

Theorem 11.8(3), standardness: the linearization of a finite ray category Q with kQ representation-finite is standard, in every characteristic. By Theorem 11.8(1) kQ is presented by the ray table of its A₀; by Definition 3.9 it is presented by Q; Lemma 3.6 identifies the two tables, so kQ ≅ A₀, and the converse of Corollary 4.15 applies.

The scalar-weight group of a table (Definition 7.1)

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.wRel {V R : Type} (T : Mult V R) : AddSubgroup (R →₀ ℤ)

The relations of W(Q): [rs] - [r] - [s] for rs ≠ 0, and the identity symbols.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Mult.W {V R : Type} (T : Mult V R) : Type

Definition 7.1: the scalar-weight group W(Q) = ℤ⟨[r]⟩ / ⟨[rs] - [r] - [s] : rs ≠ 0⟩, identity symbols being zero.

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.wCls {V R : Type} (T : Mult V R) (r : R) : T.W

The class [r].

theorem MultiplicativeBasisDeformations.RaySys.Mult.wCls_mul {V R : Type} (T : Mult V R) {r s t : R} (h : T.mul r s = some t) : T.wCls t = T.wCls r + T.wCls s

theorem MultiplicativeBasisDeformations.RaySys.Mult.wCls_e {V R : Type} (T : Mult V R) (x : V) : T.wCls (T.e x) = 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.mk_single {V R : Type} (T : Mult V R) (r : R) (n : ℤ) : (↑fun₀ | r => n) = n • T.wCls r

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.wLift {V R : Type} (T : Mult V R) {M : Type u_1} [AddCommGroup M] (φ : R → M) (hmul : ∀ (r s t : R), T.mul r s = some t → φ t = φ r + φ s) (he : ∀ (x : V), φ (T.e x) = 0) : T.W →+ M

Homomorphisms out of W(Q) are additive weights.

theorem MultiplicativeBasisDeformations.RaySys.Mult.wLift_cls {V R : Type} (T : Mult V R) {M : Type u_1} [AddCommGroup M] (φ : R → M) (hmul : ∀ (r s t : R), T.mul r s = some t → φ t = φ r + φ s) (he : ∀ (x : V), φ (T.e x) = 0) (r : R) : (T.wLift φ hmul he) (T.wCls r) = φ r

theorem MultiplicativeBasisDeformations.RaySys.Mult.W.hom_ext {V R : Type} (T : Mult V R) {M : Type u_1} [AddCommGroup M] {f g : T.W →+ M} (h : ∀ (r : R), f (T.wCls r) = g (T.wCls r)) : f = g

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.wEquiv {V R : Type} {T : Mult V R} {V' R' : Type} {T' : Mult V' R'} (m : R ≃ R') (ν : V ≃ V') (hmul : ∀ (r s : R), T'.mul (m r) (m s) = Option.map (⇑m) (T.mul r s)) (he : ∀ (x : V), m (T.e x) = T'.e (ν x)) : T.W ≃+ T'.W

Isomorphic tables have isomorphic scalar-weight groups.

theorem MultiplicativeBasisDeformations.MeshWalk.nz_of_deckV_ne {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {x y : D.PV} {g : Deck Q v₀} (h : deckV D v₀ hF x y g ≠ 0) : NZ Q c v₀ D (x, y, g)

theorem MultiplicativeBasisDeformations.MeshWalk.A0Mult_mul_of {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {x y z : D.PV} {g h : Deck Q v₀} (hne : CategoryTheory.CategoryStruct.comp (deckV D v₀ hF x y g) (deckV D v₀ hF y z h) ≠ 0) : (A0Mult D v₀ hF).mul ⟨(y, z, h), ⋯⟩ ⟨(x, y, g), ⋯⟩ = some ⟨(x, z, g * h), ⋯⟩

A nonzero product of deck vectors is a product in the table of A₀.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wA0Equiv {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : (A0Mult D v₀ hF).W ≃+ WP Q c v₀ D

W(ray A₀) = W(P): the scalar-weight group of the table of A₀ is the group WP of deck pieces.

theorem MultiplicativeBasisDeformations.RaySys.Mult.W_free_of_rayPres {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {T : Mult V R} {k : Type u} [Field k] [IsAlgClosed k] (hbasic : IsBasicAlgebra ↥(T.Lin k)) (hfin : IsRepresentationFinite k ↥(T.Lin k)) (r₀ : R) {F : PrimitiveIdempotents ↥(T.Lin k)} {ι : V ≃ Fin F.m} (hP : F.IsRayPres T ι (T.b k)) (hc : T.Conn) : Module.Free ℤ T.W

W(Q) is free for a connected table presenting its own representation-finite basic linearization: Q is identified with the ray table of A₀, whose scalar-weight group is free (Proposition 7.2(1)).

theorem MultiplicativeBasisDeformations.RaySys.Mult.W_free_of_isEmpty {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {T : Mult V R} [IsEmpty R] : Module.Free ℤ T.W

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.wSplit {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) : P.W ≃+ (sub (compData hC)).W × (sub (compData ⋯)).W

W splits along a union of components.

theorem MultiplicativeBasisDeformations.RaySys.Tab.W_free (k : Type u) [Field k] [IsAlgClosed k] (n : ℕ) (V R L : Type) [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) : Fintype.card R < n → IsRepresentationFinite k ↥(P.Lin k) → Module.Free ℤ P.W

W of a representation-finite ray table is free (Proposition 8.3(3) for ray tables), by strong induction on the number of rays, splitting along components.

theorem MultiplicativeBasisDeformations.MeshWalk.W_A0_free {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)ᵐᵒᵖ) : Module.Free ℤ (A0Mult D v₀ hF).W

W(ray A₀) is free, also for disconnected A₀.

theorem MultiplicativeBasisDeformations.RaySys.Mult.W_free_of_isFiniteRayCategory {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {T : Mult V R} {k : Type u} [Field k] [IsAlgClosed k] (hQ : T.IsFiniteRayCategory k) (hfin : IsRepresentationFinite k ↥(T.Lin k)) : Module.Free ℤ T.W

Theorem 11.8(3), freeness of W(Q): for a finite ray category Q with kQ representation-finite, W(Q) is free abelian. Q is identified with the ray table of the algebra A₀ of kQ (Theorem 11.8(1) and Lemma 3.6), whose scalar-weight group is free.

theorem MultiplicativeBasisDeformations.finalStandardness_rayCategory (k : Type u) [Field k] [IsAlgClosed k] {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (Q : RaySys.Mult V R) (hQ : Q.IsFiniteRayCategory k) (hfin : IsRepresentationFinite k ↥(Q.Lin k)) : Module.Free ℤ Q.W ∧ IsStandard k ↥(Q.Lin k)

Theorem 11.8(3) (thm:final-standardness): for every finite ray category Q with kQ representation-finite, over an algebraically closed field of any characteristic, W(Q) is free abelian and kQ is standard, k(Γ_{kQ}) ≃ ind(mod kQ).