The norm form on O_d

Thesis. §3.2, the norm form N(a + bτ) = a² + d·a·b + ((d² − d)/4)·b² and its multiplicativity (this is the norm used throughout the ideal-counting of §3.1–§3.3).

This file proves:

• normForm — the integer norm form N(a, b)
• normForm_mul — multiplicativity N(αβ) = N(α)·N(β)
• tauConj — the Galois conjugate tauConj = d − τ (other root of poly d)
• tau_add_tauConj / tau_mul_tauConj — the Vieta relations
• normForm_eq_mul_conj— (a + bτ)(a + btauConj) = N(a, b)

Divergence from thesis. The thesis states N(a + bτ) directly as a quadratic form. Here it is derived and shown multiplicative through the Galois conjugate tauConj and the Vieta relations τ + tauConj = d, τ·tauConj = (d²−d)/4, which exhibit N as an honest multiplicative norm α ↦ α·alphaConj. The end formula agrees with the thesis; the route via tauConj is a Lean-idiomatic reformulation.

Norm form

noncomputable def QuadraticOrder.normForm (d a b : ℤ) : ℤ

The norm form on QuadraticOrder d: the norm of a + b·τ is a² + d·a·b + ((d²-d)/4)·b².

Derivation: N(a + bτ) = (a + bτ)(a + b(d - τ)), using the fact that τ and d - τ are the two roots of X² - dX + (d²-d)/4. Expanding: a² + ab(d - τ) + abτ + b²τ(d - τ) = a² + abd + b²·τ(d-τ). Since τ² - dτ + (d²-d)/4 = 0, we have τ(d - τ) = (d²-d)/4, giving the formula.

Equations

• QuadraticOrder.normForm d a b = a ^ 2 + d * a * b + (d ^ 2 - d) / 4 * b ^ 2

theorem QuadraticOrder.normForm_mul {d : ℤ} (a b c e : ℤ) : normForm d (a * c - (d ^ 2 - d) / 4 * (b * e)) (a * e + b * c + d * b * e) = normForm d a b * normForm d c e

The norm form is multiplicative: N(αβ) = N(α)·N(β).

This follows from the ring-identity that holds for any integers a, b, c, e, d, and any integer q substituted for (d²-d)/4.

Conjugate and norm involution

The element tauConj := d • 1 - tau is the "Galois conjugate" of tau: it is the other root of poly d. Together with tau, it satisfies the standard Vieta relations, and exhibits normForm as a multiplicative norm via the factorisation (a + b·τ)(a + b·tauConj) = N(a, b).

noncomputable def QuadraticOrder.tauConj {d : ℤ} : QuadraticOrder d

The Galois conjugate of tau: the other root of poly d.

Equations

• QuadraticOrder.tauConj = d • 1 - QuadraticOrder.tau

theorem QuadraticOrder.tau_add_tauConj {d : ℤ} : tau + tauConj = d • 1

Vieta: the sum of the roots of poly d equals d.

theorem QuadraticOrder.tau_mul_tauConj {d : ℤ} : tau * tauConj = ((d ^ 2 - d) / 4) • 1

Vieta: the product of the roots of poly d equals (d^2 - d) / 4.

theorem QuadraticOrder.tauConj_minimal_poly {d : ℤ} : tauConj ^ 2 - d • tauConj + ((d ^ 2 - d) / 4) • 1 = 0

The conjugate tauConj is also a root of the defining polynomial poly d.

@[simp]

theorem QuadraticOrder.poly_aeval_tauConj {d : ℤ} : (Polynomial.aeval tauConj) (poly d) = 0

The Galois conjugate tauConj is also a root of poly d.

theorem QuadraticOrder.normForm_eq_mul_conj {d : ℤ} (a b : ℤ) : (a • 1 + b • tau) * (a • 1 + b • tauConj) = normForm d a b • 1

The norm involution: (a + b·τ)(a + b·tauConj) = N(a, b). This exhibits the conjugate as the involution under which normForm is the multiplicative norm.