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

• to_charZero : CharZero K
• to_finiteDimensional : FiniteDimensional ℚ K

theorem NumberField.to_charZero {K : Type u_1} [Field K] [self : NumberField K] : CharZero K

theorem NumberField.to_finiteDimensional {K : Type u_1} [Field K] [self : NumberField K] : 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] [nf : NumberField K] : Algebra.IsAlgebraic ℚ K

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

Equations

• ⋯ = ⋯

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] [nf : 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 : NumberField.RingOfIntegers K} {y : NumberField.RingOfIntegers K} (h : ↑x = ↑y) : x = y

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

theorem NumberField.RingOfIntegers.eq_iff {K : Type u_1} [Field K] {x : NumberField.RingOfIntegers K} {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 : K) (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 : K) (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 : K) (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 : K) (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, ⋯⟩

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

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

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.

@[simp]

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.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] [nf : NumberField K] : IsNoetherian ℤ (NumberField.RingOfIntegers K)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable def NumberField.RingOfIntegers.basis (K : Type u_1) [Field K] [nf : 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' := ⋯ }

noncomputable def NumberField.integralBasis (K : Type u_1) [Field K] [nf : 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] [nf : 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] [nf : 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] [nf : 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] [nf : NumberField K] : FiniteDimensional.finrank ℤ (NumberField.RingOfIntegers K) = FiniteDimensional.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

• ⋯ = ⋯