The norm form of a quaternion algebra

The product x * star x of a quaternion with its conjugate is a scalar (QuaternionAlgebra.mul_star_eq_coe). Its real part is the reduced norm, and this file packages it as a quadratic form QuaternionAlgebra.normForm on ℍ[R,c₁,c₂,c₃] over a commutative ring, with its coordinate expression and its multiplicativity.

In the classical presentation ℍ[R,a,b] = ℍ[R,a,0,b], where i² = a, j² = b and k = i * j, the basis 1, i, j, k is orthogonal for the norm form, which is therefore the diagonal form ⟨1, -a, -b, ab⟩; this is the two-fold Pfister form ⟨⟨a,b⟩⟩. The pure quaternions -- those with vanishing real part, which by QuaternionAlgebra.self_add_star_eq_zero_iff are exactly those of vanishing reduced trace once 2 is regular -- carry the restricted form ⟨-a, -b, ab⟩.

The reduced norm is what ties a quaternion algebra to quadratic-form theory. Over a field of characteristic other than two, with nonzero parameters a and b, whether ℍ[K,a,b] is split or a division algebra is determined by its norm form; the diagonalizations above turn this into a question about ⟨1, -a, -b, ab⟩.

Main definitions

• QuaternionAlgebra.normForm: the norm form x ↦ (x * star x).re of ℍ[R,c₁,c₂,c₃].
• QuaternionAlgebra.pureNormForm: its restriction to the pure quaternions of ℍ[R,a,b].

Main results

• QuaternionAlgebra.normForm_mul: the norm form is multiplicative.
• QuaternionAlgebra.mem_unitary_iff_normForm_eq_one: a quaternion is unitary exactly when its norm form is one.
• QuaternionAlgebra.isUnit_iff_normForm_isUnit: a quaternion is invertible exactly when its norm is, and QuaternionAlgebra.anisotropic_normForm_iff: over a field, a quaternion algebra is a division algebra exactly when its norm form is anisotropic.
• QuaternionAlgebra.equivalent_normForm_weightedSumSquares: the norm form of ℍ[R,a,b] is the diagonal form ⟨1, -a, -b, ab⟩, with the explicit isometry QuaternionAlgebra.normFormIsometryEquivWeightedSumSquares.
• QuaternionAlgebra.equivalent_pureNormForm_weightedSumSquares: the pure norm form of ℍ[R,a,b] is the diagonal form ⟨-a, -b, ab⟩, with the explicit isometry QuaternionAlgebra.pureNormFormIsometryEquivWeightedSumSquares.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, §2.
• P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §1.1.

def QuaternionAlgebra.normForm {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) : QuadraticForm R (QuaternionAlgebra R c₁ c₂ c₃)

The norm form of a quaternion algebra: the reduced norm x ↦ (x * star x).re, which is a quadratic form because x * star x is the scalar x.re² + c₂ x.re x.imI - c₁ x.imI² - c₃ x.imJ² - c₂ c₃ x.imJ x.imK + c₁ c₃ x.imK².

Equations

• QuaternionAlgebra.normForm c₁ c₂ c₃ = QuadraticMap.ofPolar (fun (x : QuaternionAlgebra R c₁ c₂ c₃) => (x * star x).re) ⋯ ⋯ ⋯

theorem QuaternionAlgebra.normForm_apply {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : (normForm c₁ c₂ c₃) x = (x * star x).re

theorem QuaternionAlgebra.normForm_apply_coordinates {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : (normForm c₁ c₂ c₃) x = x.re ^ 2 + c₂ * x.re * x.imI - c₁ * x.imI ^ 2 - c₃ * x.imJ ^ 2 - c₂ * c₃ * x.imJ * x.imK + c₁ * c₃ * x.imK ^ 2

The norm form in coordinates: the basis 1, i, j, k is orthogonal for it as soon as c₂ = 0.

theorem QuaternionAlgebra.polar_normForm {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x y : QuaternionAlgebra R c₁ c₂ c₃) : QuadraticMap.polar (⇑(normForm c₁ c₂ c₃)) x y = (x * star y + y * star x).re

The companion bilinear form of the norm form is the reduced trace of x * star y.

theorem QuaternionAlgebra.self_mul_star {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : x * star x = ↑((normForm c₁ c₂ c₃) x)

A quaternion times its conjugate is the scalar given by its norm form.

theorem QuaternionAlgebra.star_mul_self {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : star x * x = ↑((normForm c₁ c₂ c₃) x)

The conjugate of a quaternion times the quaternion is the scalar given by its norm form.

@[simp]

theorem QuaternionAlgebra.mem_unitary_iff_normForm_eq_one {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : x ∈ unitary (QuaternionAlgebra R c₁ c₂ c₃) ↔ (normForm c₁ c₂ c₃) x = 1

A quaternion is unitary exactly when its norm form is one.

@[simp]

theorem QuaternionAlgebra.normForm_coe {R : Type u_1} [CommRing R] (c₁ c₂ c₃ r : R) : (normForm c₁ c₂ c₃) ↑r = r ^ 2

@[simp]

theorem QuaternionAlgebra.normForm_star {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : (normForm c₁ c₂ c₃) (star x) = (normForm c₁ c₂ c₃) x

@[simp]

theorem QuaternionAlgebra.normForm_mul {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x y : QuaternionAlgebra R c₁ c₂ c₃) : (normForm c₁ c₂ c₃) (x * y) = (normForm c₁ c₂ c₃) x * (normForm c₁ c₂ c₃) y

The norm form is multiplicative.

theorem QuaternionAlgebra.isUnit_iff_normForm_isUnit {R : Type u_1} [CommRing R] (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : IsUnit x ↔ IsUnit ((normForm c₁ c₂ c₃) x)

A quaternion is invertible exactly when its norm is. The inverse of x is N(x)⁻¹ star x, and conversely the norm form is multiplicative.

theorem QuaternionAlgebra.anisotropic_normForm_iff {K : Type u_2} [Field K] (c₁ c₂ c₃ : K) : QuadraticMap.Anisotropic (normForm c₁ c₂ c₃) ↔ ∀ (x : QuaternionAlgebra K c₁ c₂ c₃), x ≠ 0 → IsUnit x

Division or not, by the norm form. A quaternion algebra over a field is a division algebra, in the sense that every nonzero element is invertible, exactly when its norm form is anisotropic.

theorem QuaternionAlgebra.self_add_star_eq_zero_iff {R : Type u_1} [CommRing R] (a b : R) (h2 : IsRegular 2) (x : QuaternionAlgebra R a 0 b) : x + star x = 0 ↔ x ∈ (reₗ a 0 b).ker

The pure quaternions of ℍ[R,a,b], the kernel of the real part, are exactly the quaternions of vanishing reduced trace x + star x.

def QuaternionAlgebra.pureNormForm {R : Type u_1} [CommRing R] (a b : R) : QuadraticForm R ↥(reₗ a 0 b).ker

The pure norm form of ℍ[R,a,b]: the norm form restricted to the pure quaternions, those with vanishing real part.

Equations

• QuaternionAlgebra.pureNormForm a b = QuadraticMap.comp (QuaternionAlgebra.normForm a 0 b) (QuaternionAlgebra.reₗ a 0 b).ker.subtype

@[simp]

theorem QuaternionAlgebra.pureNormForm_apply {R : Type u_1} [CommRing R] (a b : R) (x : ↥(reₗ a 0 b).ker) : (pureNormForm a b) x = (normForm a 0 b) ↑x

theorem QuaternionAlgebra.pureNormForm_apply_coordinates {R : Type u_1} [CommRing R] (a b : R) (x : ↥(reₗ a 0 b).ker) : (pureNormForm a b) x = -(a * (↑x).imI ^ 2) - b * (↑x).imJ ^ 2 + a * b * (↑x).imK ^ 2

The pure norm form in coordinates: the basis i, j, k is orthogonal for it.

def QuaternionAlgebra.normFormIsometryEquivWeightedSumSquares {R : Type u_1} [CommRing R] (a b : R) : QuadraticMap.IsometryEquiv (normForm a 0 b) (QuadraticMap.weightedSumSquares R ![1, -a, -b, a * b])

The coordinates 1, i, j, k are an isometry from the norm form of ℍ[R,a,b] to the diagonal form ⟨1, -a, -b, ab⟩, the two-fold Pfister form ⟨⟨a,b⟩⟩.

Equations

• QuaternionAlgebra.normFormIsometryEquivWeightedSumSquares a b = { toLinearEquiv := QuaternionAlgebra.linearEquivTuple a 0 b, map_app' := ⋯ }

@[simp]

theorem QuaternionAlgebra.normFormIsometryEquivWeightedSumSquares_apply {R : Type u_1} [CommRing R] (a b : R) (x : QuaternionAlgebra R a 0 b) : (normFormIsometryEquivWeightedSumSquares a b) x = ![x.re, x.imI, x.imJ, x.imK]

@[simp]

theorem QuaternionAlgebra.normFormIsometryEquivWeightedSumSquares_symm_apply {R : Type u_1} [CommRing R] (a b : R) (v : Fin 4 → R) : (normFormIsometryEquivWeightedSumSquares a b).symm v = { re := v 0, imI := v 1, imJ := v 2, imK := v 3 }

theorem QuaternionAlgebra.equivalent_normForm_weightedSumSquares {R : Type u_1} [CommRing R] (a b : R) : QuadraticMap.Equivalent (normForm a 0 b) (QuadraticMap.weightedSumSquares R ![1, -a, -b, a * b])

The norm form of ℍ[R,a,b] is ⟨1, -a, -b, ab⟩.

def QuaternionAlgebra.pureNormFormIsometryEquivWeightedSumSquares {R : Type u_1} [CommRing R] (a b : R) : QuadraticMap.IsometryEquiv (pureNormForm a b) (QuadraticMap.weightedSumSquares R ![-a, -b, a * b])

The coordinates i, j, k are an isometry from the pure norm form of ℍ[R,a,b] to the diagonal form ⟨-a, -b, ab⟩.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.pureNormFormIsometryEquivWeightedSumSquares_apply {R : Type u_1} [CommRing R] (a b : R) (x : ↥(reₗ a 0 b).ker) : (pureNormFormIsometryEquivWeightedSumSquares a b) x = ![(↑x).imI, (↑x).imJ, (↑x).imK]

@[simp]

theorem QuaternionAlgebra.pureNormFormIsometryEquivWeightedSumSquares_symm_apply {R : Type u_1} [CommRing R] (a b : R) (v : Fin 3 → R) : (pureNormFormIsometryEquivWeightedSumSquares a b).symm v = ⟨{ re := 0, imI := v 0, imJ := v 1, imK := v 2 }, ⋯⟩

theorem QuaternionAlgebra.equivalent_pureNormForm_weightedSumSquares {R : Type u_1} [CommRing R] (a b : R) : QuadraticMap.Equivalent (pureNormForm a b) (QuadraticMap.weightedSumSquares R ![-a, -b, a * b])

The pure norm form of ℍ[R,a,b] is ⟨-a, -b, ab⟩.

theorem Quaternion.normSq_eq_normForm {R : Type u_1} [CommRing R] (x : Quaternion R) : normSq x = (QuaternionAlgebra.normForm (-1) 0 (-1)) x

Mathlib's Quaternion.normSq is the norm form of ℍ[R] = ℍ[R,-1,0,-1].

theorem Quaternion.mem_unitary_iff_normSq_eq_one {R : Type u_1} [CommRing R] (x : Quaternion R) : x ∈ unitary (Quaternion R) ↔ normSq x = 1

A Hamilton quaternion is unitary exactly when its norm-square is one.

@[simp]

theorem Quaternion.normSq_coe_unitary_eq_one {R : Type u_1} [CommRing R] (x : ↥(unitary (Quaternion R))) : normSq ↑x = 1

The quaternion underlying a unitary Hamilton quaternion has norm-square one.