Change of generators in a quaternion algebra

This file proves the quaternion-symbol rescaling relations by changing the standard generators. TauCeti.QuaternionAlgebra.rescaleJEquiv identifies ℍ[R,a,c²b] with ℍ[R,a,b] by sending j to c j, for a unit c. Its first-parameter counterpart TauCeti.QuaternionAlgebra.rescaleIEquiv is obtained from it using Mathlib's QuaternionAlgebra.swapEquiv, whose formulas on the standard generators are recorded here as well.

More generally, TauCeti.QuaternionAlgebra.normMulEquiv identifies ℍ[R,a,N(z) b] with ℍ[R,a,b] for a unit z = x + y √a of QuadraticAlgebra R a 0, by sending j to (x + y i) j.

Completing the square gives the general change of generators TauCeti.QuaternionAlgebra.completeSquareEquiv, identifying ℍ[R,a,b,c] with ℍ[R,QuadraticAlgebra.discr a b,0,c] when 2 is invertible.

These equivalences are defined through QuaternionAlgebra.Basis.liftHom, Mathlib's universal property for quaternion algebras. The formulas on i, j, and k are exposed as simplification lemmas, so later proofs can use these equivalences without unfolding their construction.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter III, §2.11.

def TauCeti.QuaternionAlgebra.completeSquareEquiv {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : QuaternionAlgebra R a b c ≃ₐ[R] QuaternionAlgebra R (QuadraticAlgebra.discr a b) 0 c

Completing the square in a quaternion algebra. The change of generators i ↦ ⅟ 2 * (b + i) identifies ℍ[R,a,b,c] with the zero-linear-term presentation ℍ[R,QuadraticAlgebra.discr a b,0,c].

Equations

• TauCeti.QuaternionAlgebra.completeSquareEquiv a b c = AlgEquiv.ofAlgHom (TauCeti.completeSquareBasis✝ a b c).liftHom (TauCeti.completeSquareInvBasis✝ a b c).liftHom ⋯ ⋯

@[simp]

theorem TauCeti.QuaternionAlgebra.completeSquareEquiv_apply_i {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : (completeSquareEquiv a b c) { re := 0, imI := 1, imJ := 0, imK := 0 } = { re := ⅟2 * b, imI := ⅟2, imJ := 0, imK := 0 }

The image of the standard generator i under the completing-square equivalence.

@[simp]

theorem TauCeti.QuaternionAlgebra.completeSquareEquiv_apply_j {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : (completeSquareEquiv a b c) { re := 0, imI := 0, imJ := 1, imK := 0 } = { re := 0, imI := 0, imJ := 1, imK := 0 }

The image of the standard generator j under the completing-square equivalence.

@[simp]

theorem TauCeti.QuaternionAlgebra.completeSquareEquiv_apply_k {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : (completeSquareEquiv a b c) { re := 0, imI := 0, imJ := 0, imK := 1 } = { re := 0, imI := 0, imJ := ⅟2 * b, imK := ⅟2 }

The image of the standard generator k under the completing-square equivalence.

@[simp]

theorem TauCeti.QuaternionAlgebra.completeSquareEquiv_symm_apply_i {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : (completeSquareEquiv a b c).symm { re := 0, imI := 1, imJ := 0, imK := 0 } = { re := -b, imI := 2, imJ := 0, imK := 0 }

The image of the standard generator i under the inverse completing-square equivalence.

@[simp]

theorem TauCeti.QuaternionAlgebra.completeSquareEquiv_symm_apply_j {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : (completeSquareEquiv a b c).symm { re := 0, imI := 0, imJ := 1, imK := 0 } = { re := 0, imI := 0, imJ := 1, imK := 0 }

The image of the standard generator j under the inverse completing-square equivalence.

@[simp]

theorem TauCeti.QuaternionAlgebra.completeSquareEquiv_symm_apply_k {R : Type u_1} [CommRing R] [Invertible 2] (a b c : R) : (completeSquareEquiv a b c).symm { re := 0, imI := 0, imJ := 0, imK := 1 } = { re := 0, imI := 0, imJ := -b, imK := 2 }

The image of the standard generator k under the inverse completing-square equivalence.

def TauCeti.QuaternionAlgebra.rescaleJEquiv {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : QuaternionAlgebra R a 0 (↑c ^ 2 * b) ≃ₐ[R] QuaternionAlgebra R a 0 b

Square rescaling of the second quaternion parameter. If c is a unit, rescaling the standard generators j and k by c gives an R-algebra equivalence ℍ[R,a,c²b] ≃ₐ[R] ℍ[R,a,b].

Equations

• TauCeti.QuaternionAlgebra.rescaleJEquiv a b c = AlgEquiv.ofAlgHom (TauCeti.rescaleJHom✝ a b c) (TauCeti.rescaleJInvHom✝ a b c) ⋯ ⋯

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleJEquiv_apply_i {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleJEquiv a b c) { re := 0, imI := 1, imJ := 0, imK := 0 } = (QuaternionAlgebra.Basis.self R).i

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleJEquiv_apply_j {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleJEquiv a b c) { re := 0, imI := 0, imJ := 1, imK := 0 } = ↑c • (QuaternionAlgebra.Basis.self R).j

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleJEquiv_apply_k {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleJEquiv a b c) { re := 0, imI := 0, imJ := 0, imK := 1 } = ↑c • (QuaternionAlgebra.Basis.self R).k

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleJEquiv_symm_apply_i {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleJEquiv a b c).symm { re := 0, imI := 1, imJ := 0, imK := 0 } = (QuaternionAlgebra.Basis.self R).i

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleJEquiv_symm_apply_j {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleJEquiv a b c).symm { re := 0, imI := 0, imJ := 1, imK := 0 } = ↑c⁻¹ • (QuaternionAlgebra.Basis.self R).j

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleJEquiv_symm_apply_k {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleJEquiv a b c).symm { re := 0, imI := 0, imJ := 0, imK := 1 } = ↑c⁻¹ • (QuaternionAlgebra.Basis.self R).k

@[simp]

theorem TauCeti.QuaternionAlgebra.swapEquiv_apply_i {R : Type u_1} [CommRing R] (a b : R) : (QuaternionAlgebra.swapEquiv a b) { re := 0, imI := 1, imJ := 0, imK := 0 } = (QuaternionAlgebra.Basis.self R).j

Mathlib's QuaternionAlgebra.swapEquiv sends i to j.

@[simp]

theorem TauCeti.QuaternionAlgebra.swapEquiv_apply_j {R : Type u_1} [CommRing R] (a b : R) : (QuaternionAlgebra.swapEquiv a b) { re := 0, imI := 0, imJ := 1, imK := 0 } = (QuaternionAlgebra.Basis.self R).i

Mathlib's QuaternionAlgebra.swapEquiv sends j to i.

@[simp]

theorem TauCeti.QuaternionAlgebra.swapEquiv_symm_apply_i {R : Type u_1} [CommRing R] (a b : R) : (QuaternionAlgebra.swapEquiv a b).symm { re := 0, imI := 1, imJ := 0, imK := 0 } = (QuaternionAlgebra.Basis.self R).j

The inverse of Mathlib's QuaternionAlgebra.swapEquiv sends i to j.

@[simp]

theorem TauCeti.QuaternionAlgebra.swapEquiv_symm_apply_j {R : Type u_1} [CommRing R] (a b : R) : (QuaternionAlgebra.swapEquiv a b).symm { re := 0, imI := 0, imJ := 1, imK := 0 } = (QuaternionAlgebra.Basis.self R).i

The inverse of Mathlib's QuaternionAlgebra.swapEquiv sends j to i.

def TauCeti.QuaternionAlgebra.rescaleIEquiv {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : QuaternionAlgebra R (↑c ^ 2 * a) 0 b ≃ₐ[R] QuaternionAlgebra R a 0 b

Square rescaling of the first quaternion parameter. This is the first-parameter version of TauCeti.QuaternionAlgebra.rescaleJEquiv, obtained by exchanging i and j before and after rescaling.

Equations

• TauCeti.QuaternionAlgebra.rescaleIEquiv a b c = (QuaternionAlgebra.swapEquiv (↑c ^ 2 * a) b).trans ((TauCeti.QuaternionAlgebra.rescaleJEquiv b a c).trans (QuaternionAlgebra.swapEquiv b a))

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleIEquiv_apply_i {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleIEquiv a b c) { re := 0, imI := 1, imJ := 0, imK := 0 } = ↑c • (QuaternionAlgebra.Basis.self R).i

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleIEquiv_apply_j {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleIEquiv a b c) { re := 0, imI := 0, imJ := 1, imK := 0 } = (QuaternionAlgebra.Basis.self R).j

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleIEquiv_apply_k {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleIEquiv a b c) { re := 0, imI := 0, imJ := 0, imK := 1 } = ↑c • (QuaternionAlgebra.Basis.self R).k

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleIEquiv_symm_apply_i {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleIEquiv a b c).symm { re := 0, imI := 1, imJ := 0, imK := 0 } = ↑c⁻¹ • (QuaternionAlgebra.Basis.self R).i

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleIEquiv_symm_apply_j {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleIEquiv a b c).symm { re := 0, imI := 0, imJ := 1, imK := 0 } = (QuaternionAlgebra.Basis.self R).j

@[simp]

theorem TauCeti.QuaternionAlgebra.rescaleIEquiv_symm_apply_k {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : (rescaleIEquiv a b c).symm { re := 0, imI := 0, imJ := 0, imK := 1 } = ↑c⁻¹ • (QuaternionAlgebra.Basis.self R).k

def TauCeti.QuaternionAlgebra.normMulEquiv {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : QuaternionAlgebra R a 0 (QuadraticAlgebra.norm ↑z * b) ≃ₐ[R] QuaternionAlgebra R a 0 b

Norm rescaling of the second quaternion parameter. For a unit z = x + y √a of the quadratic algebra R[√a] = QuadraticAlgebra R a 0, sending j to (x + y i) j gives an R-algebra equivalence ℍ[R,a,N(z) b] ≃ₐ[R] ℍ[R,a,b]. The quaternion symbol (a, b) therefore depends on b only up to norms of units of R[√a]; TauCeti.QuaternionAlgebra.rescaleJEquiv is the analogous statement for a unit scalar c, whose norm is c².

Equations

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

@[simp]

theorem TauCeti.QuaternionAlgebra.normMulEquiv_apply_i {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : (normMulEquiv a b z) { re := 0, imI := 1, imJ := 0, imK := 0 } = { re := 0, imI := 1, imJ := 0, imK := 0 }

@[simp]

theorem TauCeti.QuaternionAlgebra.normMulEquiv_apply_j {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : (normMulEquiv a b z) { re := 0, imI := 0, imJ := 1, imK := 0 } = { re := 0, imI := 0, imJ := (↑z).re, imK := (↑z).im }

@[simp]

theorem TauCeti.QuaternionAlgebra.normMulEquiv_apply_k {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : (normMulEquiv a b z) { re := 0, imI := 0, imJ := 0, imK := 1 } = { re := 0, imI := 0, imJ := a * (↑z).im, imK := (↑z).re }

@[simp]

theorem TauCeti.QuaternionAlgebra.normMulEquiv_symm_apply_i {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : (normMulEquiv a b z).symm { re := 0, imI := 1, imJ := 0, imK := 0 } = { re := 0, imI := 1, imJ := 0, imK := 0 }

@[simp]

theorem TauCeti.QuaternionAlgebra.normMulEquiv_symm_apply_j {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : (normMulEquiv a b z).symm { re := 0, imI := 0, imJ := 1, imK := 0 } = { re := 0, imI := 0, imJ := (↑z⁻¹).re, imK := (↑z⁻¹).im }

@[simp]

theorem TauCeti.QuaternionAlgebra.normMulEquiv_symm_apply_k {R : Type u_1} [CommRing R] (a b : R) (z : (QuadraticAlgebra R a 0)ˣ) : (normMulEquiv a b z).symm { re := 0, imI := 0, imJ := 0, imK := 1 } = { re := 0, imI := 0, imJ := a * (↑z⁻¹).im, imK := (↑z⁻¹).re }