Eisenstein generators of the counted extensions

The totally ramified degree-n subextensions of a separable closure are precisely the fields obtained by adjoining a root of a monic Eisenstein polynomial of degree n. The root is taken in the separable closure, so inseparable Eisenstein polynomials contribute no extensions.

These characterizations connect coefficient-space root counts with the family totallyRamifiedOfDegree. They also show that the family is preserved under embeddings into the separable closure, as needed when regrouping extensions by isomorphism class.

The proofs transport the local-field Eisenstein-generator theorems through the canonical finite-intermediate-field structures; no valuation or topology on the separable closure is needed. The bridge is exists_isRoot_adjoin_eq_top_of_eisenstein: for those structures, the generator of the subextension generated by a root of an Eisenstein polynomial is an integral root of it. Through it, natCast_discriminantExponent_adjoin_eq_iInf_of_eisenstein computes the discriminant exponent of such a subextension from the Eisenstein formula for the different exponent. A special case of the generator theorem is adjoin_mem_totallyRamifiedOfDegree_of_pow_eq: for a uniformizer ϖ and 0 < n, a root of X ^ n - ϖ generates a member of σ_K(n). In degree two, a root of an Eisenstein polynomial X ^ 2 + b X + c generates a member of σ_K(2) whose discriminant exponent is min (2 v_K(b)) (2 v_K(2) + 1) (natCast_discriminantExponent_adjoin_eq_min_of_sq_add_mul_add_eq_zero). For a uniformizer ϖ, K(√ϖ) therefore has discriminant exponent 2 v_K(2) + 1 (natCast_discriminantExponent_adjoin_of_sq_eq_of_irreducible), and in residue characteristic 2, K(√(1 - ϖ)) is a member of σ_K(2) (adjoin_mem_totallyRamifiedOfDegree_two_of_sq_eq_one_sub) of discriminant exponent 2 v_K(2) (natCast_discriminantExponent_adjoin_of_sq_eq_one_sub_of_irreducible).

References

• J.-P. Serre, Local Fields, Chapter I, §6, Proposition 17.
• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 13.
• J.-P. Serre, Une « formule de masse » pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris Sér. A 286 (1978), 1031–1036, §2.

theorem TauCeti.exists_eisenstein_generator_of_mem_totallyRamifiedOfDegree {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ totallyRamifiedOfDegree K n) : ∃ (f : Polynomial ↥(ValuativeRel.valuation K).integer) (x : SeparableClosure K), f.Monic ∧ f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ∧ f.natDegree = n ∧ (Polynomial.aeval x) (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f) = 0 ∧ K⟮x⟯ = L

Every counted extension has a monic Eisenstein generator of the prescribed degree, viewed as an element of the ambient separable closure.

theorem TauCeti.exists_isRoot_adjoin_eq_top_of_eisenstein {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) {x : SeparableClosure K} (hx : (Polynomial.aeval x) (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f) = 0) [Module.Finite K ↥K⟮x⟯] : ∃ (π : ↥(ValuativeRel.valuation ↥K⟮x⟯).integer), (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation ↥K⟮x⟯).integer) f).IsRoot π ∧ K⟮↑π⟯ = ⊤

Let x be a root in the separable closure of an Eisenstein polynomial f. With the canonical local-field structure on K⟮x⟯, the generator of K⟮x⟯ lies in its integer ring: it is an integral root π of f that generates K⟮x⟯ over K. Monicity is not required.

theorem TauCeti.natCast_discriminantExponent_adjoin_eq_iInf_of_eisenstein {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) {x : SeparableClosure K} (hx : (Polynomial.aeval x) (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f) = 0) : ↑K⟮x⟯.discriminantExponent = ⨅ (i : Fin f.natDegree), f.natDegree • (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) (f.coeff (↑i + 1) * (↑↑i + 1)) + ↑↑i

For a root x in the separable closure of an Eisenstein polynomial f over 𝒪[K], the discriminant exponent of K⟮x⟯ is the least valuation of the terms of the derivative of f in the power basis of x: the i-th term has valuation deg f • v_K (f.coeff (i + 1) * (i + 1)) + i.

theorem TauCeti.adjoin_mem_totallyRamifiedOfDegree_of_eisenstein {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) (hdeg : f.natDegree = n) {x : SeparableClosure K} (hx : (Polynomial.aeval x) (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f) = 0) : K⟮x⟯ ∈ totallyRamifiedOfDegree K n

A root in the separable closure of an Eisenstein polynomial generates a counted extension, whose degree is the degree of the polynomial. Monicity is not required.

theorem TauCeti.adjoin_mem_totallyRamifiedOfDegree_of_pow_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) {n : ℕ} (hn : 0 < n) {x : SeparableClosure K} (hx : x ^ n = (algebraMap K (SeparableClosure K)) ↑ϖ) : K⟮x⟯ ∈ totallyRamifiedOfDegree K n

Roots of X ^ n - ϖ generate counted extensions. For a uniformizer ϖ of K and 0 < n, a root in the separable closure of X ^ n - ϖ, which is Eisenstein, generates a member of σ_K(n).

theorem TauCeti.adjoin_mem_totallyRamifiedOfDegree_two_of_sq_add_mul_add_eq_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {b c : ↥(ValuativeRel.valuation K).integer} (hb : b ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) (hc : Irreducible c) {x : SeparableClosure K} (hx : x ^ 2 + (algebraMap K (SeparableClosure K)) ↑b * x + (algebraMap K (SeparableClosure K)) ↑c = 0) : K⟮x⟯ ∈ totallyRamifiedOfDegree K 2

Roots of Eisenstein quadratics generate counted extensions. If b ∈ 𝓂[K] and c is a uniformizer of K, a root in the separable closure of X ^ 2 + b X + c generates a member of σ_K(2).

theorem TauCeti.natCast_discriminantExponent_adjoin_eq_min_of_sq_add_mul_add_eq_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {b c : ↥(ValuativeRel.valuation K).integer} (hb : b ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) (hc : Irreducible c) {x : SeparableClosure K} (hx : x ^ 2 + (algebraMap K (SeparableClosure K)) ↑b * x + (algebraMap K (SeparableClosure K)) ↑c = 0) : ↑K⟮x⟯.discriminantExponent = min (2 * (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) b) (2 * (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) 2 + 1)

The discriminant exponent of a root of an Eisenstein quadratic. If b ∈ 𝓂[K] and c is a uniformizer of K, a root x in the separable closure of X ^ 2 + b X + c generates an extension of discriminant exponent min (2 v_K(b)) (2 v_K(2) + 1).

theorem TauCeti.natCast_discriminantExponent_adjoin_of_sq_eq_of_irreducible {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) {x : SeparableClosure K} (hx : x ^ 2 = (algebraMap K (SeparableClosure K)) ↑ϖ) : ↑K⟮x⟯.discriminantExponent = 2 * (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) 2 + 1

The discriminant exponent of K(√ϖ). For a uniformizer ϖ of K, a square root of ϖ in the separable closure generates an extension of discriminant exponent 2 v_K(2) + 1.

theorem TauCeti.adjoin_mem_totallyRamifiedOfDegree_two_of_sq_eq_one_sub {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ϖ : ↥(ValuativeRel.valuation K).integer} (h2 : 2 ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) (hϖ : Irreducible ϖ) {x : SeparableClosure K} (hx : x ^ 2 = 1 - (algebraMap K (SeparableClosure K)) ↑ϖ) : K⟮x⟯ ∈ totallyRamifiedOfDegree K 2

K(√(1 - ϖ)) is totally ramified for a uniformizer ϖ of a local field K of residue characteristic 2: it is generated by √(1 - ϖ) + 1, a root of the Eisenstein polynomial X ^ 2 - 2 X + ϖ.

theorem TauCeti.natCast_discriminantExponent_adjoin_of_sq_eq_one_sub_of_irreducible {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ϖ : ↥(ValuativeRel.valuation K).integer} (h2 : 2 ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) (hϖ : Irreducible ϖ) {x : SeparableClosure K} (hx : x ^ 2 = 1 - (algebraMap K (SeparableClosure K)) ↑ϖ) : ↑K⟮x⟯.discriminantExponent = 2 * (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) 2

The discriminant exponent of K(√(1 - ϖ)). For a uniformizer ϖ of a local field K of residue characteristic 2, a square root of 1 - ϖ in the separable closure generates an extension of discriminant exponent 2 v_K(2).

theorem TauCeti.mem_totallyRamifiedOfDegree_iff_exists_eisenstein_generator {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} : L ∈ totallyRamifiedOfDegree K n ↔ ∃ (f : Polynomial ↥(ValuativeRel.valuation K).integer) (x : SeparableClosure K), f.Monic ∧ f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ∧ f.natDegree = n ∧ (Polynomial.aeval x) (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f) = 0 ∧ K⟮x⟯ = L

Membership in the counted family is equivalent to being generated by a root of a monic Eisenstein polynomial of the prescribed degree.

theorem AlgHom.fieldRange_mem_totallyRamifiedOfDegree {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (φ : ↥L →ₐ[K] SeparableClosure K) (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) : φ.fieldRange ∈ TauCeti.totallyRamifiedOfDegree K n

The image of any embedding of a counted extension into the separable closure is again a counted extension of the same degree.