Generators of a quadratic extension

Mathlib's Algebra.IsQuadraticExtension K L records that L/K has degree two but says nothing about the elements realising that degree. This file first supplies a non-scalar element, then shows how to choose and change a generator when the base is a field:

Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap: an element outside the image of the base exists. Over a field base, the coordinate theorem below makes any such element a generator. Algebra.IsQuadraticExtension.exists_eq_algebraMap_add_algebraMap_mul: every element is b + aθ for a fixed generator θ, the coordinate presentation over the basis 1, θ (used by the quadratic field-norm computation). Algebra.IsQuadraticExtension.exists_ne_zero_eq_algebraMap_add_algebraMap_mul: for a second generator the θ-coefficient is nonzero, so any two generators differ by θ' = b + aθ with a ≠ 0 and a statement proved for one transfers to every other. TauCeti.linearIndependent_one_of_notMem_range_algebraMap is the linear-algebra step behind them. TauCeti.quadraticExtensionBasis makes (1, x) a basis for any non-scalar x in a degree-two algebra over a field, with evaluation lemmas for its two basis vectors.

None asks for a field on L: each theorem needs only a semiring, with the ring structure required by linear independence obtained locally through Algebra.semiringToRing. Non-scalar existence is stated over the commutative semirings admitted by Mathlib's IsQuadraticExtension; the strong rank condition also forces the base to be nontrivial. The coordinate results require a field base: over ℤ, the element (0, 2) lies outside the diagonal copy of ℤ in ℤ × ℤ but does not span the algebra together with 1. Over a field, the results cover split and non-reduced quadratic algebras such as K × K and K[X]/(X²).

These are used by the extension quadratic twist in TauCeti/AlgebraicGeometry/EllipticCurve/QuadraticTwist/Basic.lean and by the quadratic field-norm computation in TauCeti/NumberTheory/NumberField/Quadratic/Norm.lean. The shared basis also supplies explicit coordinates for quadratic-extension trace transfer.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/LinearAlgebra/Dimension/IsQuadraticExtension.lean at commit 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. Only the results the twist consumes are ported; the rest of the source file — which restates Algebra.IsQuadraticExtension itself, already in Mathlib — is not needed.

theorem Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap (K : Type u_1) (L : Type u_2) [CommSemiring K] [StrongRankCondition K] [Semiring L] [Algebra K L] [IsQuadraticExtension K L] : ∃ (θ : L), θ ∉ Set.range ⇑(algebraMap K L)

A quadratic algebra contains an element outside the image of the base ring. Were every element in the image of algebraMap, the algebra would have rank one, contradicting finrank = 2. The base K needs to be a commutative semiring with the strong rank condition, and L a semiring. The strong rank condition forces K to be nontrivial; the quadratic-extension hypothesis makes L free of rank 2, and the faithful scalar action makes algebraMap injective.

theorem TauCeti.linearIndependent_one_of_notMem_range_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Semiring L] [Algebra K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) : LinearIndependent K ![1, θ]

1 and any element lying outside the base field are linearly independent over the base field. The ambient algebra needs only a semiring structure: its field-algebra structure supplies a ring structure, and the hypothesis on θ implies that the algebra is nontrivial.

noncomputable def TauCeti.quadraticExtensionBasis (K : Type u_1) (L : Type u_2) [Field K] [Semiring L] [Algebra K L] {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hfin : Module.finrank K L = 2) : Module.Basis (Fin 2) K L

The basis (1, x) of a degree-two algebra over a field for an element outside the base.

Equations

• TauCeti.quadraticExtensionBasis K L hx hfin = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[simp]

theorem TauCeti.quadraticExtensionBasis_zero (K : Type u_1) (L : Type u_2) [Field K] [Semiring L] [Algebra K L] {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hfin : Module.finrank K L = 2) : (quadraticExtensionBasis K L hx hfin) 0 = 1

@[simp]

theorem TauCeti.quadraticExtensionBasis_one (K : Type u_1) (L : Type u_2) [Field K] [Semiring L] [Algebra K L] {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hfin : Module.finrank K L = 2) : (quadraticExtensionBasis K L hx hfin) 1 = x

theorem Algebra.IsQuadraticExtension.exists_eq_algebraMap_add_algebraMap_mul (K : Type u_1) (L : Type u_2) [Field K] [Semiring L] [Algebra K L] [IsQuadraticExtension K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) (x : L) : ∃ (a : K) (b : K), x = (algebraMap K L) b + (algebraMap K L) a * θ

Every element of a quadratic extension is b + aθ for a fixed generator θ: the basis 1, θ spans L over K. The θ-coefficient may vanish, exactly when the element lies in the base field; exists_ne_zero_eq_algebraMap_add_algebraMap_mul records that it does not for a second generator. The spanning is K-linear algebra, so this needs only a semiring on L.

theorem Algebra.IsQuadraticExtension.exists_ne_zero_eq_algebraMap_add_algebraMap_mul (K : Type u_1) (L : Type u_2) [Field K] [Semiring L] [Algebra K L] [IsQuadraticExtension K L] {θ θ' : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) (hθ' : θ' ∉ Set.range ⇑(algebraMap K L)) : ∃ (a : K) (b : K), a ≠ 0 ∧ θ' = (algebraMap K L) b + (algebraMap K L) a * θ

Any element of a quadratic extension L/K is a K-linear combination of 1 and a given generator θ, and the θ-coefficient is nonzero if the element also lies outside K. So any two generators differ by θ' = b + aθ with a ≠ 0.