Number fields

This file defines a number field and the ring of integers corresponding to it.

Main definitions

• NumberField defines a number field as a field which has characteristic zero and is finite dimensional over ℚ.
• ringOfIntegers defines the ring of integers (or number ring) corresponding to a number field as the integral closure of ℤ in the number field.

Implementation notes

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice.

References

• [D. Marcus, Number Fields][marcus1977number]
• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [P. Samuel, Algebraic Theory of Numbers][samuel1970algebraic]

Tags

number field, ring of integers

class NumberField (K : Type u_1) [Field K] : Prop

• to_charZero : CharZero K
• to_finiteDimensional : FiniteDimensional ℚ K

A number field is a field which has characteristic zero and is finite dimensional over ℚ.

theorem Int.not_isField : ¬IsField ℤ

ℤ with its usual ring structure is not a field.

theorem NumberField.isAlgebraic (K : Type u_1) [Field K] [nf : NumberField K] : Algebra.IsAlgebraic ℚ K

def NumberField.ringOfIntegers (K : Type u_1) [Field K] : Subalgebra ℤ K

The ring of integers (or number ring) corresponding to a number field is the integral closure of ℤ in the number field.

Equations

• NumberField.ringOfIntegers K = integralClosure ℤ K

def NumberField.term𝓞 : Lean.ParserDescr

Equations

• NumberField.term𝓞 = Lean.ParserDescr.node `NumberField.term𝓞 1024 (Lean.ParserDescr.symbol "𝓞")

theorem NumberField.mem_ringOfIntegers (K : Type u_1) [Field K] (x : K) : x ∈ NumberField.ringOfIntegers K ↔ IsIntegral ℤ x

theorem NumberField.isIntegral_of_mem_ringOfIntegers {K : Type u_3} [Field K] {x : K} (hx : x ∈ NumberField.ringOfIntegers K) : IsIntegral ℤ { val := x, property := hx }

instance NumberField.inst_ringOfIntegersAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Algebra { x // x ∈ NumberField.ringOfIntegers K } { x // x ∈ NumberField.ringOfIntegers L }

Given an algebra between two fields, create an algebra between their two rings of integers.

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.RingOfIntegers.instIsFractionRingSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAlgebraToCommSemiringToSemifieldId {K : Type u_1} [Field K] [NumberField K] : IsFractionRing { x // x ∈ NumberField.ringOfIntegers K } K

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.RingOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommSemiringToCommSemiringToSemifieldToAlgebraId {K : Type u_1} [Field K] : IsIntegralClosure { x // x ∈ NumberField.ringOfIntegers K } ℤ K

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.RingOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRing {K : Type u_1} [Field K] [NumberField K] : IsIntegrallyClosed { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.RingOfIntegers.isIntegral_coe {K : Type u_1} [Field K] (x : { x // x ∈ NumberField.ringOfIntegers K }) : IsIntegral ℤ ↑x

theorem NumberField.RingOfIntegers.map_mem {K : Type u_1} [Field K] {F : Type u_3} {L : Type u_4} [Field L] [CharZero K] [CharZero L] [AlgHomClass F ℚ K L] (f : F) (x : { x // x ∈ NumberField.ringOfIntegers K }) : ↑f ↑x ∈ NumberField.ringOfIntegers L

noncomputable def NumberField.RingOfIntegers.equiv {K : Type u_1} [Field K] (R : Type u_3) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] : { x // x ∈ NumberField.ringOfIntegers K } ≃+* R

The ring of integers of K are equivalent to any integral closure of ℤ in K

Equations

• NumberField.RingOfIntegers.equiv R = AlgEquiv.toRingEquiv (AlgEquiv.symm (IsIntegralClosure.equiv ℤ R K { x // x ∈ NumberField.ringOfIntegers K }))

instance NumberField.RingOfIntegers.instCharZeroSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToAddMonoidWithOneToAddGroupWithOneToRing (K : Type u_1) [Field K] [nf : NumberField K] : CharZero { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.RingOfIntegers.instIsNoetherianIntSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersInstSemiringIntToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingIntModuleToAddCommGroup (K : Type u_1) [Field K] [nf : NumberField K] : IsNoetherian ℤ { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.RingOfIntegers.not_isField (K : Type u_1) [Field K] [nf : NumberField K] : ¬IsField { x // x ∈ NumberField.ringOfIntegers K }

The ring of integers of a number field is not a field.

instance NumberField.RingOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRing (K : Type u_1) [Field K] [nf : NumberField K] : IsDedekindDomain { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.RingOfIntegers.instFreeIntSubtypeMemSubalgebraToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersInstSemiringIntToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingIntModuleToAddCommGroup (K : Type u_1) [Field K] [nf : NumberField K] : Module.Free ℤ { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.RingOfIntegers.instIsLocalizationSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommSemiringToCommSemiringToSemifieldAlgebraMapSubmonoidInstCommSemiringIntToSemiringAlgebraNonZeroDivisorsToMonoidWithZeroInstSemiringIntToAlgebraId (K : Type u_1) [Field K] [nf : NumberField K] : IsLocalization (Algebra.algebraMapSubmonoid { x // x ∈ NumberField.ringOfIntegers K } (nonZeroDivisors ℤ)) K

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NumberField.RingOfIntegers.basis (K : Type u_1) [Field K] [nf : NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) ℤ { x // x ∈ NumberField.ringOfIntegers K }

A ℤ-basis of the ring of integers of K.

Equations

• NumberField.RingOfIntegers.basis K = Module.Free.chooseBasis ℤ { x // x ∈ NumberField.ringOfIntegers K }

noncomputable def NumberField.integralBasis (K : Type u_1) [Field K] [nf : NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) ℚ K

A basis of K over ℚ that is also a basis of 𝓞 K over ℤ.

Equations

• NumberField.integralBasis K = Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K (NumberField.RingOfIntegers.basis K)

@[simp]

theorem NumberField.integralBasis_apply (K : Type u_1) [Field K] [nf : NumberField K] (i : Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) : ↑(NumberField.integralBasis K) i = ↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } K) (↑(NumberField.RingOfIntegers.basis K) i)

theorem NumberField.mem_span_integralBasis (K : Type u_1) [Field K] [nf : NumberField K] {x : K} : x ∈ Submodule.span ℤ (Set.range ↑(NumberField.integralBasis K)) ↔ x ∈ NumberField.ringOfIntegers K

theorem NumberField.RingOfIntegers.rank (K : Type u_1) [Field K] [nf : NumberField K] : FiniteDimensional.finrank ℤ { x // x ∈ NumberField.ringOfIntegers K } = FiniteDimensional.finrank ℚ K

instance Rat.numberField : NumberField ℚ

Equations

• Rat.numberField = Rat.numberField.proof_1

noncomputable def Rat.ringOfIntegersEquiv : { x // x ∈ NumberField.ringOfIntegers ℚ } ≃+* ℤ

The ring of integers of ℚ as a number field is just ℤ.

Equations

• Rat.ringOfIntegersEquiv = NumberField.RingOfIntegers.equiv ℤ

instance AdjoinRoot.instNumberFieldAdjoinRootRatCommRingFieldField {f : Polynomial ℚ} [hf : Fact (Irreducible f)] : NumberField (AdjoinRoot f)

The quotient of ℚ[X] by the ideal generated by an irreducible polynomial of ℚ[X] is a number field.

Equations

• @AdjoinRoot.instNumberFieldAdjoinRootRatCommRingFieldField = @AdjoinRoot.instNumberFieldAdjoinRootRatCommRingFieldField.proof_1