Splitting quadratic algebras

A quadratic algebra whose defining polynomial has roots r and s with unit difference is isomorphic to R × R. The two coordinates evaluate its generator at those roots. The construction reuses Mathlib's change of generator and the elementary splitting of QuadraticAlgebra R 0 1, whose generator is idempotent.

When 2 is invertible and a is the square of a unit u, the roots of QuadraticAlgebra R a 0 are u and -u. Its inverse splitting uses the half-sum and rescaled half-difference. None of these maps requires a field hypothesis on R. Under this splitting the norm and trace become the product and sum of the two coordinates, and the quadratic involution exchanges them.

def QuadraticAlgebra.algEquivProdOfIdempotent {R : Type u_1} [CommRing R] : QuadraticAlgebra R 0 1 ≃ₐ[R] R × R

The quadratic algebra with an idempotent generator is the product algebra.

@[simp]

theorem QuadraticAlgebra.algEquivProdOfIdempotent_apply {R : Type u_1} [CommRing R] (z : QuadraticAlgebra R 0 1) : algEquivProdOfIdempotent z = (z.re + z.im, z.re)

Evaluation of the idempotent-generator algebra at the roots 1 and 0.

@[simp]

theorem QuadraticAlgebra.algEquivProdOfIdempotent_symm_apply {R : Type u_1} [CommRing R] (z : R × R) : algEquivProdOfIdempotent.symm z = { re := z.2, im := z.1 - z.2 }

The inverse idempotent splitting recovers the constant and generator coefficients.

noncomputable def QuadraticAlgebra.algEquivProdOfRoots {R : Type u_1} [CommRing R] {a b : R} (r s : R) (h : IsUnit (r - s)) (ha : a = -(r * s)) (hb : b = r + s) : QuadraticAlgebra R a b ≃ₐ[R] R × R

A quadratic algebra splits by evaluation at two roots whose difference is a unit.

@[simp]

theorem QuadraticAlgebra.algEquivProdOfRoots_apply {R : Type u_1} [CommRing R] {a b : R} (r s : R) (h : IsUnit (r - s)) (ha : a = -(r * s)) (hb : b = r + s) (z : QuadraticAlgebra R a b) : (algEquivProdOfRoots r s h ha hb) z = (z.re + r * z.im, z.re + s * z.im)

Splitting evaluates each element at the two roots.

@[simp]

theorem QuadraticAlgebra.algEquivProdOfRoots_symm_apply {R : Type u_1} [CommRing R] {a b : R} (r s : R) (h : IsUnit (r - s)) (ha : a = -(r * s)) (hb : b = r + s) (z : R × R) : (algEquivProdOfRoots r s h ha hb).symm z = { re := (r * z.2 - s * z.1) * ↑h.unit⁻¹, im := (z.1 - z.2) * ↑h.unit⁻¹ }

The inverse splitting divides the coordinate difference and interpolation numerator by the unit root difference.

noncomputable def QuadraticAlgebra.algEquivProdOfSq {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (u : Rˣ) (ha : a = ↑u ^ 2) : QuadraticAlgebra R a 0 ≃ₐ[R] R × R

With 2 invertible, QuadraticAlgebra R a 0 with a = u² for a unit u splits by sending its square-root generator to (u, -u).

@[simp]

theorem QuadraticAlgebra.algEquivProdOfSq_apply {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (u : Rˣ) (ha : a = ↑u ^ 2) (z : QuadraticAlgebra R a 0) : (algEquivProdOfSq u ha) z = (z.re + ↑u * z.im, z.re - ↑u * z.im)

The unit-square specialization evaluates at the two opposite square roots.

@[simp]

theorem QuadraticAlgebra.algEquivProdOfSq_symm_apply {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (u : Rˣ) (ha : a = ↑u ^ 2) (z : R × R) : (algEquivProdOfSq u ha).symm z = { re := ⅟2 * (z.1 + z.2), im := ↑u⁻¹ * ⅟2 * (z.1 - z.2) }

The inverse splitting map recovers the half-sum and rescaled half-difference.

theorem QuadraticAlgebra.norm_eq_fst_mul_snd_algEquivProdOfSq {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (u : Rˣ) (ha : a = ↑u ^ 2) (z : QuadraticAlgebra R a 0) : norm z = ((algEquivProdOfSq u ha) z).1 * ((algEquivProdOfSq u ha) z).2

In the unit-square splitting, the norm is the product of the two coordinates.

theorem QuadraticAlgebra.trace_eq_fst_add_snd_algEquivProdOfSq {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (u : Rˣ) (ha : a = ↑u ^ 2) (z : QuadraticAlgebra R a 0) : trace z = ((algEquivProdOfSq u ha) z).1 + ((algEquivProdOfSq u ha) z).2

In the unit-square splitting, the trace is the sum of the two coordinates.

theorem QuadraticAlgebra.algEquivProdOfSq_star {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (u : Rˣ) (ha : a = ↑u ^ 2) (z : QuadraticAlgebra R a 0) : (algEquivProdOfSq u ha) (star z) = ((algEquivProdOfSq u ha) z).swap

The unit-square splitting turns the quadratic involution into the exchange of the two factors.