Main theorems (statements)

Theorems A and B of the introduction (main.tex), Theorem 11.7 (thm:final-basis), Corollary 5.5 (cor:away-from-two-basis), and Theorem 11.8(2) (thm:final-standardness).

Throughout, k is algebraically closed and A is a finite-dimensional k-algebra, in the same universe (the vendored Auslander--Reiten library works in one universe). "Characteristic different from two" is ringChar k ≠ 2.

theorem MultiplicativeBasisDeformations.theoremB (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) (hchar : ringChar k ≠ 2) : IsStandard k A

Theorem B (main.tex; Corollary 5.5, cor:away-from-two-basis). Every basic finite-dimensional representation-finite algebra over an algebraically closed field of characteristic different from two is standard.

theorem MultiplicativeBasisDeformations.basic_hasNormedBasis (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) (hchar : ringChar k ≠ 2) : HasNormedMultiplicativeBasis k A

Corollary 5.5(2) (cor:away-from-two-basis), existence part: a basic representation-finite algebra over an algebraically closed field of characteristic different from two has a normed multiplicative basis. The standard equivalence of Theorem B identifies A with A₀ (restricting to the projective labels), and A₀ has a normed multiplicative basis by Proposition 4.14 and Corollary 3.3.

theorem MultiplicativeBasisDeformations.theoremA_of_ringChar_ne_two (k : Type u) [Field k] [IsAlgClosed k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) (hchar : ringChar k ≠ 2) : HasNormedMultiplicativeBasis k A

Theorem A away from characteristic two (main.tex; Theorem 11.7(1) for char k ≠ 2, via Corollary 5.5(2) and Lemma 2.1): the basic algebra eAe is a representation-finite full corner, it has a normed multiplicative basis, and Lemma 2.1 lifts it to A.

theorem MultiplicativeBasisDeformations.theoremA (k : Type u) [Field k] [IsAlgClosed k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : HasNormedMultiplicativeBasis k A

Theorem A (main.tex; Theorem 11.7(1), thm:final-basis). Every finite-dimensional representation-finite algebra over an algebraically closed field has a normed multiplicative basis. Outside characteristic two this is theoremA_of_ringChar_ne_two; in characteristic two the basic corner has one by Proposition 8.3 with Corollary 10.5 (basic_hasNormedBasis_char2), and Lemma 2.1 lifts it to A.

theorem MultiplicativeBasisDeformations.awayFromTwoBasis (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) (hchar : ringChar k ≠ 2) (F : PrimitiveIdempotents A) : IsStandard k A ∧ ∃ (b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsNormedMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b ∧ F.KillsZeroRayProducts ⇑b

Corollary 5.5 (cor:away-from-two-basis). Let A be basic and representation-finite, and char k ≠ 2. (1) A ≅ k ray A, and A is standard. (2) The ray basis is a normed multiplicative basis of A, with one representative of every nonzero ray.

theorem MultiplicativeBasisDeformations.finalBasis_ray (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) (F : PrimitiveIdempotents A) : ∃ (b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsNormedMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b

Theorem 11.7(2) (thm:final-basis). For a basic algebra, the normed multiplicative basis can be chosen with one representative of every nonzero ray, the primitive idempotents representing the identity rays.

theorem MultiplicativeBasisDeformations.finalBasis_rayLinearization (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) (hchar : ringChar k ≠ 2) (F : PrimitiveIdempotents A) : ∃ (b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsNormedMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b ∧ F.KillsZeroRayProducts ⇑b

Theorem 11.7(3) (thm:final-basis). For a basic algebra and characteristic different from two, these representatives induce an isomorphism k ray A ≅ A.

theorem MultiplicativeBasisDeformations.standard_iff_rayLinearization (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) (F : PrimitiveIdempotents A) : IsStandard k A ↔ ∃ (b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A), IsMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b ∧ F.KillsZeroRayProducts ⇑b

Theorem 11.8(2) (thm:final-standardness). In every characteristic, a basic representation-finite algebra is standard if and only if A ≅ k ray A, expressed by a multiplicative ray transversal that kills zero ray products.