The conductor form of quadratic orders

Every order O in a quadratic number field has the form ℤ + f 𝓞 K, where f = [𝓞 K : O], and its conductor is the principal ideal f 𝓞 K. This is the arithmetic description used to express the Picard group of a quadratic order as a congruence quotient of maximal-order ideals.

The results apply to real and imaginary quadratic fields alike. The degree-two hypothesis is essential: orders in higher-degree fields need not have this form.

References

• D. A. Cox, Primes of the Form x² + ny², §7, Proposition 7.2.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_toRingOfIntegers_iff_exists_int_add_index_mul {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (hK : Module.finrank ℚ K = 2) (x : NumberField.RingOfIntegers K) : x ∈ O.toRingOfIntegers ↔ ∃ (a : ℤ) (y : NumberField.RingOfIntegers K), x = ↑a + ↑O.index * y

An element of the maximal order lies in a quadratic order exactly when it is an integer plus the index of the order times an algebraic integer: O = ℤ + [𝓞 K : O] 𝓞 K.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductor_eq_span_index {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (hK : Module.finrank ℚ K = 2) : O.conductor = Ideal.span {↑O.index}

The conductor of a quadratic order is generated by its index in the maximal order.