Finite Galois splitting fields

Every finite-dimensional central simple algebra over a field is split by a finite Galois subextension of a separable closure. Starting with a finite separable splitting field, its normal closure is still finite and is Galois over the base field. Splitting persists after passing to that larger field.

This puts the splitting field in the form needed to use its Galois group, for example in the crossed-product description of central simple algebras.

Main result

• TauCeti.Algebra.exists_finiteGalois_splittingField: a finite-dimensional central simple algebra has a finite Galois splitting field inside a separable closure.

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_finiteGalois_splittingField (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 ∧ IsGalois K ↥L ∧ IsSplittingField K A ↥L

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

The field is an intermediate field of SeparableClosure K, so it comes with its specified embedding into the separable closure as well as its finite-dimensional, Galois, and splitting properties.