The different of a monogenic quadratic field #
For a number field K with an algebraic integer θ such that minpoly ℤ θ = X² − d and
𝓞 K = ℤ[θ], the different of 𝓞 K over ℤ is generated by the derivative f'(θ) = 2θ of
the minimal polynomial: 𝔡 = (2θ). This is the monogenic different formula in the quadratic
case, uniform in the radicand d; the generation hypothesis 𝓞 K = ℤ[θ] holds for instance
when d is squarefree and not 1 modulo 4 (adjoin_gen_eq_top_of_mod_four_ne_one).
Main results #
TauCeti.NumberField.differentIdeal_eq_span_two_mul_gen:differentIdeal ℤ (𝓞 K) = (2θ).
theorem
TauCeti.NumberField.differentIdeal_eq_span_two_mul_gen
{K : Type u_1}
[Field K]
[NumberField K]
{θ : NumberField.RingOfIntegers K}
{d : ℤ}
(hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d)
(hadj : ℤ[θ] = ⊤)
:
The different of ℤ[θ] is generated by f'(θ) = 2θ when 𝓞 K = ℤ[θ] and
minpoly ℤ θ = X² − d.