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öhlich, Algebraic Number Theory][cassels1967algebraic]
• [P. Samuel, Algebraic Theory of Numbers][samuel1967]

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 ℚ.

• 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

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

instance NumberField.of_subfield {K : Type u_1} [Field K] [NumberField K] (E : Subfield K) : NumberField ↥E

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.

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.

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

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

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

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

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

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

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

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

@[reducible, inline]

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

The canonical coercion from 𝓞 K to K.

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

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

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

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

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

theorem NumberField.RingOfIntegers.eq_iff {K : Type u_1} [Field K] {x y : 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 (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) : RingOfIntegers K →+* RingOfIntegers L

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

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) : RingOfIntegers K ≃+* RingOfIntegers L

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

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

Given an algebra structure between two fields, this instance creates an algebra structure between their two rings of integers.

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) : RingOfIntegers K →ₐ[RingOfIntegers k] RingOfIntegers L

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

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) : RingOfIntegers K ≃ₐ[RingOfIntegers k] RingOfIntegers L

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

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 (RingOfIntegers k) (RingOfIntegers K) (RingOfIntegers L)

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

The canonical map from 𝓞 K to K is injective.

This is a convenient abbreviation for FaithfulSMul.algebraMap_injective.

theorem NumberField.RingOfIntegers.coe_eq_zero_iff {K : Type u_1} [Field K] {x : RingOfIntegers K} : (algebraMap (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 FaithfulSMul.algebraMap_injective.

theorem NumberField.RingOfIntegers.coe_ne_zero_iff {K : Type u_1} [Field K] {x : RingOfIntegers K} : (algebraMap (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 FaithfulSMul.algebraMap_injective.

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

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

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

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

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

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

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

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

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

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

theorem NumberField.RingOfIntegers.not_isField (K : Type u_1) [Field K] [NumberField K] : ¬IsField (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 (RingOfIntegers K)

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

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

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

A ℤ-basis of the ring of integers of 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) : RingOfIntegers K

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

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 →+ RingOfIntegers K

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

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 →* RingOfIntegers K

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

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

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

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 (RingOfIntegers K) R] [Algebra R L] [IsScalarTower (RingOfIntegers K) R L] [IsIntegralClosure R (RingOfIntegers K) L] : RingOfIntegers L ≃ₐ[RingOfIntegers K] R

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

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

Any extension between ring of integers is integral.

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 (RingOfIntegers K) (RingOfIntegers L)

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

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 (RingOfIntegers K) (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 (RingOfIntegers K) (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 (RingOfIntegers K) (RingOfIntegers L)

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

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

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

@[simp]

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

@[simp]

theorem NumberField.integralBasis_repr_apply (K : Type u_1) [Field K] [NumberField K] (x : RingOfIntegers K) (i : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) : ((integralBasis K).repr ((algebraMap (RingOfIntegers K) K) x)) i = (algebraMap ℤ ℚ) (((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 ⇑(integralBasis K)) ↔ x ∈ (algebraMap (RingOfIntegers K) K).range

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

instance Rat.numberField : NumberField ℚ

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

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

@[simp]

theorem Rat.coe_ringOfIntegersEquiv (z : NumberField.RingOfIntegers ℚ) : ↑(ringOfIntegersEquiv z) = (algebraMap (NumberField.RingOfIntegers ℚ) ℚ) z

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.