The trace and the norm of a quadratic irrationality

An element x of a degree-2 extension E/F that does not lie in F satisfies a monic quadratic x² = t x - d over F, and the pair (1, x) is then an F-basis of E. In that basis multiplication by x is the companion matrix TauCeti.companionFinTwo t d of X² - t X + d, which is the reading of the companion matrix its own docstring advertises. Since the trace and the norm of x are the trace and the determinant of that matrix, and both are basis independent, Tr_{E/F} x = t and N_{E/F} x = d.

These are what pin the elliptic normal form of GL₂ in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/NormalForm.lean, where the quadratic is the characteristic polynomial of a matrix and x is the eigenvalue it acquires in E.

Read in the other direction, every x : E satisfies the quadratic built from its own trace and norm, x² = Tr_{E/F}(x) · x - N_{E/F}(x), with no hypothesis on x: what the x ∉ F hypothesis buys the two theorems above is not the equation but the uniqueness of its coefficients. This is what separates the elliptic conjugacy classes of GL₂(F) from the split ones, an eigenvalue in E outside F being exactly what a split class does not have.

Over a finite base field such an x always exists as soon as the quadratic has no root in F: the quadratic is then irreducible, so AdjoinRoot of it is a degree-2 extension of F, and any two extensions of a finite field of the same degree are isomorphic (FiniteField.algEquivExtension), so every degree-2 extension already contains a root.

Main results

• TauCeti.Algebra.trace_eq_of_mul_self_eq and TauCeti.Algebra.norm_eq_of_mul_self_eq: the trace and the norm of an element x of a degree-2 extension satisfying x² = t x - d, and lying outside the base field, are t and d.
• TauCeti.exists_mul_self_eq_of_finite: over a finite field, a quadratic with no root in F has a root in every degree-2 extension.

References

• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 1.

The basis (1, x)

The trace and the norm

theorem TauCeti.Algebra.trace_eq_of_mul_self_eq {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] {x : E} (hx : x ∉ Set.range ⇑(algebraMap F E)) {t d : F} (hx2 : x * x = (algebraMap F E) t * x - (algebraMap F E) d) : (Algebra.trace F E) x = t

The trace of a quadratic irrationality. If E/F has degree 2 and x : E lies outside F and satisfies x² = t x - d, then Tr_{E/F} x = t.

theorem TauCeti.Algebra.norm_eq_of_mul_self_eq {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] {x : E} (hx : x ∉ Set.range ⇑(algebraMap F E)) {t d : F} (hx2 : x * x = (algebraMap F E) t * x - (algebraMap F E) d) : (Algebra.norm F) x = d

The norm of a quadratic irrationality. If E/F has degree 2 and x : E lies outside F and satisfies x² = t x - d, then N_{E/F} x = d.

A root of the quadratic in the extension

theorem TauCeti.exists_mul_self_eq_of_finite {F : Type u_1} [Field F] [Finite F] (E : Type u_2) [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] {t d : F} (hroot : ∀ (a : F), a * a ≠ t * a - d) : ∃ (x : E), x * x = (algebraMap F E) t * x - (algebraMap F E) d

Over a finite field a quadratic without a root has a root in every degree-2 extension. A quadratic with no root in F is irreducible, so AdjoinRoot of it is a degree-2 extension of F; over a finite field any two extensions of the same degree are isomorphic, so the supplied E already contains a root.