Documentation

TauCeti.Algebra.CentralSimple.Real

Frobenius' theorem: the real central division algebras are ℝ and ℍ[ℝ] #

A finite-dimensional division algebra over ℝ whose centre is ℝ is ℝ-isomorphic either to ℝ itself or to the Hamilton quaternions ℍ[ℝ]. This is the classification the Brauer group of ℝ needs: it says that the two Brauer classes already known -- the identity and the class of ℍ[ℝ] -- are all there are.

The proof runs in three steps, and only the first uses anything about central simple algebras.

The degree is at most two. A central division algebra has a subfield of degree deg ℝ D (TauCeti.Algebra.exists_subalgebra_isField_finrank_eq_deg), and a finite extension of ℝ is ℝ or ℂ (Mathlib's Real.nonempty_algEquiv_or), so that degree is 1 or 2 and finrank ℝ D is 1 or 4.

Every element satisfies a real quadratic. For y : D the subalgebra ℝ[y] is commutative and finite-dimensional over ℝ, hence a field, hence ℝ or ℂ again; in either case y * y is a real combination of 1 and y (TauCeti.exists_mul_self_eq_algebraMap_add_smul). Completing the square and rescaling turn any y outside ℝ into an i with i * i = -1 (TauCeti.exists_mul_self_eq_neg_one).

A second imaginary unit anticommutes with the first. Centrality gives an x not commuting with i, and then j = x + i * x * i satisfies i * j = i * x - x * i = -(j * i), so it is nonzero and anticommutes with i. Anticommutation forces j * j to be a real scalar, necessarily negative because a nonnegative one would factor in the division ring D and put j in ℝ; rescaling j makes j * j = -1. The pair (i, j) is a QuaternionAlgebra.Basis, so ℍ[ℝ] maps to D, and the map is injective because ℍ[ℝ] is a division ring and surjective because both sides have dimension 4.

Beyond the degree bound no maximal subfield, centralizer theorem or Skolem-Noether argument is needed; the rest is the elementary Frobenius argument.

Main results #

Implementation notes #

Mathlib's NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero is the same quadratic relation, but it is stated for an element of a normed ℝ-algebra whose norm is multiplicative. That hypothesis is not available here, D carrying no norm; the relation is therefore reproved from the finite-dimensionality of ℝ[y].

The three quadratic lemmas are stated for a domain rather than a division ring: no inverse in D is ever taken, only inverses of real scalars, so [Ring D] [IsDomain D] is what the arguments use. The division algebras of Frobenius' theorem supply those instances.

References #

This is the classification of "the finite-dimensional real division algebras with center ℝ" listed as a prerequisite of the real base field target in Layer 6 of the semisimple algebras roadmap. See R. S. Pierce, Associative Algebras, GTM 88, Chapter 13, and P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §1.1.

Real quadratics #

source
theorem TauCeti.exists_mul_self_eq_algebraMap_add_smul {D : Type u_1} [Ring D] [IsDomain D] [Algebra ℝ D] [FiniteDimensional ℝ D] (y : D) :
∃ (a : ℝ) (b : ℝ), y * y = (algebraMap ℝ D) a + b • y

Every element of a finite-dimensional real algebra that is a domain satisfies a monic real quadratic: y * y = a + b * y for real a and b.

The subalgebra ℝ[y] is a commutative domain of finite dimension over ℝ, hence a field, hence ℝ-isomorphic to ℝ or to ℂ by Mathlib's Real.nonempty_algEquiv_or. In the first case y is already real; in the second y corresponds to a complex number z, which satisfies z * z = -normSq z + (2 * z.re) * z.

source
theorem TauCeti.exists_mul_self_eq_neg_one {D : Type u_1} [Ring D] [IsDomain D] [Algebra ℝ D] [FiniteDimensional ℝ D] (h : Module.finrank ℝ D ≠ 1) :
∃ (i : D), i * i = -1

A finite-dimensional real algebra that is a domain and is not ℝ contains a square root of -1.

Take any y outside the copy of ℝ, write y * y = a + b * y, and complete the square: the element u = y - b / 2 has u * u a real scalar, and u is again outside ℝ, so exists_smul_mul_self_eq_neg_one rescales it to a square root of -1.

source
theorem TauCeti.exists_mul_self_eq_neg_one_and_mul_eq_neg_mul {D : Type u_1} [Ring D] [IsDomain D] [Algebra ℝ D] [FiniteDimensional ℝ D] {i x : D} (hi : i * i = -1) (hx : x * i ≠ i * x) :
∃ (j : D), j * j = -1 ∧ i * j = -(j * i)

A square root of -1 that does not commute with everything has an anticommuting partner: if i * i = -1 and some x fails to commute with i, then there is a j with j * j = -1 and i * j = -(j * i).

The partner is built from x as follows. The element j₀ = x + i * x * i satisfies i * j₀ = i * x - x * i = -(j₀ * i), so it is nonzero and anticommutes with i. Its square commutes with i, so in the quadratic j₀ * j₀ = a + b * j₀ the linear coefficient b must vanish, i * j₀ being nonzero. So j₀ * j₀ is a real scalar while j₀ itself is not, j₀ being a scalar only if it commuted with i; exists_smul_mul_self_eq_neg_one then rescales j₀ to a square root of -1, and rescaling keeps the anticommutation.

The degree of a real central division algebra #

source
theorem TauCeti.Algebra.deg_le_two (D : Type u_1) [DivisionRing D] [Algebra ℝ D] [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] :
deg ℝ D ≤ 2

A real central division algebra has degree at most 2. It has a subfield of degree deg ℝ D, and a finite extension of ℝ is ℝ or ℂ, so that degree is 1 or 2.

Frobenius' theorem #

source
theorem TauCeti.nonempty_algEquiv_quaternion_of_finrank_eq_four (D : Type u_1) [Ring D] [IsDomain D] [Algebra ℝ D] [Algebra.IsCentral ℝ D] (h4 : Module.finrank ℝ D = 4) :
Nonempty (D ≃ₐ[ℝ] Quaternion ℝ)

A four-dimensional central ℝ-algebra without zero divisors is ℝ-isomorphic to the Hamilton quaternions ℍ[ℝ]. Such an algebra is automatically a division algebra, being a domain of finite dimension over a field.

This is the substantive half of Frobenius' theorem, and the form to reach for once the dimension is known: TauCeti.nonempty_algEquiv_real_or_quaternion re-derives the degree bound and hands back a disjunction that still has to be eliminated. The absence of zero divisors is what rules out the split central simple algebra Matrix (Fin 2) (Fin 2) ℝ.

source
theorem TauCeti.nonempty_algEquiv_real_or_quaternion (D : Type u_1) [DivisionRing D] [Algebra ℝ D] [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] :
Nonempty (D ≃ₐ[ℝ] ℝ) ∨ Nonempty (D ≃ₐ[ℝ] Quaternion ℝ)

Frobenius' theorem. A finite-dimensional division algebra over ℝ with centre ℝ is ℝ-isomorphic either to ℝ or to the Hamilton quaternions ℍ[ℝ].

This is the classification to use when nothing is known about D beyond the hypotheses. If finrank ℝ D = 4 is already in hand, TauCeti.nonempty_algEquiv_quaternion_of_finrank_eq_four gives the quaternion isomorphism directly, with no disjunction to discharge.