Finite separable splitting fields

Every finite-dimensional central simple algebra over a field has a finite separable splitting field. The separable closure splits the algebra, and finite descent produces a finite intermediate field which is automatically separable over the base field.

Main result

• TauCeti.Algebra.exists_isSplittingField_finiteDimensional_isSeparable: every finite-dimensional central simple algebra has a finite separable splitting field.

References

See P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2, and R. S. Pierce, Associative Algebras, Chapter 13.

theorem TauCeti.Algebra.exists_isSplittingField_finiteDimensional_isSeparable (K : Type u) [Field K] (A : Type w) [Ring A] [Algebra K A] [FiniteDimensional K A] [Algebra.IsCentral K A] [IsSimpleRing A] : ∃ (L : IntermediateField K (SeparableClosure K)), FiniteDimensional K ↥L ∧ IsSplittingField K A ↥L

Every finite-dimensional central simple algebra has a finite separable splitting field.

The result exposes a finite intermediate field of the separable closure which splits the algebra. It is automatically separable over K by the intermediate-field instance.