A ≅ k ray A implies that A is standard in characteristic two (Theorem 11.8(2))

main-theorems.tex: "Proposition 8.3(2) and (3) give the initial-form comparison […] Combine them with Proposition 4.14 and Corollary 4.15 to obtain (1) and (2)."

A multiplicative ray transversal killing the zero ray products (A ≅ k ray A) is a basis whose table presents A (selfPres). Proposition 8.3(2) presents A by the table P of A₀; Lemma 3.6 matches the two tables (IsRayPres.matchFn, IsRayPres.mul_iff), so A ≅ kP ≅ A₀ (algEquivA0_of_rayBasis), and A is standard by the converse of Corollary 4.15 (isStandard_of_algEquiv).

theorem MultiplicativeBasisDeformations.RaySys.nonempty_algEquiv_of_match {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] [Fintype V'] [DecidableEq V'] [Fintype R'] [DecidableEq R'] (T : Mult V R) (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)) (k : Type u) [Field k] : Nonempty (↥(T.Lin k) ≃ₐ[k] ↥(T'.Lin k))

An isomorphism of tables gives an isomorphism of linearizations.

theorem MultiplicativeBasisDeformations.RaySys.nonempty_algEquiv_of_match' {V R V' R' : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {iV' : Fintype V'} {dV' : DecidableEq V'} {iR' : Fintype R'} {dR' : DecidableEq R'} (T : Mult V R) (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)) (k : Type u) [Field k] : Nonempty (↥(T.Lin k) ≃ₐ[k] ↥(T'.Lin k))

nonempty_algEquiv_of_match with the instances of the target as ordinary implicit arguments, to be found by unification.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfSpec {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (r : R) : ∃ (x : Fin F.m) (y : Fin F.m), b (c r) ∈ F.corner x y ∧ b (c r) ≠ 0 ∧ ↑(c r) = F.ray x y (b (c r))

noncomputable def MultiplicativeBasisDeformations.PrimitiveIdempotents.selfSrc {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (r : R) : Fin F.m

The source of a ray.

noncomputable def MultiplicativeBasisDeformations.PrimitiveIdempotents.selfTgt {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (r : R) : Fin F.m

The target of a ray.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfSpec' {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (r : R) : b (c r) ∈ F.corner (F.selfSrc ht c r) (F.selfTgt ht c r) ∧ b (c r) ≠ 0

def MultiplicativeBasisDeformations.PrimitiveIdempotents.idRay {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) (x : Fin F.m) : NonzeroRay k F

The identity ray at x.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.b_idRay {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) (x : Fin F.m) : b (F.idRay x) = F.e x

def MultiplicativeBasisDeformations.PrimitiveIdempotents.selfE {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {R : Type} (c : R ≃ NonzeroRay k F) (x : Fin F.m) : R

The identity rays, as indices.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.b_selfE {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (x : Fin F.m) : b (c (F.selfE c x)) = F.e x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfSrc_E {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (x : Fin F.m) : F.selfSrc ht c (F.selfE c x) = x

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfTgt_E {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) (x : Fin F.m) : F.selfTgt ht c (F.selfE c x) = x

noncomputable def MultiplicativeBasisDeformations.PrimitiveIdempotents.selfTable {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (hm : IsMultiplicativeBasis b) (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) : RaySys.Mult (Fin F.m) R

The table of the basis.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfTable_mul {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (hm : IsMultiplicativeBasis b) (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) {r s t : R} (h : (F.selfTable hm ht c).mul r s = some t) : b (c r) * b (c s) = b (c t)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfTable_mul_none {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (hm : IsMultiplicativeBasis b) (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) {r s : R} (h : (F.selfTable hm ht c).mul r s = none) : b (c r) * b (c s) = 0

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.selfPres {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (hm : IsMultiplicativeBasis b) (ht : F.IsRayTransversal ⇑b) (hz : F.KillsZeroRayProducts ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) : F.IsRayPres (F.selfTable hm ht c) (Equiv.refl (Fin F.m)) (⇑b ∘ ⇑c)

A multiplicative ray transversal killing zero ray products presents A by its table.

noncomputable def MultiplicativeBasisDeformations.PrimitiveIdempotents.selfLin {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {b : Module.Basis (NonzeroRay k F) k A} (hm : IsMultiplicativeBasis b) (ht : F.IsRayTransversal ⇑b) {R : Type} [Fintype R] [DecidableEq R] (c : R ≃ NonzeroRay k F) : ↥((F.selfTable hm ht c).Lin k) ≃ₐ[k] A

k(table) ≅ A.

theorem MultiplicativeBasisDeformations.IndSkeleton.isStandard_of_subsingleton {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) [Subsingleton A] : S.IsStandard

A trivial algebra is standard: there are no indecomposable modules.

theorem MultiplicativeBasisDeformations.IndSkeleton.algEquivA0_of_rayBasis {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) [CharP k 2] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (hn : Nontrivial A) (F : PrimitiveIdempotents A) {b : Module.Basis (PrimitiveIdempotents.NonzeroRay k F) k A} (hm : IsMultiplicativeBasis b) (ht : F.IsRayTransversal ⇑b) (hz : F.KillsZeroRayProducts ⇑b) : Nonempty (A ≃ₐ[k] S.A0 b')

A ≅ k ray A gives A ≅ A₀ in characteristic two (Proposition 8.3(2) with Lemma 3.6).