Fractional ideals of an order as lattices

A fractional ideal I of an order O in a number field K is a finitely generated free ℤ-module, and when I ≠ 0 it spans K over ℚ, so its ℤ-rank is the degree [K : ℚ]. Any ℤ-basis of I is therefore a ℚ-basis of K. These are the facts that let one compute with a fractional ideal of an order through coordinates, as one does for the lattices [α, β] of a quadratic order.

Main results

• TauCeti.GlobalNumberFields.NumberFieldOrder.span_rat_eq_top: a nonzero fractional ideal of an order spans its number field over ℚ.
• TauCeti.GlobalNumberFields.NumberFieldOrder.span_int_range_basis: the members of a ℤ-basis of a fractional ideal span it over ℤ.
• TauCeti.GlobalNumberFields.NumberFieldOrder.span_rat_range_basis: the members of any ℤ-basis of a nonzero fractional ideal span the number field over ℚ.
• TauCeti.GlobalNumberFields.NumberFieldOrder.finrank_int_eq_finrank_rat: a nonzero fractional ideal has ℤ-rank [K : ℚ].
• TauCeti.GlobalNumberFields.NumberFieldOrder.exists_basis_restrictScalars_eq_span: a nonzero fractional ideal of an order is the ℤ-span of a ℚ-basis of the number field.

Implementation notes

This generalises Mathlib's treatment of fractional ideals of the maximal order 𝓞 K in Mathlib/NumberTheory/NumberField/FractionalIdeal.lean. The Module.Finite ℤ and Module.Free ℤ instances follow its instances for 𝓞 K, which transport the ideal to its numerator (there along FractionalIdeal.equivNum, here along FractionalIdeal.equivNumOfIsLocalization). The results span_int_range_basis and finrank_int_eq_finrank_rat are the order analogues of NumberField.mem_span_basisOfFractionalIdeal and NumberField.fractionalIdeal_rank, which Mathlib states only for 𝓞 K.

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.

instance TauCeti.GlobalNumberFields.NumberFieldOrder.instFiniteIntSubtypeMemSubmoduleSubalgebraToSubalgebraCoeToSubmodule {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) : Module.Finite ℤ ↥↑I

A fractional ideal of an order is a finitely generated ℤ-module: it is isomorphic to its numerator, an ideal of the order, which lies in the finitely generated ℤ-module O.

instance TauCeti.GlobalNumberFields.NumberFieldOrder.instFreeIntSubtypeMemSubmoduleSubalgebraToSubalgebraCoeToSubmodule {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) : Module.Free ℤ ↥↑I

A fractional ideal of an order is a free ℤ-module.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.span_rat_eq_top {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) : Submodule.span ℚ ↑I = ⊤

A nonzero fractional ideal of an order spans its number field over ℚ. It contains x O for each of its nonzero elements x, and O spans K over ℚ.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.span_int_range_basis {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} {ι : Type u_2} (b : Module.Basis ι ℤ ↥↑I) : ↑(Submodule.span ℤ (Set.range fun (i : ι) => ↑(b i))) = ↑I

The members of a ℤ-basis of a fractional ideal span it over ℤ.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.span_rat_range_basis {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) {ι : Type u_2} (b : Module.Basis ι ℤ ↥↑I) : Submodule.span ℚ (Set.range fun (i : ι) => ↑(b i)) = ⊤

A ℤ-basis of a nonzero fractional ideal spans the number field over ℚ.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.finrank_int_eq_finrank_rat {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) : Module.finrank ℤ ↥↑I = Module.finrank ℚ K

A nonzero fractional ideal of an order has ℤ-rank [K : ℚ]. A ℤ-basis of the ideal is linearly independent over ℚ and spans K, so it is a ℚ-basis of K.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.exists_basis_restrictScalars_eq_span {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) : ∃ (b : Module.Basis (Fin (Module.finrank ℚ K)) ℚ K), Submodule.restrictScalars ℤ ↑I = Submodule.span ℤ (Set.range ⇑b)

A nonzero fractional ideal of an order is the ℤ-span of a ℚ-basis of the number field. A ℤ-basis of the ideal is linearly independent over ℚ and spans K.