The different exponent and derivatives of generating equations

Let F' / k' be an extension of the field extension F / k with F' / F finite and separable, let P' be a place of F' over the place P of F, and suppose F' = F(y). If y is a root of a monic polynomial ψ with coefficients in the valuation ring 𝒪_P, then

d(P' ∣ P) ≤ ord_{P'} (ψ'(y))

provided ψ'(y) ≠ 0 (Stichtenoth, Theorem 3.5.10(a), where ψ is the minimal polynomial of y). This is the tool that computes different exponents from an explicit equation: a place at which ψ'(y) is a unit is unramified, with d(P' ∣ P) = 0.

When an integral element generates the full local integral closure, the corresponding bound is an equality for the derivative of its minimal polynomial.

Main results

• TauCeti.Place.differentExponent_le_ord_aeval_derivative: d(P' ∣ P) ≤ ord_{P'} (ψ'(y)).
• TauCeti.Place.differentExponent_eq_ord_aeval_derivative_minpoly: equality for a generator of the integral closure.
• TauCeti.Place.differentExponent_eq_zero_of_valuation_aeval_derivative_eq_one: if ψ'(y) is a unit at P', then d(P' ∣ P) = 0.

References

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

theorem TauCeti.Place.differentExponent_le_ord_aeval_derivative (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} (hgen : F⟮y⟯ = ⊤) {ψ : Polynomial F} (hψ : ψ.Monic) (hcoeff : ∀ (i : ℕ), ψ.coeff i ∈ (restrict k F P').integers) (hy : (Polynomial.aeval y) ψ = 0) (hψ' : (Polynomial.aeval y) (Polynomial.derivative ψ) ≠ 0) : ↑(differentExponent k F P') ≤ P'.ord ((Polynomial.aeval y) (Polynomial.derivative ψ))

The different exponent is bounded by the derivative of a generating equation (Stichtenoth, Theorem 3.5.10(a)): if F' = F(y) and y is a root of a monic ψ ∈ F[X] whose coefficients are regular at the place P below P', then d(P' ∣ P) ≤ ord_{P'} (ψ'(y)), as long as ψ'(y) ≠ 0. Stichtenoth takes ψ to be the minimal polynomial of y; any monic multiple of it with coefficients in 𝒪_P works as well.

theorem TauCeti.Place.differentExponent_eq_ord_aeval_derivative_minpoly (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {x : ↥(integralClosure (↥(restrict k F P').integers) F')} (hx : (↥(restrict k F P').integers)[x] = ⊤) : ↑(differentExponent k F P') = P'.ord ((Polynomial.aeval ((algebraMap (↥(integralClosure (↥(restrict k F P').integers) F')) F') x)) (Polynomial.derivative (minpoly F ((algebraMap (↥(integralClosure (↥(restrict k F P').integers) F')) F') x))))

For a generator of the integral closure over the valuation ring, the different exponent is the order of the derivative of its field minimal polynomial.

theorem TauCeti.Place.differentExponent_eq_zero_of_valuation_aeval_derivative_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} (hgen : F⟮y⟯ = ⊤) {ψ : Polynomial F} (hψ : ψ.Monic) (hcoeff : ∀ (i : ℕ), ψ.coeff i ∈ (restrict k F P').integers) (hy : (Polynomial.aeval y) ψ = 0) (hψ' : P'.valuation ((Polynomial.aeval y) (Polynomial.derivative ψ)) = 1) : differentExponent k F P' = 0

A place at which the derivative of a generating equation is a unit is unramified (Stichtenoth, Theorem 3.5.10(a)): if F' = F(y), y is a root of a monic ψ ∈ F[X] whose coefficients are regular at the place P below P', and ψ'(y) is a unit at P', then d(P' ∣ P) = 0.