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. `

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

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_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_coe_mul_mk {R : Type u_1} {a b : R} [CommSemiring R] (n x y : R) : omega * ↑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_1} {a b : R} [CommSemiring R] (x y : R) : { re := x, im := y } = ↑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.

Equations

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

@[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

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 ω.

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_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 } = ↑x * ↑x + ↑b * ↑x * ↑y - ↑a * ↑y * ↑y

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

Equations

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

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.

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_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_coe {R : Type u_1} {a b : R} [CommRing R] (r : R) : norm ↑r = r ^ 2

@[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.coe_norm_eq_mul_star {R : Type u_1} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : ↑(norm z) = z * star z

@[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.coe_mem_nonZeroDivisors_iff {R : Type u_1} {a b : R} [CommRing R] {r : R} : ↑r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R

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

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.

Equations

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