Quadratic algebras : involution and norm.

Let R be a commutative ring. We define:

• QuadraticAlgebra.star : the quadratic involution

• QuadraticAlgebra.norm : the norm

We prove :

• QuadraticAlgebra.isUnit_iff_norm_isUnit: w : QuadraticAlgebra R a b is a unit iff w.norm is a unit in R.

• QuadraticAlgebra.norm_mem_nonZero_divisors_iff: w : QuadraticAlgebra R a b isn't a zero divisor iff w.norm isn't a zero divisor in R.

• If R is a field, and ∀ r, r ^ 2 ≠ a + b * r, then QuadraticAlgebra R a b is a field.

Warning

If you are working over ℚ, note the existence of the diamond explained in Mathlib.Algebra.QuadraticAlgebra.Defs.

def QuadraticAlgebra.omega {R : Type u_1} {a b : R} [Zero R] [One R] : QuadraticAlgebra R a b

The representative of the root in the quadratic algebra

def QuadraticAlgebra.termω : Lean.ParserDescr

the canonical element ⟨0, 1⟩ in a quadratic algebra QuadraticAlgebra R a b.

@[simp]

theorem QuadraticAlgebra.omega_re {R : Type u_1} {a b : R} [Zero R] [One R] : omega.re = 0

@[simp]

theorem QuadraticAlgebra.omega_im {R : Type u_1} {a b : R} [Zero R] [One R] : omega.im = 1

theorem QuadraticAlgebra.omega_mul_omega_eq_mk {R : Type u_1} {a b : R} [CommSemiring R] : omega * omega = { re := a, im := b }

theorem QuadraticAlgebra.omega_mul_omega_eq_add {R : Type u_1} {a b : R} [CommSemiring R] : omega * omega = a • 1 + b • omega

@[simp]

theorem QuadraticAlgebra.omega_mul_mk {R : Type u_1} {a b : R} [CommSemiring R] (x y : R) : omega * { re := x, im := y } = { re := a * y, im := x + b * y }

@[simp]

theorem QuadraticAlgebra.omega_mul_algebraMap_mul_mk {R : Type u_1} {a b : R} [CommSemiring R] (n x y : R) : omega * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } = { re := a * n * y, im := n * x + n * b * y }

@[deprecated QuadraticAlgebra.omega_mul_algebraMap_mul_mk (since := "2025-12-15")]

theorem QuadraticAlgebra.omega_mul_coe_mul_mk {R : Type u_1} {a b : R} [CommSemiring R] (n x y : R) : omega * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } = { re := a * n * y, im := n * x + n * b * y }

Alias of QuadraticAlgebra.omega_mul_algebraMap_mul_mk.

theorem QuadraticAlgebra.mk_eq_add_smul_omega {R : Type u_1} {a b : R} [CommSemiring R] (x y : R) : { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x + y • omega

theorem QuadraticAlgebra.algHom_ext {R : Type u_1} {a b : R} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] {f g : QuadraticAlgebra R a b →ₐ[R] A} (h : f omega = g omega) : f = g

theorem QuadraticAlgebra.algHom_ext_iff {R : Type u_1} {a b : R} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] {f g : QuadraticAlgebra R a b →ₐ[R] A} : f = g ↔ f omega = g omega

def QuadraticAlgebra.lift {R : Type u_1} {a b : R} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] : { u : A // u * u = a • 1 + b • u } ≃ (QuadraticAlgebra R a b →ₐ[R] A)

The unique AlgHom from QuadraticAlgebra R a b to an R-algebra A, constructed by replacing ω with the provided root. Conversely, this associates to every algebra morphism QuadraticAlgebra R a b →ₐ[R] A a value of ω in A.

@[simp]

theorem QuadraticAlgebra.lift_symm_apply_coe {R : Type u_1} {a b : R} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] (f : QuadraticAlgebra R a b →ₐ[R] A) : ↑(lift.symm f) = f omega

@[simp]

theorem QuadraticAlgebra.lift_apply_apply {R : Type u_1} {a b : R} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] (u : { u : A // u * u = a • 1 + b • u }) (z : QuadraticAlgebra R a b) : (lift u) z = z.re • 1 + z.im • ↑u

@[implicit_reducible]

instance QuadraticAlgebra.instStar {R : Type u_1} {a b : R} [CommRing R] : Star (QuadraticAlgebra R a b)

Conjugation in QuadraticAlgebra R a b. The conjugate of x + y ω is x + y ω' = (x - a * y) - y ω.

@[simp]

theorem QuadraticAlgebra.star_mk {R : Type u_1} {a b : R} [CommRing R] (x y : R) : star { re := x, im := y } = { re := x + b * y, im := -y }

@[simp]

theorem QuadraticAlgebra.re_star {R : Type u_1} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (star z).re = z.re + b * z.im

@[simp]

theorem QuadraticAlgebra.im_star {R : Type u_1} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (star z).im = -z.im

theorem QuadraticAlgebra.mul_star {R : Type u_1} {a b : R} [CommRing R] (x y : R) : { re := x, im := y } * star { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x + (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) y - (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y * (algebraMap R (QuadraticAlgebra R a b)) y

@[implicit_reducible]

instance QuadraticAlgebra.instStarRing {R : Type u_1} {a b : R} [CommRing R] : StarRing (QuadraticAlgebra R a b)

def QuadraticAlgebra.norm {R : Type u_1} {a b : R} [CommRing R] : QuadraticAlgebra R a b →* R

the norm in a quadratic algebra, as a MonoidHom.

theorem QuadraticAlgebra.norm_def {R : Type u_1} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : norm z = z.re * z.re + b * z.re * z.im - a * z.im * z.im

@[simp]

theorem QuadraticAlgebra.norm_zero {R : Type u_1} {a b : R} [CommRing R] : norm 0 = 0

@[simp]

theorem QuadraticAlgebra.norm_one {R : Type u_1} {a b : R} [CommRing R] : norm 1 = 1

@[simp]

theorem QuadraticAlgebra.norm_algebraMap {R : Type u_1} {a b : R} [CommRing R] (r : R) : norm ((algebraMap R (QuadraticAlgebra R a b)) r) = r ^ 2

@[deprecated QuadraticAlgebra.norm_algebraMap (since := "2025-12-15")]

theorem QuadraticAlgebra.norm_coe {R : Type u_1} {a b : R} [CommRing R] (r : R) : norm ((algebraMap R (QuadraticAlgebra R a b)) r) = r ^ 2

Alias of QuadraticAlgebra.norm_algebraMap.

@[simp]

theorem QuadraticAlgebra.norm_natCast {R : Type u_1} {a b : R} [CommRing R] (n : ℕ) : norm ↑n = ↑n ^ 2

@[simp]

theorem QuadraticAlgebra.norm_intCast {R : Type u_1} {a b : R} [CommRing R] (n : ℤ) : norm ↑n = ↑n ^ 2

theorem QuadraticAlgebra.algebraMap_norm_eq_mul_star {R : Type u_1} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (algebraMap R (QuadraticAlgebra R a b)) (norm z) = z * star z

@[deprecated QuadraticAlgebra.algebraMap_norm_eq_mul_star (since := "2025-12-15")]

theorem QuadraticAlgebra.coe_norm_eq_mul_star {R : Type u_1} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (algebraMap R (QuadraticAlgebra R a b)) (norm z) = z * star z

Alias of QuadraticAlgebra.algebraMap_norm_eq_mul_star.

@[simp]

theorem QuadraticAlgebra.norm_neg {R : Type u_1} {a b : R} [CommRing R] (x : QuadraticAlgebra R a b) : norm (-x) = norm x

@[simp]

theorem QuadraticAlgebra.norm_star {R : Type u_1} {a b : R} [CommRing R] (x : QuadraticAlgebra R a b) : norm (star x) = norm x

theorem QuadraticAlgebra.isUnit_iff_norm_isUnit {R : Type u_1} {a b : R} [CommRing R] {x : QuadraticAlgebra R a b} : IsUnit x ↔ IsUnit (norm x)

theorem QuadraticAlgebra.norm_eq_one_iff_mem_unitary {R : Type u_1} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z = 1 ↔ z ∈ unitary (QuadraticAlgebra R a b)

An element of QuadraticAlgebra R a b has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem QuadraticAlgebra.mem_unitary {R : Type u_1} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z = 1 → z ∈ unitary (QuadraticAlgebra R a b)

Alias of the forward direction of QuadraticAlgebra.norm_eq_one_iff_mem_unitary.

---

An element of QuadraticAlgebra R a b has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem QuadraticAlgebra.norm_eq_one {R : Type u_1} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : z ∈ unitary (QuadraticAlgebra R a b) → norm z = 1

Alias of the reverse direction of QuadraticAlgebra.norm_eq_one_iff_mem_unitary.

---

An element of QuadraticAlgebra R a b has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem QuadraticAlgebra.mker_norm_eq_unitary {R : Type u_1} {a b : R} [CommRing R] : MonoidHom.mker norm = unitary (QuadraticAlgebra R a b)

The kernel of the norm map on QuadraticAlgebra R a b equals the submonoid of unitary elements.

theorem QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff {R : Type u_1} {a b : R} [CommRing R] {r : R} : (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R

@[deprecated QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff (since := "2025-12-15")]

theorem QuadraticAlgebra.coe_mem_nonZeroDivisors_iff {R : Type u_1} {a b : R} [CommRing R] {r : R} : (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R

Alias of QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff.

theorem QuadraticAlgebra.star_mem_nonZeroDivisors {R : Type u_1} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} (hz : z ∈ nonZeroDivisors (QuadraticAlgebra R a b)) : star z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.star_mem_nonZeroDivisors_iff {R : Type u_1} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : star z ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.norm_mem_nonZeroDivisors_iff {R : Type u_1} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z ∈ nonZeroDivisors R ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.norm_eq_zero_iff_eq_zero {R : Type u_1} {a b : R} [Field R] [Hab : Fact (∀ (r : R), r ^ 2 ≠ a + b * r)] {z : QuadraticAlgebra R a b} : norm z = 0 ↔ z = 0

@[implicit_reducible]

instance QuadraticAlgebra.instField {R : Type u_1} {a b : R} [Field R] [Hab : Fact (∀ (r : R), r ^ 2 ≠ a + b * r)] : Field (QuadraticAlgebra R a b)

If R is a field and there is no r : R such that r ^ 2 = a + b * r, then QuadraticAlgebra R a b is a field.