The different of a monogenic extension

When the integral closure B of A in L is generated over A by a single element x — the monogenic case — the different ideal is generated by f'(x), where f is the minimal polynomial of x:

differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))}.

This is the computational handle on the different. Without it the different is only accessible through the trace dual, which is not something one evaluates at a specific extension.

The conductor is what makes this work

Mathlib supplies the general identity

conductor A x * differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))} (conductor_mul_differentIdeal),

which holds for any x generating L over K, monogenic or not. The order conductor measures exactly the failure of A[x] to be all of B, so the monogenic hypothesis is precisely the statement that it is the unit ideal (conductor_eq_top_of_adjoin_eq_top). This file records the resulting closed form; it reproves neither half.

Only the ring generation hypothesis Algebra.adjoin A {x} = ⊤ is needed. Mathlib's identity also asks that x generate L over K, but in this setting that follows: L is the fraction field of B = A[x], so every element of L is a ratio of two polynomials in x (TauCeti.IntermediateField.adjoin_eq_top_of_algebra_adjoin_eq_top).

Main results

• TauCeti.differentIdeal_eq_span_aeval_derivative_minpoly: the closed form.

References

• J. Neukirch, Algebraic Number Theory, Chapter III, §2.
• J-P. Serre, Local Fields, Chapter III, §6.

theorem TauCeti.differentIdeal_eq_span_aeval_derivative_minpoly (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] [FiniteDimensional K L] [Algebra.IsSeparable K L] (x : B) (hx : A[x] = ⊤) : differentIdeal A B = Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}

The different of a monogenic extension is generated by f'(x). The hypothesis is that x generates B as an A-algebra; that it also generates L over K is a consequence, since L is the fraction field of B.