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

source

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

Instances

source

theorem NumberField.to_charZero {K : Type u_1} :

∀ {inst : Field K} [self : NumberField K], CharZero K

source

theorem NumberField.to_finiteDimensional {K : Type u_1} :

∀ {inst : Field K} [self : NumberField K], FiniteDimensional ℚ K

source

theorem Int.not_isField :

¬IsField ℤ

ℤ with its usual ring structure is not a field.

source

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

Algebra.IsAlgebraic ℚ K

source

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

⋯ = ⋯

source

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)

Instances For

source

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.

Equations

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

source

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

CommRing (NumberField.RingOfIntegers K)

Equations

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

source

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

IsDomain (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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

CharZero (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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)

source

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

NoZeroSMulDivisors (NumberField.RingOfIntegers K) K

Equations

⋯ = ⋯

source

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

Nontrivial (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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)

source

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

⋯ = ⋯

source

@[reducible, inline]

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

The canonical coercion from 𝓞 K to K.

Equations

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

source

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 }

source

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

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

source

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

x = y ↔ ↑x = ↑y

source

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

x = y

source

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

↑x = ↑y ↔ x = y

source

@[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

source

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

↑⟨x, hx⟩ = x

source

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

source

@[simp]

theorem NumberField.RingOfIntegers.mk_one {K : Type u_1} [Field K] :

⟨1, ⋯⟩ = 1

source

@[simp]

theorem NumberField.RingOfIntegers.mk_zero {K : Type u_1} [Field K] :

⟨0, ⋯⟩ = 0

source

@[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, ⋯⟩

source

@[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, ⋯⟩

source

@[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, ⋯⟩

source

@[simp]

theorem NumberField.RingOfIntegers.neg_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure ℤ K) :

-⟨x, hx⟩ = ⟨-x, ⋯⟩

source

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' := ⋯ }

source

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) ⋯ ⋯

source

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

source

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' := ⋯ }

source

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) ⋯ ⋯

source

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

⋯ = ⋯

source

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.

source

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.

source

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.

source

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

IsIntegral ℤ ((algebraMap (NumberField.RingOfIntegers K) K) x)

source

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

IsIntegral ℤ x

source

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

IsFractionRing (NumberField.RingOfIntegers K) K

Equations

⋯ = ⋯

source

instance NumberField.RingOfIntegers.instIsIntegralClosureInt {K : Type u_1} [Field K] :

IsIntegralClosure (NumberField.RingOfIntegers K) ℤ K

Equations

⋯ = ⋯

source

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

IsIntegrallyClosed (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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

source

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

CharZero (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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

IsNoetherian ℤ (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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.

source

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

IsDedekindDomain (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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

Module.Free ℤ (NumberField.RingOfIntegers K)

Equations

⋯ = ⋯

source

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

IsLocalization (Algebra.algebraMapSubmonoid (NumberField.RingOfIntegers K) (nonZeroDivisors ℤ)) K

Equations

⋯ = ⋯

source

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)

source

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, ⋯⟩

source

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' := ⋯ }

source

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' := ⋯ }

source

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)

source

@[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)

source

@[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)

source

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

source

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

Module.finrank ℤ (NumberField.RingOfIntegers K) = Module.finrank ℚ K

source

instance Rat.numberField :

NumberField ℚ

Equations

Rat.numberField = ⋯

source

noncomputable def Rat.ringOfIntegersEquiv :

NumberField.RingOfIntegers ℚ ≃+* ℤ

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

Equations

Rat.ringOfIntegersEquiv = NumberField.RingOfIntegers.equiv ℤ

source

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

⋯ = ⋯

Documentation

Mathlib.NumberTheory.NumberField.Basic

Number fields #

Main definitions #

Implementation notes #

References #

Tags #