Quadratic normal forms in intermediate fields

This file contains normal-form lemmas for adjoining one element whose square already lies in an intermediate field, together with the corresponding quadratic finrank and degree-doubling API. Conversely, it shows by completing the square that, when 2 ≠ 0, every quadratic intermediate field is generated by an element whose square lies in the base field. For finite Galois extensions this also identifies each index-two subgroup as the stabilizer of a nonzero square root (exists_sq_mem_range_apply_eq_self_iff_of_index_eq_two). The finrank lemmas live here because they combine the normal form with intermediate-field scalar restriction for one quadratic tower step. The receiver-style finrank lemmas extend Mathlib's IntermediateField API and therefore live in that namespace; the remaining normal-form API stays in TauCeti.IntermediateField.

Provenance

exists_add_mul_of_mem_sup_adjoin_sq is 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 it was a step in the square-class descent for multiquadratic fields; here it is stated for an arbitrary field extension.

theorem TauCeti.IntermediateField.exists_add_mul_of_mem_sup_adjoin_sq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {x : L} (hx2 : x ^ 2 ∈ F) {y : L} (hy : y ∈ F ⊔ K⟮x⟯) : ∃ (a : L) (b : L), a ∈ F ∧ b ∈ F ∧ y = a + b * x

If x² ∈ F, every element of F ⊔ K⟮x⟯ has the form a + b * x with a, b ∈ F.

@[simp]

theorem TauCeti.IntermediateField.mem_sup_adjoin_sq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {x : L} (hx2 : x ^ 2 ∈ F) {y : L} : y ∈ F ⊔ K⟮x⟯ ↔ ∃ (a : L) (b : L), a ∈ F ∧ b ∈ F ∧ y = a + b * x

Membership in F ⊔ K⟮x⟯, for x² ∈ F, is equivalent to having the form a + b * x with a, b ∈ F.

theorem IntermediateField.finrank_adjoin_simple_eq_two_of_sq_mem_notMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) {x : L} (hx2 : x ^ 2 ∈ F) (hxF : x ∉ F) : Module.finrank ↥F ↥(↥F)⟮x⟯ = 2

If x² ∈ F but x ∉ F, then the simple extension F⟮x⟯ has finrank two over F.

theorem IntermediateField.finrank_sup_adjoin_simple_eq_mul_two {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) {x : L} (hx2 : x ^ 2 ∈ F) (hxF : x ∉ F) : Module.finrank K ↥(F ⊔ K⟮x⟯) = Module.finrank K ↥F * 2

If x² ∈ F but x ∉ F, then adjoining x doubles the degree: [F ⊔ K⟮x⟯ : K] = 2 · [F : K].

theorem TauCeti.IntermediateField.finrank_adjoin_simple_eq_two_of_not_isSquare {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {a : K} {x : L} (hx : x ^ 2 = (algebraMap K L) a) (ha : ¬IsSquare a) : Module.finrank K ↥K⟮x⟯ = 2

A square root of a nonsquare radicand generates a quadratic extension. If x ^ 2 = a for some a ∈ K that is not a square in K, then [K(x) : K] = 2: the square already lies in the base field, and nonsquareness of a is exactly what keeps x out of it.

No assumption on the characteristic of K is needed: when 2 = 0 the extension is purely inseparable, X ^ 2 - a being (X - x) ^ 2, but it is still quadratic.

theorem TauCeti.IntermediateField.isSquare_mul_of_adjoin_simple_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NeZero 2] {a c : K} {x y : L} (hx : x ^ 2 = (algebraMap K L) a) (hy : y ^ 2 = (algebraMap K L) c) (hxb : x ∉ ⊥) (hxy : K⟮x⟯ = K⟮y⟯) : IsSquare (a * c)

Same square class from a shared simple quadratic field. Let x and y be square roots of a and c in a field extension L / K with 2 ≠ 0. If x ∉ K and the simple extensions K(x) and K(y) coincide, then a · c is a square in K: two square roots generate the same quadratic subfield only when their radicands lie in the same square class.

theorem TauCeti.IntermediateField.exists_sq_mem_range_adjoin_simple_eq_of_finrank_eq_two {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NeZero 2] {E : IntermediateField K L} (hE : Module.finrank K ↥E = 2) : ∃ x ∈ E, x ∉ ⊥ ∧ (∃ (a : K), x ^ 2 = (algebraMap K L) a) ∧ K⟮x⟯ = E

A quadratic intermediate field is generated by a square root. If 2 ≠ 0 in K and the intermediate field E of L / K has degree 2 over K, then E = K⟮x⟯ for an x whose square lies in K and which does not itself lie in K.

Completing the square is what needs 2 invertible: a generator y of E satisfies a monic quadratic y² + b y + c = 0 over K, and x = 2y + b then has x² = b² - 4c ∈ K.

theorem TauCeti.IntermediateField.exists_sq_mem_range_apply_eq_self_iff_of_index_eq_two {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [NeZero 2] {H : Subgroup Gal(L/K)} (hH : H.index = 2) : ∃ (x : L) (a : K), x ≠ 0 ∧ x ^ 2 = (algebraMap K L) a ∧ ∀ (σ : Gal(L/K)), σ x = x ↔ σ ∈ H

An index-two subgroup of a finite Galois group is the stabilizer of a nonzero square root of an element of the base field, when the base field has characteristic different from two.