The different of an Eisenstein extension

For an extension generated by a root of an Eisenstein polynomial, the different exponent is the least valuation of the terms of the polynomial derivative. The powers of the root have distinct valuation residues, so these terms cannot cancel.

Main results

• TauCeti.natCast_differentExponent_eq_iInf_of_eisenstein_adjoin_eq_top gives the exact derivative-term formula for the different exponent.
• The upper-bound theorem differentExponent_le_ramificationIndex_sub_one_add_natCastValuation_of_eisenstein_adjoin_eq_top proves d(L/K) ≤ e - 1 + v_L(e), where e = e(L/K) and v_L is the normalized valuation, provided (e : L) ≠ 0.

References

• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 13.

theorem TauCeti.natCast_differentExponent_eq_iInf_of_eisenstein_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] (f : Polynomial ↥(ValuativeRel.valuation K).integer) (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) (ξ : ↥(ValuativeRel.valuation L).integer) (hroot : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot ξ) (hgen : K⟮↑ξ⟯ = ⊤) : ↑(differentExponent K L) = ⨅ (i : Fin f.natDegree), ramificationIndex K L • (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) (f.coeff (↑i + 1) * (↑↑i + 1)) + ↑↑i

For a generator of L/K that is a root of an Eisenstein polynomial, the different exponent is the least valuation of the terms of its polynomial derivative.

theorem TauCeti.differentExponent_le_ramificationIndex_sub_one_add_natCastValuation_of_eisenstein_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] (f : Polynomial ↥(ValuativeRel.valuation K).integer) (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) (ξ : ↥(ValuativeRel.valuation L).integer) (hroot : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot ξ) (hgen : K⟮↑ξ⟯ = ⊤) (he0 : ↑(ramificationIndex K L) ≠ 0) : differentExponent K L ≤ ramificationIndex K L - 1 + natCastValuation L (ramificationIndex K L) he0

For an extension generated by a root of an Eisenstein polynomial, the different exponent is at most e - 1 + v_L(e), provided e is nonzero in the extension field.