The degree of a central simple algebra

A finite-dimensional central simple algebra has square dimension over its base field. This file proves that, and defines the degree TauCeti.Algebra.deg K A as the square root of Module.finrank K A.

The proof is the base-change one, and it needs no theory of maximal subfields. Let L / K be a field extension with L separably closed. Then L ⊗[K] A is again central simple and is finite-dimensional over L of the same dimension as A over K (Module.finrank_baseChange). The separably closed Artin--Wedderburn theorem TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_isSepClosed writes it as Matrix (Fin n) (Fin n) L, whose dimension is n ^ 2.

Centrality of A over K is essential rather than decorative: ℂ is a simple, finite-dimensional ℝ-algebra whose dimension 2 is not a perfect square. That negative control is checked at the end of the file, alongside the real quaternions as the positive one.

The same argument says that a separably closed extension splits A, in deg K A rows and columns; that is recorded as TauCeti.IsSimpleRing.nonempty_algEquiv_matrix_baseChange_of_isSepClosed.

Main results

• TauCeti.IsSimpleRing.isSquare_finrank: the dimension of a finite-dimensional central simple algebra is a perfect square.
• TauCeti.Algebra.deg: the degree of a central simple algebra, with TauCeti.Algebra.deg_sq : deg K A ^ 2 = Module.finrank K A, its multiplicativity TauCeti.Algebra.deg_tensorProduct and TauCeti.Algebra.deg_matrix, the reading TauCeti.Algebra.deg_eq_mul_deg_of_algEquiv_matrix off a Wedderburn presentation, and the splitting TauCeti.IsSimpleRing.nonempty_algEquiv_matrix_baseChange_of_isSepClosed restated with matrix size deg K A.
• TauCeti.Algebra.finrank_tensorProduct_mulOpposite and TauCeti.Algebra.deg_tensorProduct_mulOpposite: the dimension (Module.finrank K A) ^ 2 and the degree Module.finrank K A of A ⊗[K] Aᵐᵒᵖ, for an arbitrary K-algebra A. These are the counts behind TauCeti/Algebra/CentralSimple/Opposite.lean.

Implementation notes

TauCeti.Algebra.deg is defined for every K-algebra, as Nat.sqrt (Module.finrank K A), the way Module.finrank is defined for every module. Its characteristic property is TauCeti.Algebra.deg_eq_of_finrank_eq_sq, which needs no hypotheses on A beyond the square dimension it is handed: the value is therefore pinned down for every square-dimensional algebra, central simple or not, and Nat.sqrt rounds down elsewhere. What central simplicity buys is that the dimension is a square (TauCeti.Algebra.deg_sq), and with it the reading of deg K A as the size of the matrix algebra A becomes over a separably closed extension. Every lemma here that computes a degree is derived from TauCeti.Algebra.deg_eq_of_finrank_eq_sq, so a downstream proof need never unfold the definition. The two exceptions do not compute a degree and go through Nat.sqrt directly, because there is no square dimension to feed the characteristic property: TauCeti.Algebra.deg_eq_of_finrank_eq, which only transports it along an equality of dimensions (and from which TauCeti.Algebra.deg_eq_of_algEquiv is read off), and TauCeti.Algebra.deg_pos, which only needs Module.finrank_pos.

TauCeti.IsSimpleRing.isSquare_finrank covers every base field, so the finite-base-field square-dimension statement that used to sit in TauCeti/Algebra/CentralSimple/Wedderburn.lean is gone, in favour of this one; that file keeps the matrix presentation TauCeti.IsSimpleRing.exists_algEquiv_matrix_of_finite, which is genuinely special to a finite base field and from which the square dimension used to be read off.

References

This implements the third bullet of Layer 4 of the semisimple algebras roadmap (square dimension by base change to the algebraic closure, and the degree defined as its square root). See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.4, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 12.

Splitting by a separably closed extension

theorem TauCeti.IsSimpleRing.isSquare_finrank (K : Type u_1) [Field K] (A : Type u_3) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : IsSquare (Module.finrank K A)

The dimension of a finite-dimensional central simple algebra is a perfect square.

Base change to an algebraic closure of K splits A, and a full matrix algebra has square dimension. Centrality cannot be dropped: Module.finrank ℝ ℂ = 2.

The degree

noncomputable def TauCeti.Algebra.deg (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] : ℕ

The degree of a central simple K-algebra A: the square root of Module.finrank K A, which is a perfect square by TauCeti.IsSimpleRing.isSquare_finrank. Equivalently, the size of the matrix algebra that A becomes over a separably closed extension of K (TauCeti.IsSimpleRing.nonempty_algEquiv_matrix_baseChange_of_isSepClosed).

This is defined for an arbitrary K-algebra. The characteristic property TauCeti.Algebra.deg_eq_of_finrank_eq_sq fixes the value whenever the dimension is a square, with or without central simplicity; on an algebra whose dimension is not a square, Nat.sqrt rounds down and the value carries no meaning.

Equations

• TauCeti.Algebra.deg K A = (Module.finrank K A).sqrt

theorem TauCeti.Algebra.deg_eq_of_finrank_eq_sq {K : Type u_1} [Field K] {A : Type u_2} [Ring A] [Algebra K A] {n : ℕ} (h : Module.finrank K A = n ^ 2) : deg K A = n

The characteristic property of the degree: a K-algebra of dimension n ^ 2 has degree n. Every lemma below that computes a degree is derived from this one, rather than by unfolding TauCeti.Algebra.deg.

theorem TauCeti.Algebra.deg_eq_of_finrank_eq {K : Type u_1} [Field K] {A : Type u_2} [Ring A] [Algebra K A] {L : Type u_3} {B : Type u_4} [Field L] [Ring B] [Algebra L B] (h : Module.finrank L B = Module.finrank K A) : deg L B = deg K A

Algebras of the same dimension have the same degree, even over different base fields. The degree being an integer square root, this needs no squareness: it transports the definition rather than computing a degree from TauCeti.Algebra.deg_eq_of_finrank_eq_sq.

theorem TauCeti.Algebra.deg_eq_of_algEquiv {K : Type u_1} [Field K] {A : Type u_2} [Ring A] [Algebra K A] {B : Type u_3} [Ring B] [Algebra K B] (e : A ≃ₐ[K] B) : deg K A = deg K B

Two isomorphic K-algebras have the same degree.

@[simp]

theorem TauCeti.Algebra.deg_self (K : Type u_1) [Field K] : deg K K = 1

theorem TauCeti.Algebra.finrank_tensorProduct_mulOpposite (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] : Module.finrank K (TensorProduct K A Aᵐᵒᵖ) = Module.finrank K A ^ 2

Passing to the opposite algebra does not change the dimension, so A ⊗[K] Aᵐᵒᵖ has dimension (Module.finrank K A) ^ 2. This is the count that turns injectivity of the Azumaya map into surjectivity in TauCeti/Algebra/CentralSimple/Opposite.lean, Module.End K A having the same dimension, and it is where the matrix size in TauCeti.Algebra.tensorOpAlgEquivMatrix comes from: a dimension, not a degree.

No finiteness hypothesis is needed: if A is infinite-dimensional both sides are 0.

theorem TauCeti.Algebra.deg_tensorProduct_mulOpposite (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] : deg K (TensorProduct K A Aᵐᵒᵖ) = Module.finrank K A

The degree of A ⊗[K] Aᵐᵒᵖ is the dimension of A. For A central simple this is the square of the degree of A (TauCeti.Algebra.deg_sq), and it is the degree-level shadow of TauCeti.Algebra.tensorOpAlgEquivMatrix: the reason the matrix size there is Module.finrank K A rather than TauCeti.Algebra.deg K A.

As with the dimension count it rests on, no hypothesis on A is needed: the dimension of A ⊗[K] Aᵐᵒᵖ is a square for every K-algebra, and that alone pins the degree.

Not a simp lemma: as soon as A is central simple and finite-dimensional, so is Aᵐᵒᵖ, and then TauCeti.Algebra.deg_tensorProduct already rewrites the left-hand side, to TauCeti.Algebra.deg K A * TauCeti.Algebra.deg K Aᵐᵒᵖ. Marking this one simp too would leave simp with two different normal forms for the same term.

theorem TauCeti.Algebra.deg_pos (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] [Nontrivial A] [FiniteDimensional K A] : 0 < deg K A

A nonzero finite-dimensional algebra has positive degree. Central simplicity is not needed: positive dimension already forces a positive integer square root.

@[simp]

theorem TauCeti.Algebra.deg_ne_zero (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] [Nontrivial A] [FiniteDimensional K A] : deg K A ≠ 0

A nonzero finite-dimensional algebra has nonzero degree.

@[simp]

theorem TauCeti.Algebra.deg_sq (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] : deg K A ^ 2 = Module.finrank K A

The dimension of a central simple algebra is the square of its degree.

@[simp]

theorem TauCeti.Algebra.deg_tensorProduct (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (B : Type u_3) [Ring B] [Algebra K B] [Algebra.IsCentral K B] [IsSimpleRing B] [FiniteDimensional K B] : deg K (TensorProduct K A B) = deg K A * deg K B

The degree is multiplicative under tensor product: this is the degree-level shadow of the fact that central simple K-algebras are closed under ⊗[K].

@[simp]

theorem TauCeti.Algebra.deg_matrix (K : Type u_1) [Field K] (A : Type u_2) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [IsSimpleRing A] [FiniteDimensional K A] (n : ℕ) : deg K (Matrix (Fin n) (Fin n) A) = n * deg K A

Passing to n × n matrices multiplies the degree by n.

theorem TauCeti.Algebra.deg_eq_mul_deg_of_algEquiv_matrix {K : Type u_1} [Field K] {A : Type u_2} [Ring A] [Algebra K A] {n : ℕ} {D : Type u_3} [Ring D] [Algebra K D] [Algebra.IsCentral K D] [IsSimpleRing D] [FiniteDimensional K D] (e : A ≃ₐ[K] Matrix (Fin n) (Fin n) D) : deg K A = n * deg K D

The degree read off a matrix presentation: if A is n × n matrices over a central simple K-algebra D then deg K A = n * deg K D. Fed the central division algebra D of TauCeti.IsSimpleRing.exists_algEquiv_matrix_centralDivisionRing, this is the degree of a Wedderburn presentation; note that A itself carries no hypotheses here, since they are inherited through the isomorphism.

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

A separably closed extension L / K splits a finite-dimensional central simple K-algebra A into matrices of size exactly TauCeti.Algebra.deg K A.

Worked examples