Derivatives of annihilating polynomials lie in the different

Let B be the integral closure of an integrally closed domain A in an extension L/K of its fraction field, and let x ∈ B generate L over K; then L/K is finite, and no separability hypothesis is needed. Mathlib shows that f'(x) lies in the different ideal 𝔇_{B/A} when f is the minimal polynomial of x over A and L/K is separable (aeval_derivative_mem_differentIdeal); if L/K is inseparable then f' vanishes. Any polynomial p ∈ A[X] with p(x) = 0 is a multiple f g of the minimal polynomial, A being integrally closed, so p'(x) = f'(x) g(x) lies in the different as well. This is the form in which an explicit equation for x bounds ramification: a prime of B not containing p'(x) does not divide the different, and when A is a Dedekind domain such a prime is unramified over A (dvd_differentIdeal_iff).

The case p = Xⁿ - a is the radical extension L = K(a^{1/n}): then p'(x) = n xⁿ⁻¹, and multiplying by x gives n a ∈ 𝔇_{B/A}.

Main results

• TauCeti.aeval_derivative_mem_differentIdeal_of_aeval_eq_zero: p'(x) ∈ 𝔇_{B/A} for every p ∈ A[X] with p(x) = 0.
• TauCeti.natCast_mul_mem_differentIdeal_of_pow_eq: if xⁿ = a ∈ A, then n a ∈ 𝔇_{B/A}.

References

• J. Neukirch, Algebraic Number Theory, Chapter III, §2.
• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Appendix, Proposition A.5.

theorem TauCeti.aeval_derivative_mem_differentIdeal_of_aeval_eq_zero {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [Field L] [CommRing B] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] {x : B} (hx : K[(algebraMap B L) x] = ⊤) {p : Polynomial A} (hp : (Polynomial.aeval x) p = 0) : (Polynomial.aeval x) (Polynomial.derivative p) ∈ differentIdeal A B

The derivative of an annihilating polynomial lies in the different. If x ∈ B generates L over K and p ∈ A[X] vanishes at x, then p'(x) ∈ 𝔇_{B/A}. For p the minimal polynomial of x this is Mathlib's aeval_derivative_mem_differentIdeal.

theorem TauCeti.natCast_mul_mem_differentIdeal_of_pow_eq {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [Field L] [CommRing B] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] {x : B} (hx : K[(algebraMap B L) x] = ⊤) {n : ℕ} {a : A} (hxa : x ^ n = (algebraMap A B) a) : ↑n * (algebraMap A B) a ∈ differentIdeal A B

A radical generator puts n a in the different. If x ∈ B generates L over K and xⁿ = a with a ∈ A, then n a ∈ 𝔇_{B/A}.