Quadratic algebras: involution, norm, and trace.

Let R be a commutative ring. We define:

• QuadraticAlgebra.star: the quadratic involution

• QuadraticAlgebra.norm: the norm

• QuadraticAlgebra.trace: the trace, as an R-linear map

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_nonZeroDivisors_iff: w : QuadraticAlgebra R a b isn't a zero divisor iff w.norm isn't a zero divisor in R.

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

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

The representative of the root in the quadratic algebra

Equations

• QuadraticAlgebra.omega = { re := 0, im := 1 }

def QuadraticAlgebra.termω : Lean.ParserDescr

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

Equations

• QuadraticAlgebra.termω = Lean.ParserDescr.node `QuadraticAlgebra.termω 1024 (Lean.ParserDescr.symbol "ω")

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem QuadraticAlgebra.omega_mul_mk {R : Type u_2} {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_2} {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 }

theorem QuadraticAlgebra.mk_eq_add_smul_omega {R : Type u_2} {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_2} {a b : R} [CommSemiring R] {A : Type u_3} [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_2} {a b : R} [CommSemiring R] {A : Type u_3} [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_2} {a b : R} [CommSemiring R] {A : Type u_3} [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.

Equations

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

@[simp]

theorem QuadraticAlgebra.lift_apply_apply {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [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

@[simp]

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

@[instance_reducible]

instance QuadraticAlgebra.instStar {R : Type u_2} {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 + b * y) - y ω.

Equations

• QuadraticAlgebra.instStar = { star := fun (z : QuadraticAlgebra R a b) => { re := z.re + b * z.im, im := -z.im } }

@[simp]

theorem QuadraticAlgebra.star_mk {R : Type u_2} {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_2} {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_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (star z).im = -z.im

theorem QuadraticAlgebra.mul_star {R : Type u_2} {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

@[instance_reducible]

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

Equations

• QuadraticAlgebra.instStarRing = { toStar := QuadraticAlgebra.instStar, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

theorem QuadraticAlgebra.sub_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : z - star z = z.im • (omega - star omega)

z - star z is a multiple of the difference ω - star ω.

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

the norm in a quadratic algebra, as a MonoidHom.

Equations

• QuadraticAlgebra.norm = { toFun := fun (z : QuadraticAlgebra R a b) => z.re * z.re + b * z.re * z.im - a * z.im * z.im, map_one' := ⋯, map_mul' := ⋯ }

theorem QuadraticAlgebra.norm_def {R : Type u_2} {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_2} {a b : R} [CommRing R] : norm 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem QuadraticAlgebra.isUnit_iff_norm_isUnit {R : Type u_2} {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_2} {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.norm_eq_one {R : Type u_2} {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.mem_unitary {R : Type u_2} {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.mker_norm_eq_unitary {R : Type u_2} {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_2} {a b : R} [CommRing R] {r : R} : (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R

theorem QuadraticAlgebra.star_mem_nonZeroDivisors {R : Type u_2} {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_2} {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_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z ∈ nonZeroDivisors R ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

def QuadraticAlgebra.trace {R : Type u_2} {a b : R} [CommRing R] : QuadraticAlgebra R a b →ₗ[R] R

The trace in a quadratic algebra, as an R-linear map.

Equations

• QuadraticAlgebra.trace = { toFun := fun (z : QuadraticAlgebra R a b) => 2 * z.re + b * z.im, map_add' := ⋯, map_smul' := ⋯ }

theorem QuadraticAlgebra.trace_def {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : trace z = 2 * z.re + b * z.im

@[simp]

theorem QuadraticAlgebra.trace_algebraMap {R : Type u_2} {a b : R} [CommRing R] (r : R) : trace ((algebraMap R (QuadraticAlgebra R a b)) r) = 2 * r

@[simp]

theorem QuadraticAlgebra.trace_natCast {R : Type u_2} {a b : R} [CommRing R] (n : ℕ) : trace ↑n = 2 * ↑n

@[simp]

theorem QuadraticAlgebra.trace_intCast {R : Type u_2} {a b : R} [CommRing R] (n : ℤ) : trace ↑n = 2 * ↑n

@[simp]

theorem QuadraticAlgebra.trace_omega {R : Type u_2} {a b : R} [CommRing R] : trace omega = b

@[simp]

theorem QuadraticAlgebra.trace_one {R : Type u_2} {a b : R} [CommRing R] : trace 1 = 2

@[simp]

theorem QuadraticAlgebra.trace_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : trace (star z) = trace z

theorem QuadraticAlgebra.algebraMap_trace_eq_add_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (algebraMap R (QuadraticAlgebra R a b)) (trace z) = z + star z

z + star z is the trace of z.

theorem QuadraticAlgebra.star_eq {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : star z = (algebraMap R (QuadraticAlgebra R a b)) (trace z) - z

The conjugate of z is trace z - z.

theorem QuadraticAlgebra.sq_sub_trace_smul_add_norm_eq_zero {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : z ^ 2 - trace z • z + (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 0

Every element of a quadratic algebra satisfies its characteristic equation.

theorem QuadraticAlgebra.sq_eq_trace_smul_sub_norm {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : z ^ 2 = trace z • z - (algebraMap R (QuadraticAlgebra R a b)) (norm z)

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

@[instance_reducible]

instance QuadraticAlgebra.instNNRatCast {K : Type u_1} [Field K] {a b : K} : NNRatCast (QuadraticAlgebra K a b)

Equations

• QuadraticAlgebra.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => { re := ↑q, im := 0 } }

@[simp]

theorem QuadraticAlgebra.re_nnratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ≥0) : (NNRatCast.nnratCast q).re = ↑q

@[simp]

theorem QuadraticAlgebra.im_nnratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ≥0) : (NNRatCast.nnratCast q).im = 0

@[instance_reducible]

instance QuadraticAlgebra.instRatCast {K : Type u_1} [Field K] {a b : K} : RatCast (QuadraticAlgebra K a b)

Equations

• QuadraticAlgebra.instRatCast = { ratCast := fun (q : ℚ) => { re := ↑q, im := 0 } }

@[simp]

theorem QuadraticAlgebra.re_ratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ) : (RatCast.ratCast q).re = ↑q

@[simp]

theorem QuadraticAlgebra.im_ratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ) : (RatCast.ratCast q).im = 0

@[instance_reducible]

instance QuadraticAlgebra.instInv {K : Type u_1} [Field K] {a b : K} : Inv (QuadraticAlgebra K a b)

Equations

• QuadraticAlgebra.instInv = { inv := fun (z : QuadraticAlgebra K a b) => (QuadraticAlgebra.norm z)⁻¹ • star z }

theorem QuadraticAlgebra.inv_def {K : Type u_1} [Field K] {a b : K} (z : QuadraticAlgebra K a b) : z⁻¹ = (norm z)⁻¹ • star z

@[simp]

theorem QuadraticAlgebra.re_inv {K : Type u_1} [Field K] {a b : K} (z : QuadraticAlgebra K a b) : z⁻¹.re = (norm z)⁻¹ * (z.re + b * z.im)

@[simp]

theorem QuadraticAlgebra.im_inv {K : Type u_1} [Field K] {a b : K} (z : QuadraticAlgebra K a b) : z⁻¹.im = -((norm z)⁻¹ * z.im)

@[instance_reducible]

instance QuadraticAlgebra.instDiv {K : Type u_1} [Field K] {a b : K} : Div (QuadraticAlgebra K a b)

Equations

• QuadraticAlgebra.instDiv = { div := fun (w z : QuadraticAlgebra K a b) => w * z⁻¹ }

theorem QuadraticAlgebra.div_def {K : Type u_1} [Field K] {a b : K} (w z : QuadraticAlgebra K a b) : w / z = w * z⁻¹

@[simp]

theorem QuadraticAlgebra.re_div {K : Type u_1} [Field K] {a b : K} (w z : QuadraticAlgebra K a b) : (w / z).re = w.re * ((norm z)⁻¹ * (z.re + b * z.im)) + -(a * w.im * ((norm z)⁻¹ * z.im))

@[simp]

theorem QuadraticAlgebra.im_div {K : Type u_1} [Field K] {a b : K} (w z : QuadraticAlgebra K a b) : (w / z).im = -(w.re * ((norm z)⁻¹ * z.im)) + w.im * ((norm z)⁻¹ * (z.re + b * z.im)) + -(b * w.im * ((norm z)⁻¹ * z.im))

@[instance_reducible]

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

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

Equations

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