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
• J.W.S. Cassels, A. Frölich, Algebraic Number Theory
• [P. Samuel, Algebraic Theory of Numbers][samuel1970algebraic]

Tags

number field, ring of integers

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

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

Stacks Tag 09GA

• to_charZero : CharZero K
• to_finiteDimensional : FiniteDimensional ℚ K

theorem Int.not_isField : ¬IsField ℤ

ℤ with its usual ring structure is not a field.

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

instance NumberField.instFiniteDimensional (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] : FiniteDimensional K L

Equations

• ⋯ = ⋯

theorem NumberField.of_module_finite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [Algebra K L] [Module.Finite K L] : NumberField L

A finite extension of a number field is a number field.

instance NumberField.of_intermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (E : IntermediateField K L) : NumberField ↥E

Equations

• ⋯ = ⋯

theorem NumberField.of_tower (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (E : Type u_3) [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] : NumberField E

def NumberField.RingOfIntegers (K : Type u_1) [Field K] : Type u_1

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

This is defined as its own type, rather than a Subalgebra, for performance reasons: looking for instances of the form SMul (RingOfIntegers _) (RingOfIntegers _) makes much more effective use of the discrimination tree than instances of the form SMul (Subtype _) (Subtype _). The drawback is we have to copy over instances manually.

Equations

• NumberField.RingOfIntegers K = ↥(integralClosure ℤ K)

def NumberField.term𝓞 : Lean.ParserDescr

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

This is defined as its own type, rather than a Subalgebra, for performance reasons: looking for instances of the form SMul (RingOfIntegers _) (RingOfIntegers _) makes much more effective use of the discrimination tree than instances of the form SMul (Subtype _) (Subtype _). The drawback is we have to copy over instances manually.

Equations

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

instance NumberField.RingOfIntegers.instCommRing (K : Type u_1) [Field K] : CommRing (NumberField.RingOfIntegers K)

Equations

• NumberField.RingOfIntegers.instCommRing K = inferInstanceAs (CommRing ↥(integralClosure ℤ K))

instance NumberField.RingOfIntegers.instIsDomain (K : Type u_1) [Field K] : IsDomain (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instCharZero (K : Type u_1) [Field K] [NumberField K] : CharZero (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instAlgebra (K : Type u_1) [Field K] : Algebra (NumberField.RingOfIntegers K) K

Equations

• NumberField.RingOfIntegers.instAlgebra K = inferInstanceAs (Algebra (↥(integralClosure ℤ K)) K)

instance NumberField.RingOfIntegers.instNoZeroSMulDivisors (K : Type u_1) [Field K] : NoZeroSMulDivisors (NumberField.RingOfIntegers K) K

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instNontrivial (K : Type u_1) [Field K] : Nontrivial (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instAlgebra_1 (K : Type u_1) [Field K] {L : Type u_3} [Ring L] [Algebra K L] : Algebra (NumberField.RingOfIntegers K) L

Equations

• NumberField.RingOfIntegers.instAlgebra_1 K = inferInstanceAs (Algebra (↥(integralClosure ℤ K)) L)

instance NumberField.RingOfIntegers.instIsScalarTower (K : Type u_1) [Field K] {L : Type u_3} [Ring L] [Algebra K L] : IsScalarTower (NumberField.RingOfIntegers K) K L

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev NumberField.RingOfIntegers.val {K : Type u_1} [Field K] (x : NumberField.RingOfIntegers K) : K

The canonical coercion from 𝓞 K to K.

Equations

• ↑x = (algebraMap (NumberField.RingOfIntegers K) K) x

instance NumberField.RingOfIntegers.instCoeHead {K : Type u_1} [Field K] : CoeHead (NumberField.RingOfIntegers K) K

This instance has to be CoeHead because we only want to apply it from 𝓞 K to K.

Equations

• NumberField.RingOfIntegers.instCoeHead = { coe := NumberField.RingOfIntegers.val }

theorem NumberField.RingOfIntegers.coe_eq_algebraMap {K : Type u_1} [Field K] (x : NumberField.RingOfIntegers K) : ↑x = (algebraMap (NumberField.RingOfIntegers K) K) x

theorem NumberField.RingOfIntegers.ext {K : Type u_1} [Field K] {x y : NumberField.RingOfIntegers K} (h : ↑x = ↑y) : x = y

theorem NumberField.RingOfIntegers.eq_iff {K : Type u_1} [Field K] {x y : NumberField.RingOfIntegers K} : ↑x = ↑y ↔ x = y

@[simp]

theorem NumberField.RingOfIntegers.map_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure ℤ K) : (algebraMap (NumberField.RingOfIntegers K) K) ⟨x, hx⟩ = x

theorem NumberField.RingOfIntegers.coe_mk {K : Type u_1} [Field K] {x : K} (hx : x ∈ integralClosure ℤ K) : ↑⟨x, hx⟩ = x

theorem NumberField.RingOfIntegers.mk_eq_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) : ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y

@[simp]

theorem NumberField.RingOfIntegers.mk_one {K : Type u_1} [Field K] : ⟨1, ⋯⟩ = 1

@[simp]

theorem NumberField.RingOfIntegers.mk_zero {K : Type u_1} [Field K] : ⟨0, ⋯⟩ = 0

@[simp]

theorem NumberField.RingOfIntegers.mk_add_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) : ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩

@[simp]

theorem NumberField.RingOfIntegers.mk_mul_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

@[simp]

theorem NumberField.RingOfIntegers.mk_sub_mk {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) : ⟨x, hx⟩ - ⟨y, hy⟩ = ⟨x - y, ⋯⟩

@[simp]

theorem NumberField.RingOfIntegers.neg_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure ℤ K) : -⟨x, hx⟩ = ⟨-x, ⋯⟩

def NumberField.RingOfIntegers.mapRingHom {K : Type u_3} {L : Type u_4} {F : Type u_5} [Field K] [Field L] [FunLike F K L] [RingHomClass F K L] (f : F) : NumberField.RingOfIntegers K →+* NumberField.RingOfIntegers L

The ring homomorphism (𝓞 K) →+* (𝓞 L) given by restricting a ring homomorphism f : K →+* L to 𝓞 K.

Equations

• NumberField.RingOfIntegers.mapRingHom f = { toFun := fun (k : NumberField.RingOfIntegers K) => ⟨f ↑k, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def NumberField.RingOfIntegers.mapRingEquiv {K : Type u_3} {L : Type u_4} {E : Type u_5} [Field K] [Field L] [EquivLike E K L] [RingEquivClass E K L] (e : E) : NumberField.RingOfIntegers K ≃+* NumberField.RingOfIntegers L

The ring isomorphsim (𝓞 K) ≃+* (𝓞 L) given by restricting a ring isomorphsim e : K ≃+* L to 𝓞 K.

Equations

• NumberField.RingOfIntegers.mapRingEquiv e = RingEquiv.ofRingHom (NumberField.RingOfIntegers.mapRingHom e) (NumberField.RingOfIntegers.mapRingHom (↑e).symm) ⋯ ⋯

instance NumberField.inst_ringOfIntegersAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Algebra (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

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

Equations

• NumberField.inst_ringOfIntegersAlgebra K L = (NumberField.RingOfIntegers.mapRingHom (algebraMap K L)).toAlgebra

def NumberField.RingOfIntegers.mapAlgHom {k : Type u_3} {K : Type u_4} {L : Type u_5} {F : Type u_6} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [FunLike F K L] [AlgHomClass F k K L] (f : F) : NumberField.RingOfIntegers K →ₐ[NumberField.RingOfIntegers k] NumberField.RingOfIntegers L

The algebra homomorphism (𝓞 K) →ₐ[𝓞 k] (𝓞 L) given by restricting a algebra homomorphism f : K →ₐ[k] L to 𝓞 K.

Equations

• NumberField.RingOfIntegers.mapAlgHom f = { toRingHom := NumberField.RingOfIntegers.mapRingHom f, commutes' := ⋯ }

def NumberField.RingOfIntegers.mapAlgEquiv {k : Type u_3} {K : Type u_4} {L : Type u_5} {E : Type u_6} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [EquivLike E K L] [AlgEquivClass E k K L] (e : E) : NumberField.RingOfIntegers K ≃ₐ[NumberField.RingOfIntegers k] NumberField.RingOfIntegers L

The isomorphism of algebras (𝓞 K) ≃ₐ[𝓞 k] (𝓞 L) given by restricting an isomorphism of algebras e : K ≃ₐ[k] L to 𝓞 K.

Equations

• NumberField.RingOfIntegers.mapAlgEquiv e = AlgEquiv.ofAlgHom (NumberField.RingOfIntegers.mapAlgHom e) (NumberField.RingOfIntegers.mapAlgHom (↑e).symm) ⋯ ⋯

instance NumberField.RingOfIntegers.inst_isScalarTower (k : Type u_3) (K : Type u_4) (L : Type u_5) [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [Algebra K L] [IsScalarTower k K L] : IsScalarTower (NumberField.RingOfIntegers k) (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

Equations

• ⋯ = ⋯

theorem NumberField.RingOfIntegers.coe_injective {K : Type u_1} [Field K] : Function.Injective ⇑(algebraMap (NumberField.RingOfIntegers K) K)

The canonical map from 𝓞 K to K is injective.

This is a convenient abbreviation for NoZeroSMulDivisors.algebraMap_injective.

theorem NumberField.RingOfIntegers.coe_eq_zero_iff {K : Type u_1} [Field K] {x : NumberField.RingOfIntegers K} : (algebraMap (NumberField.RingOfIntegers K) K) x = 0 ↔ x = 0

The canonical map from 𝓞 K to K is injective.

This is a convenient abbreviation for map_eq_zero_iff applied to NoZeroSMulDivisors.algebraMap_injective.

theorem NumberField.RingOfIntegers.coe_ne_zero_iff {K : Type u_1} [Field K] {x : NumberField.RingOfIntegers K} : (algebraMap (NumberField.RingOfIntegers K) K) x ≠ 0 ↔ x ≠ 0

The canonical map from 𝓞 K to K is injective.

This is a convenient abbreviation for map_ne_zero_iff applied to NoZeroSMulDivisors.algebraMap_injective.

theorem NumberField.RingOfIntegers.isIntegral_coe {K : Type u_1} [Field K] (x : NumberField.RingOfIntegers K) : IsIntegral ℤ ((algebraMap (NumberField.RingOfIntegers K) K) x)

theorem NumberField.RingOfIntegers.isIntegral {K : Type u_1} [Field K] (x : NumberField.RingOfIntegers K) : IsIntegral ℤ x

instance NumberField.RingOfIntegers.instIsFractionRing {K : Type u_1} [Field K] [NumberField K] : IsFractionRing (NumberField.RingOfIntegers K) K

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instIsIntegralClosureInt {K : Type u_1} [Field K] : IsIntegralClosure (NumberField.RingOfIntegers K) ℤ K

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instIsIntegralInt {K : Type u_1} [Field K] : Algebra.IsIntegral ℤ (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instIsIntegrallyClosed {K : Type u_1} [Field K] [NumberField K] : IsIntegrallyClosed (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

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

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

Equations

• NumberField.RingOfIntegers.equiv R = (IsIntegralClosure.equiv ℤ R K (NumberField.RingOfIntegers K)).symm.toRingEquiv

instance NumberField.RingOfIntegers.instCharZero_1 (K : Type u_1) [Field K] [CharZero K] : CharZero (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instIsNoetherianInt (K : Type u_1) [Field K] [NumberField K] : IsNoetherian ℤ (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

theorem NumberField.RingOfIntegers.not_isField (K : Type u_1) [Field K] [NumberField K] : ¬IsField (NumberField.RingOfIntegers K)

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

instance NumberField.RingOfIntegers.instIsDedekindDomain (K : Type u_1) [Field K] [NumberField K] : IsDedekindDomain (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instFreeInt (K : Type u_1) [Field K] [NumberField K] : Module.Free ℤ (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors (K : Type u_1) [Field K] [NumberField K] : IsLocalization (Algebra.algebraMapSubmonoid (NumberField.RingOfIntegers K) (nonZeroDivisors ℤ)) K

Equations

• ⋯ = ⋯

noncomputable def NumberField.RingOfIntegers.basis (K : Type u_1) [Field K] [NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℤ (NumberField.RingOfIntegers K)

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

Equations

• NumberField.RingOfIntegers.basis K = Module.Free.chooseBasis ℤ (NumberField.RingOfIntegers K)

def NumberField.RingOfIntegers.restrict {K : Type u_1} [Field K] {M : Type u_3} (f : M → K) (h : ∀ (x : M), IsIntegral ℤ (f x)) (x : M) : NumberField.RingOfIntegers K

Given f : M → K such that ∀ x, IsIntegral ℤ (f x), the corresponding function M → 𝓞 K.

Equations

• NumberField.RingOfIntegers.restrict f h x = ⟨f x, ⋯⟩

def NumberField.RingOfIntegers.restrict_addMonoidHom {K : Type u_1} [Field K] {M : Type u_3} [AddZeroClass M] (f : M →+ K) (h : ∀ (x : M), IsIntegral ℤ (f x)) : M →+ NumberField.RingOfIntegers K

Given f : M →+ K such that ∀ x, IsIntegral ℤ (f x), the corresponding function M →+ 𝓞 K.

Equations

• NumberField.RingOfIntegers.restrict_addMonoidHom f h = { toFun := NumberField.RingOfIntegers.restrict (⇑f) h, map_zero' := ⋯, map_add' := ⋯ }

def NumberField.RingOfIntegers.restrict_monoidHom {K : Type u_1} [Field K] {M : Type u_3} [MulOneClass M] (f : M →* K) (h : ∀ (x : M), IsIntegral ℤ (f x)) : M →* NumberField.RingOfIntegers K

Given f : M →* K such that ∀ x, IsIntegral ℤ (f x), the corresponding function M →* 𝓞 K.

Equations

• NumberField.RingOfIntegers.restrict_monoidHom f h = { toFun := NumberField.RingOfIntegers.restrict (⇑f) h, map_one' := ⋯, map_mul' := ⋯ }

instance NumberField.RingOfIntegers.instIsScalarTower_1 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : IsScalarTower (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) L

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instIsIntegralClosure (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : IsIntegralClosure (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers K) L

Equations

• ⋯ = ⋯

noncomputable def NumberField.RingOfIntegers.algEquiv (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] (R : Type u_6) [CommRing R] [Algebra (NumberField.RingOfIntegers K) R] [Algebra R L] [IsScalarTower (NumberField.RingOfIntegers K) R L] [IsIntegralClosure R (NumberField.RingOfIntegers K) L] : NumberField.RingOfIntegers L ≃ₐ[NumberField.RingOfIntegers K] R

The ring of integers of L is isomorphic to any integral closure of 𝓞 K in L

Equations

• NumberField.RingOfIntegers.algEquiv K L R = (IsIntegralClosure.equiv (NumberField.RingOfIntegers K) R L (NumberField.RingOfIntegers L)).symm

instance NumberField.RingOfIntegers.extension_algebra_isIntegral (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : Algebra.IsIntegral (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

Any extension between ring of integers is integral.

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.extension_isNoetherian (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] : IsNoetherian (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

Any extension between ring of integers of number fields is noetherian.

Equations

• ⋯ = ⋯

theorem NumberField.RingOfIntegers.ker_algebraMap_eq_bot (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : RingHom.ker (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) = ⊥

The kernel of the algebraMap between ring of integers is ⊥.

theorem NumberField.RingOfIntegers.algebraMap.injective (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : Function.Injective ⇑(algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L))

The algebraMap between ring of integers is injective.

instance NumberField.RingOfIntegers.instNoZeroSMulDivisors_1 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : NoZeroSMulDivisors (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

Equations

• ⋯ = ⋯

instance NumberField.RingOfIntegers.instNoZeroSMulDivisors_2 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] : NoZeroSMulDivisors (NumberField.RingOfIntegers K) L

Equations

• ⋯ = ⋯

noncomputable def NumberField.integralBasis (K : Type u_1) [Field K] [NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ (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] [NumberField K] (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) : (NumberField.integralBasis K) i = (algebraMap (NumberField.RingOfIntegers K) K) ((NumberField.RingOfIntegers.basis K) i)

@[simp]

theorem NumberField.integralBasis_repr_apply (K : Type u_1) [Field K] [NumberField K] (x : NumberField.RingOfIntegers K) (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) : ((NumberField.integralBasis K).repr ((algebraMap (NumberField.RingOfIntegers K) K) x)) i = (algebraMap ℤ ℚ) (((NumberField.RingOfIntegers.basis K).repr x) i)

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

theorem NumberField.RingOfIntegers.rank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℤ (NumberField.RingOfIntegers K) = Module.finrank ℚ K

instance Rat.numberField : NumberField ℚ

Equations

• Rat.numberField = ⋯

noncomputable def Rat.ringOfIntegersEquiv : NumberField.RingOfIntegers ℚ ≃+* ℤ

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

Equations

• Rat.ringOfIntegersEquiv = NumberField.RingOfIntegers.equiv ℤ

instance AdjoinRoot.instNumberFieldRat {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

• ⋯ = ⋯