Splitting fields of a central simple algebra

A field extension L / K splits a K-algebra A when the scalar extension L ⊗[K] A is a full matrix algebra over L. This file defines that predicate, TauCeti.Algebra.IsSplittingField, gives it its basic API, and settles the two cases that need no additional field theory: a separably closed extension splits every finite-dimensional central simple algebra, and over a finite base field every central simple algebra is already split by the base field itself.

The name is qualified because Mathlib's root-namespace IsSplittingField is the unrelated predicate that a field extension splits a polynomial.

The matrix size

For a central simple A the size of the matrix algebra is not extra data: it is forced to be TauCeti.Algebra.deg K A. Scalar extension preserves the dimension (Module.finrank L (L ⊗[K] A) = Module.finrank K A) and Matrix (Fin n) (Fin n) L has dimension n ^ 2 over L, so a splitting exhibits Module.finrank K A as n ^ 2; for a central simple A that dimension is already the square of the degree (TauCeti.Algebra.deg_sq), so n = TauCeti.Algebra.deg K A. This is TauCeti.Algebra.IsSplittingField.nonempty_algEquiv_matrix_deg, and it is why the existential in the definition costs nothing: the definition quantifies over n only so that it can be stated for an arbitrary K-algebra, where the degree is not yet meaningful.

Main results

• TauCeti.Algebra.IsSplittingField: the predicate itself, unfolded by TauCeti.Algebra.isSplittingField_iff, with the transport TauCeti.Algebra.isSplittingField_congr along a K-algebra isomorphism of A and the observation TauCeti.Algebra.isSplittingField_matrix that a full matrix algebra over K is split by every extension (by the base change TauCeti.Algebra.matrixBaseChangeAlgEquiv of TauCeti/Algebra/Matrix/BaseChange.lean).
• TauCeti.Algebra.IsSplittingField.matrix: a splitting field for A also splits every full matrix algebra over A.
• TauCeti.Algebra.IsSplittingField.of_isScalarTower: every further field extension of a splitting field still splits A.
• TauCeti.Algebra.isSplittingField_self_iff: A is split by its own base field exactly when it is a matrix algebra over it. This is the statement that "split" means what it should.
• TauCeti.Algebra.finrank_eq_sq_of_algEquiv_matrix and TauCeti.Algebra.IsSplittingField.nonempty_algEquiv_matrix_deg: the dimension count and, for a central simple A, the identification of the matrix size with the degree.
• TauCeti.Algebra.isSplittingField_of_isSepClosed: a separably closed extension splits every finite-dimensional central simple algebra.
• TauCeti.Algebra.isSplittingField_self_of_finite: over a finite field every central simple algebra is split by the base field, so there is nothing to split.

Implementation notes

TauCeti.Algebra.IsSplittingField is stated with L ⊗[K] A, the base field on the left, because that is the orientation in which L ⊗[K] A carries its L-algebra structure by Algebra.TensorProduct.leftAlgebra with no further glue, and it is the orientation of the base change already on main in TauCeti/Algebra/CentralSimple/Degree.lean.

The predicate deliberately asks for nothing of A beyond being a K-algebra: the elementary lemmas hold at that generality, and central simplicity is added only where the degree is mentioned. Nothing here needs A to be finite-dimensional either -- that is a consequence for a nonzero splitting, not a hypothesis.

Splitting ascends along field towers: if L splits A, so does every field extension M of L (TauCeti.Algebra.IsSplittingField.of_isScalarTower), and the matrix size does not change. So a splitting field may always be enlarged, for instance to its normal closure in order to obtain a Galois splitting field. This holds for an arbitrary, possibly noncommutative, K-algebra A.

References

This implements the splitting-field half of the fourth bullet of Layer 6 ("Splitting fields, maximal subfields, and the index") of the semisimple algebras roadmap, whose Suggested.lean pins IsSplittingField; the stronger separably closed form of its pinned algebraically closed splitting theorem is isSplittingField_of_isSepClosed, together with the splitting half of its "Finite base fields" bullet. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 13.

Splitting fields

def TauCeti.Algebra.IsSplittingField (K : Type u_1) (A : Type u_2) (L : Type u_3) [Field K] [Ring A] [Algebra K A] [Field L] [Algebra K L] : Prop

An extension L / K splits the K-algebra A when the scalar extension L ⊗[K] A is a full matrix algebra over L.

The matrix size is existentially quantified so that the predicate makes sense for an arbitrary K-algebra. For a finite-dimensional central simple A it is not a choice: it is forced to be TauCeti.Algebra.deg K A by TauCeti.Algebra.IsSplittingField.nonempty_algEquiv_matrix_deg.

Equations

• TauCeti.Algebra.IsSplittingField K A L = ∃ (n : ℕ), Nonempty (TensorProduct K L A ≃ₐ[L] Matrix (Fin n) (Fin n) L)

theorem TauCeti.Algebra.isSplittingField_iff (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] : IsSplittingField K A L ↔ ∃ (n : ℕ), Nonempty (TensorProduct K L A ≃ₐ[L] Matrix (Fin n) (Fin n) L)

The definition, unfolded: L splits A exactly when L ⊗[K] A is an n × n matrix algebra over L for some n.

This is the characterization at the generality the predicate is stated at, and everything below goes through it rather than through the body; for a finite-dimensional central simple A the size is pinned by TauCeti.Algebra.isSplittingField_iff_deg.

theorem TauCeti.Algebra.IsSplittingField.of_algEquiv (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] {B : Type u_4} [Ring B] [Algebra K B] (e : A ≃ₐ[K] B) (h : IsSplittingField K A L) : IsSplittingField K B L

Splitting is a property of the isomorphism class of A: a K-algebra isomorphic to a split one is split, by the same extension and with the same matrix size.

theorem TauCeti.Algebra.isSplittingField_congr (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] {B : Type u_4} [Ring B] [Algebra K B] (e : A ≃ₐ[K] B) : IsSplittingField K A L ↔ IsSplittingField K B L

Splitting transports along a K-algebra isomorphism of the algebra being split.

theorem TauCeti.Algebra.isSplittingField_matrix (K : Type u_1) [Field K] (L : Type u_3) [Field L] [Algebra K L] (n : ℕ) : IsSplittingField K (Matrix (Fin n) (Fin n) K) L

A full matrix algebra over K is split by every extension of K, by TauCeti.Algebra.matrixBaseChangeAlgEquiv. In particular it is split by K itself.

theorem TauCeti.Algebra.IsSplittingField.matrix (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] (h : IsSplittingField K A L) (n : ℕ) : IsSplittingField K (Matrix (Fin n) (Fin n) A) L

If L splits a K-algebra A, then it also splits every full matrix algebra over A.

After base change, the given splitting identifies each matrix entry with an m × m matrix over L; composing the two matrix indices gives an (n * m) × (n * m) matrix over L.

theorem TauCeti.Algebra.IsSplittingField.of_isScalarTower (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] (h : IsSplittingField K A L) (M : Type u_4) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : IsSplittingField K A M

Every further field extension of a splitting field is a splitting field.

If L splits A and M is a field extension of L (compatibly with K), then M ⊗[K] A is again a full matrix algebra over M, of the same size as L ⊗[K] A is over L. Use this to replace a splitting field by any larger field, such as a normal or separable closure of it.

theorem TauCeti.Algebra.isSplittingField_self_iff (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] : IsSplittingField K A K ↔ ∃ (n : ℕ), Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) K)

A is split by its own base field exactly when it is a matrix algebra over it. This is the sanity check on the definition: over L = K the scalar extension does nothing, so "split" is literally "is a matrix algebra".

theorem TauCeti.Algebra.isSplittingField_baseChange_self_iff (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] : IsSplittingField L (TensorProduct K L A) L ↔ IsSplittingField K A L

L splits A exactly when L splits the L-algebra L ⊗[K] A.

Both sides say ∃ n, L ⊗[K] A ≃ₐ[L] Mₙ(L), the left through TauCeti.Algebra.isSplittingField_self_iff and the right by definition. The lemma exists to move between the two readings, and so to bring results about a field splitting an algebra over itself to bear on a scalar extension.

theorem TauCeti.Algebra.finrank_eq_sq_of_algEquiv_matrix (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] {n : ℕ} (e : TensorProduct K L A ≃ₐ[L] Matrix (Fin n) (Fin n) L) : Module.finrank K A = n ^ 2

The dimension count behind a splitting: if L ⊗[K] A is n × n matrices over L, then A has dimension n ^ 2 over K.

Scalar extension preserves the dimension, and an n × n matrix algebra has dimension n ^ 2; no hypothesis on A is used, and in particular this is what proves that a split algebra has square dimension rather than assuming it.

theorem TauCeti.Algebra.IsSplittingField.nonempty_algEquiv_matrix_deg (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (h : IsSplittingField K A L) : Nonempty (TensorProduct K L A ≃ₐ[L] Matrix (Fin (deg K A)) (Fin (deg K A)) L)

The matrix size of a splitting is the degree. For a finite-dimensional central simple A, any splitting L ⊗[K] A ≃ₐ[L] Matrix (Fin n) (Fin n) L has n = TauCeti.Algebra.deg K A, so the splitting can always be restated at that size.

The existential in TauCeti.Algebra.IsSplittingField is therefore not a choice: n ^ 2 and (deg K A) ^ 2 are both Module.finrank K A (TauCeti.Algebra.finrank_eq_sq_of_algEquiv_matrix and TauCeti.Algebra.deg_sq), and squaring is injective on the naturals.

theorem TauCeti.Algebra.isSplittingField_iff_deg (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : IsSplittingField K A L ↔ Nonempty (TensorProduct K L A ≃ₐ[L] Matrix (Fin (deg K A)) (Fin (deg K A)) L)

A finite-dimensional central simple algebra is split by L exactly when L ⊗[K] A is the matrix algebra of size its degree.

theorem TauCeti.Algebra.isSplittingField_of_isSepClosed (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] [IsSepClosed L] : IsSplittingField K A L

A separably closed extension splits every finite-dimensional central simple algebra.

This is the base case of the separable splitting theory, and it needs no theory of maximal subfields: over a separably closed field the Wedderburn division algebra collapses, which is exactly TauCeti.IsSimpleRing.nonempty_algEquiv_matrix_baseChange_of_isSepClosed. Every finite-dimensional central simple K-algebra therefore has a separable splitting field, namely a separable closure of K.

theorem TauCeti.Algebra.isSplittingField_self_of_finite (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] [Finite K] : IsSplittingField K A K

Over a finite field every central simple algebra is split by the base field. A finite central division algebra is its own base field (little Wedderburn), so the Wedderburn presentation of A is already a matrix algebra over K; there is nothing left for an extension to split.

Together with TauCeti.Algebra.isSplittingField_self_iff this is the algebra-level content of the triviality of the Brauer group of a finite field.

Worked examples