The minimal polynomial of a primitive element of a Galois extension

Let L/K be a finite Galois extension and let x generate L over K. The Galois group acts freely on x, so the conjugates σ x for σ ∈ Gal(L/K) are exactly the roots of minpoly K x, each once, and

(minpoly K x).map (algebraMap K L) = ∏ σ : Gal(L/K), (X - C (σ x)).

Differentiating and evaluating at x kills every summand with a factor X - C x and leaves

(minpoly K x)' (x) = ∏_{σ ≠ 1} (x - σ x).

This is the form in which the derivative of the minimal polynomial enters the theory of the different: for a Galois extension of local fields it expresses the different exponent as a sum of valuations v (σ x - x) over the nontrivial automorphisms.

Main results

• TauCeti.minpoly_map_eq_prod_X_sub_C_of_adjoin_eq_top: the minimal polynomial of a primitive element is, in L[X], the product of X - C (σ x) over the Galois group.
• TauCeti.aeval_derivative_minpoly_eq_prod_of_adjoin_eq_top: its derivative at x is the product of x - σ x over the nontrivial automorphisms.

References

• J.-P. Serre, Corps Locaux, Chapter III, §6 and Chapter IV, §1.

theorem TauCeti.minpoly_map_eq_prod_X_sub_C_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {x : L} (hx : K⟮x⟯ = ⊤) : Polynomial.map (algebraMap K L) (minpoly K x) = ∏ σ : Gal(L/K), (Polynomial.X - Polynomial.C (σ x))

The image in L[X] of the minimal polynomial of a primitive element x of a finite Galois extension L/K is ∏ σ : Gal(L/K), (X - C (σ x)).

theorem TauCeti.aeval_derivative_minpoly_eq_prod_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [DecidableEq Gal(L/K)] {x : L} (hx : K⟮x⟯ = ⊤) : (Polynomial.aeval x) (Polynomial.derivative (minpoly K x)) = ∏ σ ∈ Finset.univ.erase 1, (x - σ x)

The derivative of the minimal polynomial of a primitive element x of a finite Galois extension, evaluated at x, is ∏_{σ ≠ 1} (x - σ x).