The index and discriminant of a number-field order

An order O of a number field K is a full-rank sublattice of the maximal order 𝓞 K, so it has a finite index [𝓞 K : O]. Its discriminant is the discriminant of any ℤ-basis of O. The two are tied to the field discriminant by the classical formula

disc O = [𝓞 K : O] ^ 2 * disc K,

which follows by expressing a basis of O in a basis of 𝓞 K: the change of basis matrix has determinant ± [𝓞 K : O]. This is the argument of TauCeti.NumberField.IntegralPrimitiveElement.discr_minpoly_eq_index_sq_mul_discr for a monogenic order ℤ[θ], run with an arbitrary ℤ-basis of O in place of a power basis.

The index annihilates 𝓞 K / O, so it lies in the conductor of O. Consequently the conductor is a nonzero ideal, and a prime of 𝓞 K containing the conductor lies above a prime number whose square divides disc O. In particular an order with squarefree discriminant is maximal.

Main definitions

• TauCeti.GlobalNumberFields.NumberFieldOrder.index: the index [𝓞 K : O].
• TauCeti.GlobalNumberFields.NumberFieldOrder.discr: the discriminant of an order.

Main results

• TauCeti.GlobalNumberFields.NumberFieldOrder.discr_eq_index_sq_mul: disc O = [𝓞 K : O] ^ 2 * disc K.
• TauCeti.GlobalNumberFields.NumberFieldOrder.index_dvd_index_of_le: a larger order has an index dividing that of a smaller one.
• TauCeti.GlobalNumberFields.NumberFieldOrder.natCast_index_mem_conductor: the index lies in the conductor.
• TauCeti.GlobalNumberFields.NumberFieldOrder.conductor_ne_bot: the conductor is nonzero.
• TauCeti.GlobalNumberFields.NumberFieldOrder.sq_ringChar_dvd_discr_of_conductor_le: the residue characteristic of a prime containing the conductor has square dividing disc O.
• TauCeti.GlobalNumberFields.NumberFieldOrder.eq_maximal_of_squarefree_discr: an order with squarefree discriminant is the maximal order.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §2 and §12.
• G. S. Kopp and J. C. Lagarias, Class Field Theory for Orders of Number Fields, §2.

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.index {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ℕ

The index [𝓞 K : O] of an order in the maximal order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.index_def {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.index = Nat.card (NumberField.RingOfIntegers K ⧸ Subalgebra.toSubmodule O.toRingOfIntegers)

The index of an order is the cardinality of the additive quotient 𝓞 K / O.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.index_eq_addSubgroup_index {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.index = (Subalgebra.toSubmodule O.toRingOfIntegers).toAddSubgroup.index

The index of an order is the index of O as an additive subgroup of 𝓞 K. This unfolds Submodule.cardQuot, through which NumberFieldOrder.index is defined.

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.discr {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ℤ

The discriminant of an order: the discriminant of a ℤ-basis of it. By NumberFieldOrder.discr_eq_discr it does not depend on the basis.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.discr_eq_discr {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥O.toSubalgebra) : Algebra.discr ℤ ⇑b = O.discr

Any ℤ-basis of an order computes its discriminant.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.discr_ne_zero {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.discr ≠ 0

The discriminant of an order is nonzero.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.discr_eq_index_sq_mul {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.discr = ↑O.index ^ 2 * NumberField.discr K

The index formula for discriminants. The discriminant of an order is the square of its index in the maximal order times the discriminant of the number field.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.sq_index_dvd_discr {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ↑O.index ^ 2 ∣ O.discr

The square of the index of an order divides its discriminant.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.index_ne_zero {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.index ≠ 0

The index of an order in the maximal order is nonzero.

instance TauCeti.GlobalNumberFields.NumberFieldOrder.instNeZeroNatIndex {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : NeZero O.index

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.index_dvd_index_of_le {K : Type u_1} [Field K] [NumberField K] {O O' : NumberFieldOrder K} (h : O.toSubalgebra ≤ O'.toSubalgebra) : O'.index ∣ O.index

A larger order has smaller index: if O ⊆ O', then [𝓞 K : O'] divides [𝓞 K : O].

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.natCast_index_mem_conductor {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ↑O.index ∈ O.conductor

The index annihilates 𝓞 K / O, so it lies in the conductor of O.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductor_ne_bot {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.conductor ≠ ⊥

The conductor of an order is a nonzero ideal of the maximal order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.ringChar_dvd_index_of_conductor_le {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {P : Ideal (NumberField.RingOfIntegers K)} (h : O.conductor ≤ P) : ringChar (NumberField.RingOfIntegers K ⧸ P) ∣ O.index

The residue characteristic of an ideal of 𝓞 K containing the conductor divides the index.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.sq_ringChar_dvd_discr_of_conductor_le {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {P : Ideal (NumberField.RingOfIntegers K)} (h : O.conductor ≤ P) : ↑(ringChar (NumberField.RingOfIntegers K ⧸ P)) ^ 2 ∣ O.discr

The square of the residue characteristic of an ideal of 𝓞 K containing the conductor divides the discriminant of the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.index_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.index = 1 ↔ O = maximalNumberFieldOrder K

An order has index one exactly when it is the maximal order.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.index_maximal {K : Type u_1} [Field K] [NumberField K] : (maximalNumberFieldOrder K).index = 1

The maximal order has index one.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.discr_maximal {K : Type u_1} [Field K] [NumberField K] : (maximalNumberFieldOrder K).discr = NumberField.discr K

The discriminant of the maximal order is the discriminant of the number field.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.discr_eq_discr_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.discr = NumberField.discr K ↔ O = maximalNumberFieldOrder K

An order has the discriminant of its number field exactly when it is the maximal order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.eq_maximal_of_squarefree_discr {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (h : Squarefree O.discr) : O = maximalNumberFieldOrder K

An order whose discriminant is squarefree is the maximal order.