Trace and norm in quadratic algebras and separable quadratic extensions

For a separable quadratic extension L/K the trace and norm are the two elementary symmetric functions of the pair {x, σx}, where σ is the nontrivial automorphism: tr x = x + σx and N x = x · σx (algebraMap_trace_eq_add, algebraMap_norm_eq_mul). These give the discriminant characterisation of the generators:

• discrim_eq_zero_iff_mem_range_algebraMap: the discriminant t² - 4n of X² - tX + n, the characteristic polynomial of multiplication by θ, vanishes exactly when θ ∈ K. (That polynomial is the minimal polynomial of θ precisely when θ ∉ K, which is what the statement says.) Forwards the discriminant equals (θ - σθ)², so it vanishes only where σ fixes θ; discrim_ne_zero is the contrapositive, kept separately because it is the direction consumers use;
• exists_discrim_ne_zero turns that into a choice principle: some θ has nonzero discriminant, hence generates. This is what a construction over L/K picks its generator by.

Three results hold for a commutative quadratic algebra over any nontrivial commutative base ring K, including bases with zero divisors. Algebra.IsQuadraticExtension K L supplies freeness and rank two; module-finiteness follows from the positive rank. No Euclidean division, domain, or separability hypothesis is needed. This covers quadratic orders over ℤ, the split algebra K × K, and the non-reduced K[X]/(X²):

• trace_algebraMap_add_algebraMap_mul and norm_algebraMap_add_algebraMap_mul evaluate the trace and norm of b + aθ — the first by K-linearity of the trace, the second from the 2 × 2 identity det (b • 1 + a • M) = b² + ab · tr M + a² · det M. This is how a statement about one generator transfers to another;
• discrim_eq_zero_of_mem_range_algebraMap, the easy half of the characterisation: a scalar θ = c has t = 2c and n = c², so t² - 4n = 0.

Separability is genuinely needed for the other half, and hence for discrim_ne_zero and exists_discrim_ne_zero: over a purely inseparable quadratic extension the trace form vanishes, so t = 0 and t² - 4n = 0 for every θ. In characteristic two discrim_ne_zero says t ≠ 0, reflecting that a separable quadratic extension is then Artin–Schreier rather than Kummer.

These formulas support quadratic twists and computations of norms in quadratic number fields. The nonzero-discriminant criterion selects a generator for a separable quadratic extension and ensures that twisting by that generator preserves ellipticity.

Over a base field, a square root x of d ∈ K with x ∉ K has characteristic polynomial X² - d, in every commutative quadratic algebra:

• trace_eq_zero_of_sq_eq and norm_eq_neg_of_sq_eq: Tr x = 0 and N x = -d;
• trace_algebraMap_add_algebraMap_mul_of_sq_eq and norm_algebraMap_add_algebraMap_mul_of_sq_eq: in square-root coordinates Tr (b + a x) = 2b and N (b + a x) = b² - a² d.

In a quadratic field extension trace_inv gives Tr (a⁻¹) = Tr a / N a, with no separability hypothesis. These are the inputs to the diagonalization of the twisted trace forms y ↦ Tr (a y²) of a quadratic extension.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/RingTheory/Norm/Quadratic.lean at revision bc2fe8ff7396, FLT PR #1088, Apache 2.0). That file's own header reads Authors: Kevin Buzzard, Claude; following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header. The square-root lemmas and trace_inv are not part of the adapted material.

@[simp]

theorem Algebra.IsQuadraticExtension.trace_algebraMap_add_algebraMap_mul (K : Type u_1) (L : Type u_2) [CommRing K] [Nontrivial K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] (a b : K) (θ : L) : (trace K L) ((algebraMap K L) b + (algebraMap K L) a * θ) = a * (trace K L) θ + 2 * b

The trace of b + aθ in a commutative quadratic algebra over a nontrivial commutative ring is a·tr(θ) + 2b. Neither separability nor invertibility in L is needed.

@[simp]

theorem Algebra.IsQuadraticExtension.norm_algebraMap_add_algebraMap_mul (K : Type u_1) (L : Type u_2) [CommRing K] [Nontrivial K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] (a b : K) (θ : L) : (norm K) ((algebraMap K L) b + (algebraMap K L) a * θ) = b ^ 2 + a * b * (trace K L) θ + a ^ 2 * (norm K) θ

The norm of b + aθ in a commutative quadratic algebra over a nontrivial commutative ring is b² + ab·tr(θ) + a²·N(θ). Neither separability nor invertibility in L is needed.

theorem Algebra.IsQuadraticExtension.discrim_eq_zero_of_mem_range_algebraMap (K : Type u_1) (L : Type u_2) [CommRing K] [Nontrivial K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] {θ : L} (hθ : θ ∈ Set.range ⇑(algebraMap K L)) : (trace K L) θ ^ 2 - 4 * (norm K) θ = 0

The discriminant vanishes on the image of the base ring in a commutative quadratic algebra: a scalar c has trace 2c and norm c². This includes split and non-reduced algebras. For a separable quadratic field extension, the converse is discrim_eq_zero_iff_mem_range_algebraMap.

theorem Algebra.IsQuadraticExtension.trace_eq_zero_of_sq_eq {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] {x : L} {d : K} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) : (trace K L) x = 0

A square root x of an element of the base field, lying outside the base field, has trace zero. This holds in every commutative quadratic algebra over a field, including split and nonreduced ones; for field extensions of any finite degree it is TauCeti.Algebra.trace_eq_zero_of_sq_algebraMap_of_not_mem_range.

theorem Algebra.IsQuadraticExtension.norm_eq_neg_of_sq_eq {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] {x : L} {d : K} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) : (norm K) x = -d

A square root x of d, lying outside the base field, has norm -d: its characteristic polynomial X² - Tr x · X + N x is X² - d.

theorem Algebra.IsQuadraticExtension.trace_algebraMap_add_algebraMap_mul_of_sq_eq {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] {x : L} {d : K} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) (a b : K) : (trace K L) ((algebraMap K L) b + (algebraMap K L) a * x) = 2 * b

The trace in square-root coordinates: if x² = d with x ∉ K, then Tr (b + a x) = 2 b.

theorem Algebra.IsQuadraticExtension.norm_algebraMap_add_algebraMap_mul_of_sq_eq {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] [IsQuadraticExtension K L] {x : L} {d : K} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) (a b : K) : (norm K) ((algebraMap K L) b + (algebraMap K L) a * x) = b ^ 2 - a ^ 2 * d

The norm in square-root coordinates: if x² = d with x ∉ K, then N (b + a x) = b² - a² d.

theorem Algebra.IsQuadraticExtension.trace_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] (a : L) : (trace K L) a⁻¹ = (trace K L) a / (norm K) a

In a quadratic field extension, Tr (a⁻¹) = Tr a / N a. Both sides vanish at a = 0, so no hypothesis is needed. This computes the values of twisted trace forms y ↦ Tr (a y²) at elements such as a⁻¹ or x / a, as in Kahn's diagonalization of Tr_*⟨a⟩.

theorem Algebra.IsQuadraticExtension.algebraMap_trace_eq_add (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] {σ : Gal(L/K)} (hσ : σ ≠ 1) (x : L) : (algebraMap K L) ((trace K L) x) = x + σ x

In a separable quadratic extension, the trace of x is x + σx, where σ is the nontrivial automorphism.

theorem Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] {σ : Gal(L/K)} (hσ : σ ≠ 1) (x : L) : (algebraMap K L) ((norm K) x) = x * σ x

In a separable quadratic extension, the norm of x is x * σx, where σ is the nontrivial automorphism.

@[simp]

theorem Algebra.IsQuadraticExtension.discrim_eq_zero_iff_mem_range_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} : (trace K L) θ ^ 2 - 4 * (norm K) θ = 0 ↔ θ ∈ Set.range ⇑(algebraMap K L)

Nonzero discriminant characterises the generators of a separable quadratic extension: for t, n the trace and norm of θ, so that θ² = tθ - n, the discriminant t² - 4n of the characteristic polynomial X² - tX + n of multiplication by θ vanishes exactly when θ lies in K. (Equivalently, that polynomial is the minimal polynomial of θ exactly when θ does not lie in K.) Forwards, over the nontrivial automorphism σ the discriminant equals (θ - σθ)², so it vanishes only if σ fixes θ; backwards is discrim_eq_zero_of_mem_range_algebraMap, which needs neither separability nor a field. This is the form a construction wants: it chooses θ by nonzero discriminant and needs to know that θ generates.

theorem Algebra.IsQuadraticExtension.discrim_ne_zero (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) : (trace K L) θ ^ 2 - 4 * (norm K) θ ≠ 0

A generator of a separable quadratic extension — an element outside K — has nonzero discriminant. The contrapositive half of discrim_eq_zero_iff_mem_range_algebraMap, kept as a named lemma because that is the direction every consumer uses.

theorem Algebra.IsQuadraticExtension.exists_discrim_ne_zero (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] : ∃ (θ : L), (trace K L) θ ^ 2 - 4 * (norm K) θ ≠ 0

A separable quadratic extension has an element of nonzero discriminant t² - 4n. Such an element is automatically a generator, by discrim_eq_zero_of_mem_range_algebraMap. Stating it as an existence result is what lets a construction over L/K choose one.