Finite descent of splitting fields

A splitting of a finite-dimensional algebra over an algebraic extension descends to a finite intermediate field. A matrix presentation over the algebraic extension uses only finitely many coefficients, and adjoining those coefficients to the base field produces the desired finite extension.

Concretely, fix a basis of the algebra and pull the standard matrix units back along a splitting over the algebraic extension. Their coordinates generate a finite intermediate field L. The same coordinate formulas give elements of L ⊗[K] A; after extending scalars back to the ambient extension they are the original matrix units. They are therefore linearly independent, and the dimension count makes them a basis. The matrix-unit multiplication laws descend along the injective coefficient embedding and upgrade the resulting linear equivalence to an algebra equivalence.

Main result

• TauCeti.Algebra.exists_intermediateField_isSplittingField_finiteDimensional: a splitting over an algebraic extension descends to a finite intermediate 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_intermediateField_isSplittingField_finiteDimensional {K : Type u} [Field K] {A : Type w} [Ring A] [Algebra K A] [FiniteDimensional K A] {E : Type v} [Field E] [Algebra K E] [Algebra.IsAlgebraic K E] (h : IsSplittingField K A E) : ∃ (L : IntermediateField K E), FiniteDimensional K ↥L ∧ IsSplittingField K A ↥L

A splitting over an algebraic extension descends to a finite intermediate field.