The index of a central simple algebra

Every finite-dimensional central simple algebra A over a field K has a Wedderburn presentation

A ≃ₐ[K] Matrix (Fin n) (Fin n) D

for a finite-dimensional central division algebra D. The division algebra is unique up to ring isomorphism, and the matrix size n is unique. This file defines TauCeti.Algebra.index K A to be the degree of one such D, then proves that every presentation computes the same number. Thus the definition exposes no choice to its users.

The two numerical invariants of a presentation satisfy

deg K A = n * index K A.

The index is 1 exactly when A is split. Combining the construction with the maximal-subfield theorem gives the arithmetic meaning required by the semisimple-algebras roadmap: every central simple algebra has a finite splitting field whose degree over K is exactly its index.

Main results

• TauCeti.Algebra.index_eq_deg_of_algEquiv_matrix: the index is the degree of the division algebra in any Wedderburn presentation.
• TauCeti.Algebra.deg_eq_mul_index_of_algEquiv_matrix: the degree is the product of the matrix size and the index.
• TauCeti.Algebra.isSplittingField_self_iff_index_eq_one: a central simple algebra is split over its base field exactly when its index is one.
• TauCeti.Algebra.exists_isSplittingField_finrank_eq_index: every central simple algebra has a finite splitting field of degree its index.

References

This implements the index portion of Layer 6, “Splitting fields, maximal subfields, and the index”, of the semisimple algebras roadmap. See P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.4, and R. S. Pierce, Associative Algebras, Chapter 13.

noncomputable def TauCeti.Algebra.index (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : ℕ

The index of a finite-dimensional central simple algebra: the degree of the central division algebra in a Wedderburn presentation.

Although the definition chooses a presentation, TauCeti.Algebra.index_eq_deg_of_algEquiv_matrix shows that every presentation gives the same value.

Equations

• TauCeti.Algebra.index K A = TauCeti.Algebra.deg K (TauCeti.Algebra.WedderburnData.divisionAlgebra✝ (TauCeti.Algebra.wedderburnData✝ K A))

theorem TauCeti.Algebra.index_eq_deg_of_algEquiv_matrix {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_2} [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] (e : A ≃ₐ[K] Matrix (Fin n) (Fin n) D) : index K A = deg K D

A Wedderburn presentation computes the index. If A is n × n matrices over a finite-dimensional central division algebra D, then the index of A is deg K D.

This is the characteristic property of TauCeti.Algebra.index; later results use it instead of unfolding the choice made in the definition.

theorem TauCeti.Algebra.deg_eq_mul_index_of_algEquiv_matrix {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_2} [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] (e : A ≃ₐ[K] Matrix (Fin n) (Fin n) D) : deg K A = n * index K A

The degree read from a Wedderburn presentation. If A ≃ Mₙ(D), then deg K A = n * index K A.

theorem TauCeti.Algebra.index_eq_of_algEquiv {K : Type u_1} [Field K] {A : Type u} [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] {B : Type v} [Ring B] [Algebra K B] [Algebra.IsCentral K B] [IsSimpleRing B] [FiniteDimensional K B] (e : A ≃ₐ[K] B) : index K A = index K B

The index is invariant under isomorphism of central simple K-algebras.

@[simp]

theorem TauCeti.Algebra.index_matrix {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] : index K (Matrix (Fin n) (Fin n) A) = index K A

Passing to a positive-size full matrix algebra does not change the index.

@[simp]

theorem TauCeti.Algebra.index_eq_deg_of_divisionRing {K : Type u_1} [Field K] (D : Type u) [DivisionRing D] [Algebra K D] [Algebra.IsCentral K D] [FiniteDimensional K D] : index K D = deg K D

The index of a central division algebra is its degree.

theorem TauCeti.Algebra.index_pos (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : 0 < index K A

The index of a central simple algebra is positive.

@[simp]

theorem TauCeti.Algebra.index_ne_zero (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : index K A ≠ 0

The index of a central simple algebra is nonzero.

theorem TauCeti.Algebra.index_dvd_deg (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : index K A ∣ deg K A

The index divides the degree of a central simple algebra.

theorem TauCeti.Algebra.index_le_deg (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : index K A ≤ deg K A

The index is at most the degree of a central simple algebra.

theorem TauCeti.Algebra.isSplittingField_self_iff_index_eq_one (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : IsSplittingField K A K ↔ index K A = 1

A central simple algebra is split over its base field exactly when its index is one.

theorem TauCeti.Algebra.index_eq_one_of_isAlgClosed (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] [IsAlgClosed K] : index K A = 1

Over an algebraically closed field every central simple algebra has index one.

theorem TauCeti.Algebra.index_eq_one_of_finite (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] [Finite K] : index K A = 1

Over a finite field every central simple algebra has index one.

theorem TauCeti.Algebra.exists_isSplittingField_finrank_eq_index (K : Type u_1) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L), FiniteDimensional K L ∧ Module.finrank K L = index K A ∧ IsSplittingField K A L

Every central simple algebra has a finite splitting field of degree its index.

Choose A ≃ Mₙ(D), take a maximal subfield L of D, and use that L splits D. It then splits Mₙ(D), hence A, while finrank K L = deg K D = index K A.