Wedderburn-Artin for central simple algebras

Mathlib's IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite writes a finite-dimensional simple K-algebra A as a matrix algebra Matrix (Fin n) (Fin n) D over a division algebra D, but it says nothing about the centre of D: the theorem is about simplicity alone. For the theory of central simple algebras one needs the refinement in which D is again central over K, because that is the hypothesis every later structure theorem (the degree, Skolem-Noether, the Brauer group) carries.

This file supplies the missing step. Feeding Mathlib's Wedderburn-Artin theorem the centrality descent TauCeti.isCentral_of_isCentral_matrix gives A ≃ₐ[K] Matrix (Fin n) (Fin n) D with D a central division algebra, together with the dimension count finrank K A = n ^ 2 * finrank K D.

The same file settles the finite base field. A finite division ring is a field (little Wedderburn), so Algebra.IsCentral.baseField_essentially_unique collapses a finite central division algebra to its base field, and every central simple algebra over a finite field is a full matrix algebra Matrix (Fin n) (Fin n) K. In particular its dimension is the square n ^ 2. Centrality is what makes this work: 𝔽_{q^m} is a finite division algebra over 𝔽_q which is not the base field, the failure being exactly that its structure map is not surjective.

Main results

• TauCeti.IsSimpleRing.exists_algEquiv_matrix_centralDivisionRing: Wedderburn-Artin for central simple algebras. A finite-dimensional central simple K-algebra A is Matrix (Fin n) (Fin n) D for a finite-dimensional central division K-algebra D, and finrank K A = n ^ 2 * finrank K D.
• TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_forall_nonempty_algEquiv: over a field whose finite-dimensional central division algebras are all the field itself, every finite-dimensional central simple algebra is a full matrix algebra over that field. It is the criterion behind TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_finite below and TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_isSepClosed in TauCeti/Algebra/CentralSimple/SeparablyClosed.lean.
• TauCeti.baseFieldAlgEquivOfFinite: a finite central division algebra over a field is the base field.
• TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_finite: a central simple algebra over a finite field is a full matrix algebra over that field, so in particular its dimension is the perfect square n ^ 2. That dimension count holds over every base field, by TauCeti.IsSimpleRing.isSquare_finrank in TauCeti/Algebra/CentralSimple/Degree.lean, which is the statement to use; only the matrix presentation itself is special to a finite field.

Implementation notes

TauCeti.baseFieldAlgEquivOfFinite assumes Finite D, the single hypothesis little Wedderburn needs, rather than the pair Finite K and FiniteDimensional K D; the two are equivalent, because K embeds in D. The central-simple corollary does take the pair Finite K and FiniteDimensional K A, which is how a finite base field is met in practice.

Uniqueness of the pair (n, D) is not proved here; it needs the invariance of the Wedderburn data, which is a separate development.

References

This implements the second bullet of Layer 4 of the semisimple algebras roadmap (A ≅ Mₙ(D) for a central division algebra D, with finrank K A = n² · finrank K D) together with its finite-field worked example. See R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, and P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Chapter 2.

Wedderburn-Artin for central simple algebras

theorem TauCeti.IsSimpleRing.exists_algEquiv_matrix_centralDivisionRing (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra K D) (_ : Algebra.IsCentral K D) (_ : FiniteDimensional K D), Module.finrank K A = n ^ 2 * Module.finrank K D ∧ Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) D)

Wedderburn-Artin for central simple algebras. A finite-dimensional central simple K-algebra A is isomorphic to a matrix algebra over a finite-dimensional central division K-algebra D, and then finrank K A = n ^ 2 * finrank K D.

Mathlib's IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite supplies everything except the centrality of D, which comes from TauCeti.isCentral_of_isCentral_matrix.

theorem TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_forall_nonempty_algEquiv (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (h : ∀ (D : Type u) [inst : DivisionRing D] [inst_1 : Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D], Nonempty (D ≃ₐ[K] K)) : ∃ (n : ℕ) (_ : NeZero n), Module.finrank K A = n ^ 2 ∧ Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) K)

A field whose central division algebras are all itself splits every central simple algebra. Given the Wedderburn presentation A ≃ₐ Mₙ(D), the hypothesis collapses D to K.

The hypothesis says that K admits no finite-dimensional central division algebra other than itself, equivalently that its Brauer group is trivial. It holds over a finite field, by little Wedderburn, and over a separably closed field, where Jacobson--Noether would otherwise produce a separable element outside the base field.

Finite central division algebras and finite base fields

noncomputable def TauCeti.baseFieldAlgEquivOfFinite (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Finite D] : D ≃ₐ[K] K

A finite central division algebra over a field is the base field, as an isomorphism of K-algebras.

A finite division ring is a field by little Wedderburn (the instance littleWedderburn), so K → D is a central extension of fields and Algebra.IsCentral.baseField_essentially_unique applied to the tower D / D / K makes it bijective. Centrality is essential: 𝔽_{q^m} is a finite division algebra over 𝔽_q whose structure map is not surjective for m > 1.

Equations

• TauCeti.baseFieldAlgEquivOfFinite K D = (AlgEquiv.ofBijective (Algebra.ofId K D) ⋯).symm

@[simp]

theorem TauCeti.baseFieldAlgEquivOfFinite_symm_apply (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Finite D] (a : K) : (baseFieldAlgEquivOfFinite K D).symm a = (algebraMap K D) a

@[simp]

theorem TauCeti.algebraMap_baseFieldAlgEquivOfFinite (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Finite D] (x : D) : (algebraMap K D) ((baseFieldAlgEquivOfFinite K D) x) = x

@[simp]

theorem TauCeti.finrank_eq_one_of_finite (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [Finite D] : Module.finrank K D = 1

A finite central division algebra over a field is one-dimensional over it.

theorem TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_finite (K : Type u_1) [Field K] [Finite K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : ∃ (n : ℕ) (_ : NeZero n), Module.finrank K A = n ^ 2 ∧ Nonempty (A ≃ₐ[K] Matrix (Fin n) (Fin n) K)

A central simple algebra over a finite field is a full matrix algebra. Over a finite field the only finite-dimensional central division algebra is the field itself, so the division algebra in the Wedderburn presentation collapses and finrank K A = n ^ 2.

This is the finite-field analogue of Mathlib's IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed; note that IsSimpleRing A alone would not suffice, since A could be a proper field extension of K.