Stickelberger's congruence

The discriminant of a number field is congruent to 0 or 1 modulo 4.

Let b be a ℚ-basis of the number field K consisting of algebraic integers, and let M be the matrix of its images under the embeddings of K into an algebraic closure E of ℚ, so that disc b = (det M) ^ 2. Splitting the Leibniz expansion of det M into the sums P and N over the even and the odd permutations gives disc b = (P + N) ^ 2 - 4 * (P * N). An automorphism of E permutes the embeddings, hence the columns of M, and so fixes P + N and P * N. Both are algebraic integers, so both are rational integers, and disc b is a square minus four times an integer. Taking b to be an integral basis gives the congruence for NumberField.discr K.

The congruence concerns the absolute discriminant only: the relative discriminant of an extension of Dedekind domains is an ideal, and has no residue modulo 4.

Main results

• Module.Basis.exists_discr_eq_sq_sub_four_mul_of_isIntegral: the discriminant of a ℚ-basis of algebraic integers has the form s ^ 2 - 4 * p with s p : ℤ.
• TauCeti.NumberField.exists_discr_eq_sq_sub_four_mul: the same for the discriminant of K.
• TauCeti.NumberField.discr_emod_four_eq_zero_or_one: Stickelberger's congruence, NumberField.discr K % 4 = 0 ∨ NumberField.discr K % 4 = 1.

References

• L. Stickelberger, Über eine neue Eigenschaft der Diskriminanten algebraischer Zahlkörper, Verhandlungen des ersten Internationalen Mathematiker-Kongresses (1897).
• W. Narkiewicz, Elementary and Analytic Theory of Algebraic Numbers, Chapter 4.

theorem Module.Basis.exists_discr_eq_sq_sub_four_mul_of_isIntegral {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℚ K) (hb : ∀ (i : ι), IsIntegral ℤ (b i)) : ∃ (s : ℤ) (p : ℤ), Algebra.discr ℚ ⇑b = ↑s ^ 2 - 4 * ↑p

The discriminant of a basis of algebraic integers is a square minus four times an integer. For a ℚ-basis b of a number field consisting of algebraic integers, there are s p : ℤ with Algebra.discr ℚ b = s ^ 2 - 4 * p; here s and p are the sum and the product of the even and the odd parts of the Leibniz expansion of the embedding determinant.

theorem TauCeti.NumberField.exists_discr_eq_sq_sub_four_mul (K : Type u_1) [Field K] [NumberField K] : ∃ (s : ℤ) (p : ℤ), NumberField.discr K = s ^ 2 - 4 * p

The discriminant of a number field is a square minus four times an integer.

theorem TauCeti.NumberField.discr_emod_four_eq_zero_or_one (K : Type u_1) [Field K] [NumberField K] : NumberField.discr K % 4 = 0 ∨ NumberField.discr K % 4 = 1

Stickelberger's congruence. The discriminant of a number field is congruent to 0 or 1 modulo 4.