Algebra equivalences of quaternion algebras

An algebra equivalence between two quaternion algebras is compatible with all of their quadratic-form structure: it commutes with quaternion conjugation, preserves the reduced trace and the reduced norm, maps the pure quaternions onto the pure quaternions, and therefore restricts to an isometry of pure norm forms. In the classical presentation ℍ[R,a,b], this turns an isomorphism ℍ[R,a,b] ≃ₐ[R] ℍ[R,c,d] into an isometry of ternary diagonal forms ⟨-a, -b, ab⟩ ≅ ⟨-c, -d, cd⟩. It is the step that lets an equality of quaternion algebras up to isomorphism be read back as an isometry of quadratic forms, as in the classification of forms of dimension three by their determinant and their quaternion algebra.

The one input is intrinsic: the trace of left multiplication by x on the free module ℍ[R,c₁,c₂,c₃] is twice the reduced trace x + star x = 2 x.re + c₂ x.imI (QuaternionAlgebra.trace_mulLeft). An algebra equivalence conjugates left multiplication by x into left multiplication by its image, so it preserves this trace; once 2 is cancellable it preserves the reduced trace, and star x = (x + star x) - x is then preserved as well. Everything else follows formally from QuaternionAlgebra.self_mul_star.

Main results

• QuaternionAlgebra.trace_mulLeft: the trace of left multiplication by a quaternion.
• QuaternionAlgebra.reducedTrace_eq_of_algEquiv: an algebra equivalence preserves the reduced trace.
• QuaternionAlgebra.map_star_of_algEquiv: an algebra equivalence of quaternion algebras commutes with conjugation, so that StarAlgEquiv.ofAlgEquiv makes it a ⋆-algebra equivalence.
• QuaternionAlgebra.normForm_eq_of_algEquiv: it preserves the reduced norm, and QuaternionAlgebra.normFormIsometryEquivOfAlgEquiv is the resulting isometry of norm forms.
• QuaternionAlgebra.re_eq_of_algEquiv and QuaternionAlgebra.map_ker_reₗ_of_algEquiv: between algebras ℍ[R,a,b] it preserves real parts and maps the pure quaternions onto the pure quaternions.
• QuaternionAlgebra.pureNormFormIsometryEquivOfAlgEquiv: the restricted isometry of pure norm forms, and QuaternionAlgebra.equivalent_weightedSumSquares_of_algEquiv: isomorphic quaternion algebras ℍ[R,a,b] and ℍ[R,c,d] have isometric forms ⟨-a, -b, ab⟩ and ⟨-c, -d, cd⟩.

Implementation notes

Everything is stated over a commutative ring in which 2 is regular, which is exactly what the proof consumes; over a field this is the standing hypothesis that 2 is invertible. Some such hypothesis is needed for the argument: when 2 = 0 and c₂ = 0 the trace of left multiplication vanishes identically, so it carries no information about conjugation.

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.

theorem QuaternionAlgebra.trace_mulLeft {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} (x : QuaternionAlgebra R c₁ c₂ c₃) : (LinearMap.trace R (QuaternionAlgebra R c₁ c₂ c₃)) (LinearMap.mulLeft R x) = 2 * (2 * x.re + c₂ * x.imI)

The trace of left multiplication by a quaternion x is twice its reduced trace x + star x = 2 x.re + c₂ x.imI.

theorem QuaternionAlgebra.reducedTrace_eq_of_algEquiv {R : Type u_1} [CommRing R] {c₁ c₂ c₃ d₁ d₂ d₃ : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] QuaternionAlgebra R d₁ d₂ d₃) (x : QuaternionAlgebra R c₁ c₂ c₃) : 2 * (f x).re + d₂ * (f x).imI = 2 * x.re + c₂ * x.imI

An algebra equivalence of quaternion algebras preserves the reduced trace, in coordinates.

theorem QuaternionAlgebra.map_star_of_algEquiv {R : Type u_1} [CommRing R] {c₁ c₂ c₃ d₁ d₂ d₃ : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] QuaternionAlgebra R d₁ d₂ d₃) (x : QuaternionAlgebra R c₁ c₂ c₃) : f (star x) = star (f x)

An algebra equivalence of quaternion algebras commutes with conjugation, once 2 is regular. Together with StarAlgEquiv.ofAlgEquiv this makes every such equivalence a ⋆-algebra equivalence.

@[simp]

theorem QuaternionAlgebra.normForm_eq_of_algEquiv {R : Type u_1} [CommRing R] {c₁ c₂ c₃ d₁ d₂ d₃ : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] QuaternionAlgebra R d₁ d₂ d₃) (x : QuaternionAlgebra R c₁ c₂ c₃) : (normForm d₁ d₂ d₃) (f x) = (normForm c₁ c₂ c₃) x

An algebra equivalence of quaternion algebras preserves the reduced norm.

def QuaternionAlgebra.normFormIsometryEquivOfAlgEquiv {R : Type u_1} [CommRing R] {c₁ c₂ c₃ d₁ d₂ d₃ : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] QuaternionAlgebra R d₁ d₂ d₃) : QuadraticMap.IsometryEquiv (normForm c₁ c₂ c₃) (normForm d₁ d₂ d₃)

An algebra equivalence of quaternion algebras, viewed as an isometry of their norm forms.

Equations

• QuaternionAlgebra.normFormIsometryEquivOfAlgEquiv h2 f = { toLinearEquiv := ↑f, map_app' := ⋯ }

@[simp]

theorem QuaternionAlgebra.normFormIsometryEquivOfAlgEquiv_apply {R : Type u_1} [CommRing R] {c₁ c₂ c₃ d₁ d₂ d₃ : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] QuaternionAlgebra R d₁ d₂ d₃) (x : QuaternionAlgebra R c₁ c₂ c₃) : (normFormIsometryEquivOfAlgEquiv h2 f) x = f x

@[simp]

theorem QuaternionAlgebra.re_eq_of_algEquiv {R : Type u_1} [CommRing R] {a b c d : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d) (x : QuaternionAlgebra R a 0 b) : (f x).re = x.re

An algebra equivalence between quaternion algebras ℍ[R,a,b] preserves real parts.

theorem QuaternionAlgebra.map_ker_reₗ_of_algEquiv {R : Type u_1} [CommRing R] {a b c d : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d) : Submodule.map (↑↑f) (reₗ a 0 b).ker = (reₗ c 0 d).ker

An algebra equivalence between quaternion algebras ℍ[R,a,b] maps the pure quaternions onto the pure quaternions.

def QuaternionAlgebra.pureNormFormIsometryEquivOfAlgEquiv {R : Type u_1} [CommRing R] {a b c d : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d) : QuadraticMap.IsometryEquiv (pureNormForm a b) (pureNormForm c d)

An algebra equivalence ℍ[R,a,b] ≃ₐ[R] ℍ[R,c,d], restricted to the pure quaternions, as an isometry of the pure norm forms.

Equations

• QuaternionAlgebra.pureNormFormIsometryEquivOfAlgEquiv h2 f = { toLinearEquiv := (↑f).ofSubmodules (QuaternionAlgebra.reₗ a 0 b).ker (QuaternionAlgebra.reₗ c 0 d).ker ⋯, map_app' := ⋯ }

@[simp]

theorem QuaternionAlgebra.coe_pureNormFormIsometryEquivOfAlgEquiv_apply {R : Type u_1} [CommRing R] {a b c d : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d) (x : ↥(reₗ a 0 b).ker) : ↑((pureNormFormIsometryEquivOfAlgEquiv h2 f) x) = f ↑x

theorem QuaternionAlgebra.equivalent_pureNormForm_of_algEquiv {R : Type u_1} [CommRing R] {a b c d : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d) : QuadraticMap.Equivalent (pureNormForm a b) (pureNormForm c d)

Isomorphic quaternion algebras have isometric pure norm forms.

theorem QuaternionAlgebra.equivalent_weightedSumSquares_of_algEquiv {R : Type u_1} [CommRing R] {a b c d : R} (h2 : IsRegular 2) (f : QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d) : (QuadraticMap.weightedSumSquares R ![-a, -b, a * b]).Equivalent (QuadraticMap.weightedSumSquares R ![-c, -d, c * d])

Isomorphic quaternion algebras ℍ[R,a,b] and ℍ[R,c,d] have isometric ternary forms ⟨-a, -b, ab⟩ and ⟨-c, -d, cd⟩, the diagonalizations of their pure norm forms.