Trace lemmas for field extensions

This file collects reusable trace facts for finite field extensions.

Main results

• NumberField.trace_eq_zero_of_sq_ratCast: the number-field specialization saying that x² ∈ ℚ, x ∉ ℚ implies Tr x = 0.
• TauCeti.Algebra.trace_eq_zero_of_sq_algebraMap_of_not_mem_range: the corresponding trace-vanishing statement for any finite field extension.
• TauCeti.Algebra.discr_one_elem_eq_of_sq_algebraMap: in a quadratic extension, the trace-form discriminant of the square-root basis {1, x} is 4a when x² = a and x ∉ F.

Provenance

Migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where these trace facts supported square-root basis computations over number fields.

theorem TauCeti.Algebra.trace_eq_zero_of_sq_algebraMap_of_not_mem_range {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] [FiniteDimensional F L] {x : L} {r : F} (hx2 : x ^ 2 = (algebraMap F L) r) (hx : x ∉ (algebraMap F L).range) : (Algebra.trace F L) x = 0

In a finite field extension, an element outside the base field whose square lies in the base field has trace zero.

theorem TauCeti.Algebra.discr_one_elem_eq_of_sq_algebraMap {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] [FiniteDimensional F L] {x : L} {a : F} (hfin : Module.finrank F L = 2) (hx2 : x ^ 2 = (algebraMap F L) a) (hx : x ∉ (algebraMap F L).range) : Algebra.discr F ![1, x] = 4 * a

For a quadratic extension L / F and an element x ∉ F whose square is a ∈ F, the trace-form discriminant of the square-root basis {1, x} equals 4 a.

theorem NumberField.trace_eq_zero_of_sq_ratCast {K : Type u_1} [Field K] [NumberField K] {x : K} {r : ℚ} (hx2 : x ^ 2 = (algebraMap ℚ K) r) (hx : x ∉ (algebraMap ℚ K).range) : (Algebra.trace ℚ K) x = 0

In a number field, an irrational element whose square is rational has trace zero.