Theorem 11.7(1)(2) in characteristic two #
main-theorems.tex (thm:final-basis). For a basic representation-finite algebra in
characteristic two, Proposition 8.3 (exists_normedRayBasis_basic_char2), with Corollary 10.5
now proved (cor105Hyp), gives a normed multiplicative ray transversal for one complete set of
primitive idempotents; conjugation (exists_algEquiv_idempotents) moves it to any other
(exists_rayTransversal_of_algEquiv).
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_rayTransversal_of_algEquiv
{k : Type u}
[Field k]
[IsAlgClosed k]
{A B : Type u}
[Ring A]
[Ring B]
[Algebra k A]
[Algebra k B]
[FiniteDimensional k A]
[FiniteDimensional k B]
(ψ : A ≃ₐ[k] B)
(F : PrimitiveIdempotents A)
(F' : PrimitiveIdempotents B)
(σ : Fin F.m ≃ Fin F'.m)
(hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i))
(b' : Module.Basis (NonzeroRay k F') k B)
(hn : IsNormedMultiplicativeBasis b')
(htr : F'.IsRayTransversal ⇑b')
:
∃ (b : Module.Basis (NonzeroRay k F) k A), IsNormedMultiplicativeBasis b ∧ F.IsRayTransversal ⇑b
Normed ray transversals transport along an algebra isomorphism matching the idempotents.
theorem
MultiplicativeBasisDeformations.finalBasis_ray_char2
(k : Type u)
[Field k]
[IsAlgClosed k]
(A : Type u)
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[CharP k 2]
(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) in characteristic two: a normed multiplicative ray transversal for any complete set of primitive idempotents.
theorem
MultiplicativeBasisDeformations.basic_hasNormedBasis_char2
(k : Type u)
[Field k]
[IsAlgClosed k]
(A : Type u)
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[CharP k 2]
(hbasic : IsBasicAlgebra A)
(hA : IsRepresentationFinite k A)
:
Theorem A for basic algebras in characteristic two.