Maximal subfields of a central division algebra

Let K be a field and D a finite-dimensional central division algebra over K. TauCeti/Algebra/CentralSimple/Subfield.lean proves that a subfield of D has degree at most TauCeti.Algebra.deg K D, and that a subfield attaining that bound splits D; what it leaves open, in as many words, is whether the bound is attained at all. This file settles that: D has a subfield of degree exactly deg K D, so the splitting field produced there is never vacuous and every central division algebra is split by a finite extension of its centre sitting inside it.

The subfield is produced by maximality, in three steps.

A commutative subalgebra of maximal dimension exists. Dimensions of subalgebras of D are bounded by finrank K D, so among the commutative ones there is a subalgebra L of largest dimension (TauCeti.exists_isMulCommutative_forall_finrank_le, in TauCeti/Algebra/Algebra/Subalgebra/MaximalCommutative.lean). Nothing about D is used here beyond finite-dimensionality.

It is its own centralizer. If x centralizes L then L and x together generate a commutative subalgebra Algebra.adjoin K (insert x L), which contains L; maximal dimension makes the containment an equality, so x ∈ L. This is TauCeti.centralizer_eq_self_of_forall_finrank_le, in the same file, and it is also what makes L a maximal subfield rather than merely a large one.

Being a commutative domain, finite-dimensional over K, L is then a field (IsField.of_isDomain_of_finite).

Its dimension is forced. For any subfield L of a finite-dimensional central simple algebra A,

finrank K L * finrank K C_A(L) = finrank K A

(TauCeti.finrank_mul_finrank_centralizer_of_isField, in TauCeti/Algebra/CentralSimple/Centralizer.lean). Applied to C_D(L) = L this reads (finrank K L)² = finrank K D = (deg K D)², so finrank K L = deg K D.

Main results

• TauCeti.Algebra.exists_subalgebra_isField_finrank_eq_deg: a central division algebra has a subfield of degree deg K D.
• TauCeti.Algebra.exists_isSplittingField_finrank_eq_deg: a central division algebra is split by a subfield of degree deg K D.

Implementation notes

Commutativity of a subalgebra is Mathlib's IsMulCommutative on its coercion to a type, which is what Algebra.isMulCommutative_adjoin produces and what the scoped instances of the IsMulCommutative namespace turn into a CommRing structure; the file therefore opens that scope, which is what lets IsField.of_isDomain_of_finite apply to a commutative subalgebra of D.

The two ingredients that use nothing of the central simple theory are stated where they belong and consumed here: the existence of a commutative subalgebra of maximal dimension and its being its own centralizer in TauCeti/Algebra/Algebra/Subalgebra/MaximalCommutative.lean, the dimension of the centralizer of a subfield beside the centralizer theorem it specializes in TauCeti/Algebra/CentralSimple/Centralizer.lean.

The existence statements are stated for a division algebra. The passage from there to an arbitrary central simple algebra A ≃ₐ[K] Mₙ(D), and with it the index ind A, needs the uniqueness of the division algebra in a Wedderburn presentation and is not done here.

References

This is the maximal-subfield existence half of the fourth bullet of Layer 6 ("Splitting fields, maximal subfields, and the index": "a maximal subfield L of a central division algebra D (with finrank K L = deg D) splits D") of the semisimple algebras roadmap. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 13.

A maximal subfield of a central division algebra

theorem TauCeti.Algebra.exists_subalgebra_isField_finrank_eq_deg (K : Type u_1) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] : ∃ (L : Subalgebra K D), IsField ↥L ∧ Module.finrank K ↥L = deg K D

A central division algebra has a subfield of degree deg K D.

The subfield is delivered as a Subalgebra K D carrying IsField; TauCeti.Algebra.exists_isSplittingField_finrank_eq_deg is the same subfield packaged as a field in its own right, together with its embedding in D.

Together with TauCeti.Algebra.finrank_le_deg, which bounds the degree of every subfield by deg K D, this says L is a maximal subfield in the literal sense as well.

theorem TauCeti.Algebra.exists_isSplittingField_finrank_eq_deg (K : Type u_1) [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (x_2 : L →ₐ[K] D), FiniteDimensional K L ∧ Module.finrank K L = deg K D ∧ IsSplittingField K D L

A central division algebra is split by a subfield of degree deg K D.

This is the maximal-subfield route to a splitting field: unlike the passage to an algebraic closure (TauCeti.Algebra.isSplittingField_of_isSepClosed), it produces a splitting field that is a finite extension of K, and one realized inside D by the accompanying homomorphism.

Worked example: a maximal subfield of the real quaternions