Central simple algebras over separably closed fields

A finite-dimensional central simple algebra over a separably closed field is a full matrix algebra. This strengthens the algebraically closed case used in the initial splitting-field API and is the field-theoretic input for refining an arbitrary finite splitting extension to a finite separable one.

The only extra issue over the algebraically closed proof is the coefficient division algebra in Artin--Wedderburn. If an algebraic central division algebra D over a separably closed field K were larger than K, the Jacobson--Noether theorem would produce an element of D outside K that is separable over K. Its irreducible minimal polynomial would have degree one, because K is separably closed, so the element would in fact lie in K, a contradiction.

The scalar-extension and splitting consequences live in TauCeti/Algebra/CentralSimple/Degree.lean and TauCeti/Algebra/CentralSimple/Splitting.lean, where they replace the former algebraically closed special cases.

Main results

• TauCeti.baseFieldAlgEquivOfIsSepClosed: an algebraic central division algebra over a separably closed field is the base field.
• TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_isSepClosed: a finite-dimensional central simple algebra over a separably closed field is a full matrix algebra.

References

See N. Jacobson, Basic Algebra II, 2nd ed., Chapter 15, and P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2.

Central division algebras over a separably closed field

theorem TauCeti.algebraMap_surjective_of_isSepClosed (K : Type u_1) [Field K] [IsSepClosed K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Algebra.IsAlgebraic K D] : Function.Surjective ⇑(algebraMap K D)

The structure map from a separably closed field onto an algebraic central division algebra is surjective.

noncomputable def TauCeti.baseFieldAlgEquivOfIsSepClosed (K : Type u_1) [Field K] [IsSepClosed K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Algebra.IsAlgebraic K D] : D ≃ₐ[K] K

An algebraic central division algebra over a separably closed field is the base field, as an equivalence of algebras.

Equations

• TauCeti.baseFieldAlgEquivOfIsSepClosed K D = (AlgEquiv.ofBijective (Algebra.ofId K D) ⋯).symm

@[simp]

theorem TauCeti.baseFieldAlgEquivOfIsSepClosed_symm_apply (K : Type u_1) [Field K] [IsSepClosed K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Algebra.IsAlgebraic K D] (a : K) : (baseFieldAlgEquivOfIsSepClosed K D).symm a = (algebraMap K D) a

@[simp]

theorem TauCeti.algebraMap_baseFieldAlgEquivOfIsSepClosed (K : Type u_1) [Field K] [IsSepClosed K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Algebra.IsAlgebraic K D] (x : D) : (algebraMap K D) ((baseFieldAlgEquivOfIsSepClosed K D) x) = x

@[simp]

theorem TauCeti.finrank_eq_one_of_isSepClosed (K : Type u_1) [Field K] [IsSepClosed K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Algebra.IsAlgebraic K D] : Module.finrank K D = 1

An algebraic central division algebra over a separably closed field is one-dimensional over that field.

Central simple algebras

theorem TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_isSepClosed (K : Type u_1) [Field K] [IsSepClosed K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : ∃ (n : ℕ) (_ : NeZero n), Module.finrank K A = n ^ 2 ∧ Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) K)

Artin--Wedderburn over a separably closed field. A finite-dimensional central simple K-algebra is a full matrix algebra over K.