HepLean Documentation

Mathlib.NumberTheory.NumberField.FractionalIdeal

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 (NumberField.RingOfIntegers K)) K) :

Module.Free ℤ ↥↑I

Equations

⋯ = ⋯

instance NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) :

Module.Finite ℤ ↥↑I

Equations

⋯ = ⋯

instance NumberField.instIsLocalizedModuleIntNonZeroDivisorsSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealRestrictScalarsSubtype (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) :

IsLocalizedModule (nonZeroDivisors ℤ) (↑ℤ (↑↑I).subtype)

Equations

⋯ = ⋯

noncomputable def NumberField.fractionalIdealBasis (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) :

Basis (Module.Free.ChooseBasisIndex ℤ ↥↑I) ℤ ↥↑I

A ℤ-basis of a fractional ideal.

Equations

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

Instances For

noncomputable def NumberField.basisOfFractionalIdeal (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) :

Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℚ K

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

Equations

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

Instances For

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

(NumberField.basisOfFractionalIdeal K I) i = ↑((NumberField.fractionalIdealBasis K ↑I) i)

theorem NumberField.mem_span_basisOfFractionalIdeal (K : Type u_1) [Field K] [NumberField K] {I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ} {x : K} :

x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I

theorem NumberField.fractionalIdeal_rank (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) :

Module.finrank ℤ ↥↑↑I = Module.finrank ℤ (NumberField.RingOfIntegers K)

theorem NumberField.det_basisOfFractionalIdeal_eq_absNorm (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) (e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I) :

|(NumberField.integralBasis K).det ⇑((NumberField.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.