The different exponent of a monogenic local extension #
The different exponent is the additive valuation of the derivative of a generator's minimal polynomial when the integer ring of the extension is generated by that element.
Main result #
TauCeti.natCast_differentExponent_eq_addVal_aeval_derivative_minpolygives this valuation formula.
theorem
TauCeti.natCast_differentExponent_eq_addVal_aeval_derivative_minpoly
(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]
[Module.Finite K L]
{x : ↥(ValuativeRel.valuation L).integer}
(hx : (↥(ValuativeRel.valuation K).integer)[x] = ⊤)
:
↑(differentExponent K L) = (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer)
((Polynomial.aeval x) (Polynomial.derivative (minpoly (↥(ValuativeRel.valuation K).integer) x)))
For an integral generator x, the different exponent is the additive valuation of the
derivative of its minimal polynomial at x.