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.instFreeIntSubtypeMemSubmoduleSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleToAlgebraToCommSemiringToSemifieldIdSetLikeCoeToSubmoduleNonZeroDivisorsToMonoidWithZeroToSemiringInstSemiringIntAddCommMonoidIntModuleAddCommGroupToRingToAddCommGroup (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K) : Module.Free ℤ ↥↑I

Equations

• (_ : Module.Free ℤ ↥↑I) = (_ : Module.Free ℤ ↥↑I)

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

Equations

• (_ : Module.Finite ℤ ↥↑I) = (_ : Module.Finite ℤ ↥↑I)

instance NumberField.instIsLocalizedModuleIntInstCommSemiringIntNonZeroDivisorsToMonoidWithZeroInstSemiringIntSubtypeMemSubmoduleSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleToAlgebraToCommSemiringToSemifieldIdSetLikeCoeToSubmoduleNonZeroDivisorsToMonoidWithZeroToSemiringValFractionalIdealToMonoidToSemiringToDivisionSemiringSemifieldIsDomainToIsDomainIsDedekindDomainIsDomainTo_principal_ideal_domainInstIsDedekindDomainSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingInstIsFractionRingSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAlgebraToCommSemiringToSemifieldIdAddCommMonoidIntModuleAddCommGroupToRingToAddCommGroupRestrictScalarsModuleIntModuleSubtype (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) : IsLocalizedModule (nonZeroDivisors ℤ) (↑ℤ (Submodule.subtype ↑↑I))

Equations

• (_ : IsLocalizedModule (nonZeroDivisors ℤ) (↑ℤ (Submodule.subtype ↑↑I))) = (_ : IsLocalizedModule (nonZeroDivisors ℤ) (↑ℤ (Submodule.subtype ↑↑I)))

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

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 ℤ) (↑ℤ (Submodule.subtype ↑↑I)) (NumberField.fractionalIdealBasis K ↑I)

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)ˣ) : FiniteDimensional.finrank ℤ ↥↑↑I = FiniteDimensional.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) : |(Basis.det (NumberField.integralBasis K)) ⇑(Basis.reindex (NumberField.basisOfFractionalIdeal K I) 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.