Fractional ideals of number fields

Prove some results on the fractional ideals of number fields.

Main definitions and results

• NumberField.basisOfFractionalIdeal: A ℚ-basis of K that spans I over ℤ where I is a fractional ideal of a number field K.
• NumberField.det_basisOfFractionalIdeal_eq_absNorm: for I a fractional ideal of a number field K, the absolute value of the determinant of the base change from integralBasis to basisOfFractionalIdeal I is equal to the norm of I.

instance NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K) : Module.Free ℤ ↥↑I

instance NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K) : Module.Finite ℤ ↥↑I

instance NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : IsLocalizedModule (nonZeroDivisors ℤ) (↑ℤ (↑↑I).subtype)

noncomputable def NumberField.fractionalIdealBasis (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K) : Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑I) ℤ ↥↑I

A ℤ-basis of a fractional ideal.

Equations

• NumberField.fractionalIdealBasis K I = Module.Free.chooseBasis ℤ ↥↑I

noncomputable def NumberField.basisOfFractionalIdeal (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℚ K

A ℚ-basis of K that spans I over ℤ, see mem_span_basisOfFractionalIdeal below.

Equations

• NumberField.basisOfFractionalIdeal K I = Module.Basis.ofIsLocalizedModule ℚ (nonZeroDivisors ℤ) (↑ℤ (↑↑I).subtype) (NumberField.fractionalIdealBasis K ↑I)

theorem NumberField.basisOfFractionalIdeal_apply (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : (basisOfFractionalIdeal K I) i = ↑((fractionalIdealBasis K ↑I) i)

theorem NumberField.mem_span_basisOfFractionalIdeal (K : Type u_1) [Field K] [NumberField K] {I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ} {x : K} : x ∈ Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I

theorem NumberField.fractionalIdeal_rank (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Module.finrank ℤ ↥↑↑I = Module.finrank ℤ (RingOfIntegers K)

theorem NumberField.det_basisOfFractionalIdeal_eq_absNorm (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (e : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| = FractionalIdeal.absNorm ↑I

The absolute value of the determinant of the base change from integralBasis to basisOfFractionalIdeal I is equal to the norm of I.