Square roots and the binomial X ^ n - C a

Mathlib's Kummer theory of X ^ n - C a (in Mathlib/FieldTheory/KummerExtension.lean) runs through a primitive n-th root of unity, which is unavailable for n = 2 in characteristic 2. This file records the elementary facts that need no root of unity: membership in the root set of X ^ n - C a is the equation x ^ n = a, and for n = 2 a single square root δ of a already splits the binomial and generates its splitting field, because the only other root is -δ.

Main results

• Polynomial.mem_rootSet_X_pow_sub_C: a point of an extension is a root of X ^ n - C a exactly when its n-th power is a.
• IntermediateField.adjoin_rootSet_X_pow_two_sub_C: a square root of a generates the root-set adjunction of X ^ 2 - C a.
• Polynomial.splits_map_X_pow_two_sub_C: a square root of a in an extension splits X ^ 2 - C a there.
• Valuation.X_pow_sub_C_irreducible_of_gcd_ord_eq_one: X ^ n - C a is irreducible when n is coprime to the order of a at a discrete valuation.
• Valuation.finrank_eq_of_pow_eq_of_gcd_ord_eq_one: a radical extension generated by a root of X ^ n - C a has degree n under the same coprimality condition.
• TauCeti.X_pow_sub_C_irreducible_of_irreducible: for a uniformizer ϖ of a discrete valuation ring, X ^ n - C ϖ is irreducible over the fraction field for every n ≠ 0.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.7.3.

@[simp]

theorem Polynomial.mem_rootSet_X_pow_sub_C {F : Type u} [CommRing F] {E : Type v} [Field E] [Algebra F E] {a : F} {n : ℕ} (hn : n ≠ 0) {x : E} : x ∈ (X ^ n - C a).rootSet E ↔ x ^ n = (algebraMap F E) a

A point of an extension is a root of X ^ n - C a exactly when its n-th power is a.

theorem IntermediateField.adjoin_rootSet_X_pow_two_sub_C {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {a : F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) a) : adjoin F ((Polynomial.X ^ 2 - Polynomial.C a).rootSet E) = F⟮δ⟯

Over a field, a square root δ of a generates the whole splitting field of X ^ 2 - C a, because the only other root is -δ.

theorem Polynomial.splits_map_X_pow_two_sub_C {F : Type u} [CommRing F] {E : Type v} [CommRing E] [Algebra F E] {a : F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) a) : (map (algebraMap F E) (X ^ 2 - C a)).Splits

A square root of a in E splits X ^ 2 - C a there: the two linear factors are X - C δ and X + C δ. Unlike Polynomial.X_pow_sub_C_splits_of_isPrimitiveRoot this needs no primitive root of unity, so it also covers characteristic 2, where the two factors coincide.

theorem Valuation.X_pow_sub_C_irreducible_of_gcd_ord_eq_one {F : Type u} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {n : ℕ} (hn : n ≠ 0) {a : F} (h : (↑n).gcd (v.ord a) = 1) : Irreducible (Polynomial.X ^ n - Polynomial.C a)

A valuative irreducibility criterion for X ^ n - C a: if n ≠ 0 is coprime to the order of a at a discrete valuation v, then X ^ n - C a is irreducible. No root of unity and no hypothesis on the characteristic is needed. For a = 0 the order is the junk value 0, so the hypothesis forces n = 1, where the statement holds trivially. See Andrew Yang's X_pow_sub_C_irreducible_of_prime in Mathlib/FieldTheory/KummerPolynomial.lean.

theorem Valuation.finrank_eq_of_pow_eq_of_gcd_ord_eq_one {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] (w : Valuation F (WithZero (Multiplicative ℤ))) {y : E} {n : ℕ} {a : F} (htop : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F E) a) (hn : n ≠ 0) (h : (↑n).gcd (w.ord a) = 1) : Module.finrank F E = n

The degree of a radical extension: if y generates E over F with y ^ n = a, and n is coprime to the order of a at a discrete valuation, then [E : F] = n. This is the degree criterion used in Stichtenoth, Proposition 3.7.3.

theorem TauCeti.X_pow_sub_C_irreducible_of_irreducible {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} (hϖ : Irreducible ϖ) {n : ℕ} (hn : n ≠ 0) : Irreducible (Polynomial.X ^ n - Polynomial.C ((algebraMap R K) ϖ))

A uniformizer has no nontrivial root in the fraction field: for a uniformizer ϖ of a discrete valuation ring R and n ≠ 0, the polynomial X ^ n - C ϖ is irreducible over the fraction field of R, as ϖ has order 1 at the valuation of the maximal ideal.