The Galois theory of separable quadratic extensions

Material complementing Mathlib/FieldTheory/Galois/Basic.lean for a separable quadratic extension L/K: it has exactly two automorphisms, so the identity and any one nontrivial automorphism exhaust Gal(L/K), and an element fixed by a nontrivial automorphism lies in the base field. Algebra.IsQuadraticExtension.quadraticCharacter records the resulting Gal(L/K) →* ℤˣ — the identity to 1, the nontrivial automorphism to -1. It is there so that a quantity alternating with the Galois action can be described uniformly in σ rather than by cases; WeierstrassCurve.quadraticTwistPointEquiv_map_eq_quadraticCharacter_smul_map is the intended consumer. Mathlib's quadraticChar is a different object — the Legendre symbol of a finite field, not a character of a Galois group.

Mathlib already supplies the surrounding structure: Algebra.IsQuadraticExtension makes L/K finite and normal (Algebra.IsQuadraticExtension.normal), hence Galois with separability (Algebra.IsQuadraticExtension.isGalois); IsGalois.card_aut_eq_finrank counts the automorphisms and IsGalois.mem_range_algebraMap_iff_fixed characterises the base field.

These are the descent inputs for quadratic twists, consumed by TauCeti/AlgebraicGeometry/EllipticCurve/GaloisDescent.lean and by TauCeti/RingTheory/Norm/Quadratic.lean, which expresses the trace and norm of a separable quadratic extension through its nontrivial automorphism.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/FieldTheory/Galois/Basic.lean at 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 consumed downstream are adapted here.

theorem Algebra.IsQuadraticExtension.card_algEquiv_eq_two (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] : Nat.card Gal(L/K) = 2

A separable quadratic extension has exactly two automorphisms.

theorem Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq (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) (φ : Gal(L/K)) : φ = 1 ∨ φ = σ

The only automorphisms of a separable quadratic extension are the identity and any given nontrivial automorphism.

@[simp]

theorem Algebra.IsQuadraticExtension.algEquiv_mul_self (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)) : σ * σ = 1

Every automorphism of a separable quadratic extension is an involution. Gal(L/K) has order two, so this needs no nontriviality hypothesis: it holds for the identity as well.

theorem Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq (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} (hx : σ x = x) : x ∈ Set.range ⇑(algebraMap K L)

An element fixed by a nontrivial automorphism — hence, Gal(L/K) having order two, by all of Gal(L/K) — lies in the base field.

theorem Algebra.IsQuadraticExtension.apply_sub_self_ne_zero (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} (hx : x ∉ Set.range ⇑(algebraMap K L)) : σ x - x ≠ 0

A nontrivial automorphism moves every element outside the base field. The difference σ x - x is the square root of the discriminant of x's minimal polynomial, so this is exactly the nondegeneracy that makes such an x a generator.

theorem Algebra.IsQuadraticExtension.exists_algEquiv_ne_one (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)), σ ≠ 1

A separable quadratic extension has a nontrivial automorphism.

theorem Algebra.IsQuadraticExtension.univ_eq_pair (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] [Algebra.IsSeparable K L] [DecidableEq Gal(L/K)] {σ : Gal(L/K)} (hσ : σ ≠ 1) : Finset.univ = {1, σ}

The automorphism group of a separable quadratic extension consists of the identity and one nontrivial element.

The quadratic character

noncomputable def Algebra.IsQuadraticExtension.quadraticCharacter (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) →* ℤˣ

The quadratic character of a separable quadratic extension: the identity goes to 1 and the nontrivial automorphism to -1. Gal(L/K) has order two, so this is a group isomorphism onto ℤˣ, but the point of packaging it as a MonoidHom is that a statement which alternates in σ — a Galois action twisted by the extension, as for the points of a quadratic twist — can then be written uniformly in σ instead of split into a fixed and a moved branch by every consumer.

Equations

• Algebra.IsQuadraticExtension.quadraticCharacter K L = { toFun := fun (σ : Gal(L/K)) => if σ = 1 then 1 else -1, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Algebra.IsQuadraticExtension.quadraticCharacter_eq_one_iff (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)} : (quadraticCharacter K L) σ = 1 ↔ σ = 1

The quadratic character detects the identity: it takes the value 1 exactly there.

theorem Algebra.IsQuadraticExtension.quadraticCharacter_eq_neg_one_of_ne_one (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) : (quadraticCharacter K L) σ = -1

Off the identity the quadratic character takes the value -1, there being nowhere else to go in ℤˣ.