The conductor of a number-field order

The conductor of an order O is the largest ideal of the maximal order contained in O. Equivalently, it consists of the algebraic integers x for which x * y belongs to O for every algebraic integer y. This ideal controls the primes where extension and contraction of ideals between O and the maximal order can fail to be inverse.

The conductor here belongs to an arbitrary order. Mathlib's conductor ℤ x describes only the monogenic order generated by one element.

References

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

def TauCeti.GlobalNumberFields.NumberFieldOrder.conductor {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : Ideal (NumberField.RingOfIntegers K)

The largest ideal of 𝓞 K whose elements all lie in the order O.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_conductor_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : NumberField.RingOfIntegers K) : x ∈ O.conductor ↔ ∀ (y : NumberField.RingOfIntegers K), ↑x * ↑y ∈ O.toSubalgebra

An algebraic integer is in the conductor exactly when all of its multiples by algebraic integers lie in the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductor_le_order {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {x : NumberField.RingOfIntegers K} (hx : x ∈ O.conductor) : ↑x ∈ O.toSubalgebra

The conductor is contained in the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductor_le_toRingOfIntegers {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ↑O.conductor ⊆ ↑O.toRingOfIntegers

The conductor, as a set of algebraic integers, is contained in the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_toRingOfIntegers_of_sub_one_mem_conductor {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {α : NumberField.RingOfIntegers K} (hα : α - 1 ∈ O.conductor) : α ∈ O.toRingOfIntegers

An algebraic integer congruent to one modulo the conductor lies in the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_toRingOfIntegers_of_mk_eq {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {α β : NumberField.RingOfIntegers K} (hβ : β ∈ O.toRingOfIntegers) (h : (Ideal.Quotient.mk O.conductor) α = (Ideal.Quotient.mk O.conductor) β) : α ∈ O.toRingOfIntegers

An algebraic integer congruent to an element of the order modulo the conductor lies in the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.le_conductor_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : Ideal (NumberField.RingOfIntegers K)) : I ≤ O.conductor ↔ ∀ x ∈ I, ↑x ∈ O.toSubalgebra

Every maximal-order ideal contained in an order lies in its conductor.

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

Enlarging an order enlarges its conductor ideal in the maximal order.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductor_maximal {K : Type u_1} [Field K] [NumberField K] : (maximalNumberFieldOrder K).conductor = ⊤

The conductor of the maximal order is the unit ideal.

@[simp]

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

An order is maximal exactly when its conductor is the unit ideal.