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) [] :

A number field is a field which has characteristic zero and is finite dimensional over β.

• to_charZero :
• to_finiteDimensional :
Instances
theorem NumberField.to_charZero {K : Type u_1} [] [self : ] :
theorem NumberField.to_finiteDimensional {K : Type u_1} [] [self : ] :
theorem Int.not_isField :

β€ with its usual ring structure is not a field.

theorem NumberField.isAlgebraic (K : Type u_1) [] [nf : ] :
instance NumberField.instFiniteDimensional (K : Type u_1) (L : Type u_2) [] [] [nf : ] [] [Algebra K L] :
Equations
• β― = β―
def NumberField.RingOfIntegers (K : Type u_1) [] :
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
Instances For

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
Instances For
Equations
Equations
• β― = β―
instance NumberField.RingOfIntegers.instCharZero (K : Type u_1) [] [nf : ] :
Equations
• β― = β―
Equations
Equations
• β― = β―
Equations
• β― = β―
instance NumberField.RingOfIntegers.instAlgebra_1 (K : Type u_1) [] {L : Type u_3} [Ring L] [Algebra K L] :
Equations
instance NumberField.RingOfIntegers.instIsScalarTower (K : Type u_1) [] {L : Type u_3} [Ring L] [Algebra K L] :
Equations
• β― = β―
@[reducible, inline]
abbrev NumberField.RingOfIntegers.val {K : Type u_1} [] (x : ) :
K

The canonical coercion from π K to K.

Equations
• βx = () x
Instances For

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} [] (x : ) :
βx = () x
theorem NumberField.RingOfIntegers.ext {K : Type u_1} [] {x : } {y : } (h : βx = βy) :
x = y
theorem NumberField.RingOfIntegers.ext_iff {K : Type u_1} [] {x : } {y : } :
x = y β βx = βy
theorem NumberField.RingOfIntegers.eq_iff {K : Type u_1} [] {x : } {y : } :
βx = βy β x = y
@[simp]
theorem NumberField.RingOfIntegers.map_mk {K : Type u_1} [] (x : K) (hx : ) :
() β¨x, hxβ© = x
theorem NumberField.RingOfIntegers.coe_mk {K : Type u_1} [] {x : K} (hx : ) :
ββ¨x, hxβ© = x
theorem NumberField.RingOfIntegers.mk_eq_mk {K : Type u_1} [] (x : K) (y : K) (hx : ) (hy : ) :
β¨x, hxβ© = β¨y, hyβ© β x = y
@[simp]
theorem NumberField.RingOfIntegers.mk_one {K : Type u_1} [] :
β¨1, β―β© = 1
@[simp]
theorem NumberField.RingOfIntegers.mk_zero {K : Type u_1} [] :
β¨0, β―β© = 0
@[simp]
theorem NumberField.RingOfIntegers.mk_add_mk {K : Type u_1} [] (x : K) (y : K) (hx : ) (hy : ) :
β¨x, hxβ© + β¨y, hyβ© = β¨x + y, β―β©
@[simp]
theorem NumberField.RingOfIntegers.mk_mul_mk {K : Type u_1} [] (x : K) (y : K) (hx : ) (hy : ) :
β¨x, hxβ© * β¨y, hyβ© = β¨x * y, β―β©
@[simp]
theorem NumberField.RingOfIntegers.mk_sub_mk {K : Type u_1} [] (x : K) (y : K) (hx : ) (hy : ) :
β¨x, hxβ© - β¨y, hyβ© = β¨x - y, β―β©
@[simp]
theorem NumberField.RingOfIntegers.neg_mk {K : Type u_1} [] (x : K) (hx : ) :
-β¨x, hxβ© = β¨-x, β―β©
instance NumberField.inst_ringOfIntegersAlgebra (K : Type u_1) (L : Type u_2) [] [] [Algebra K 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.

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} [] {x : } :
() 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} [] {x : } :
() 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.

Equations
• β― = β―
Equations
• β― = β―
Equations
• β― = β―
noncomputable def NumberField.RingOfIntegers.equiv {K : Type u_1} [] (R : Type u_3) [] [Algebra R K] [] :

The ring of integers of K are equivalent to any integral closure of β€ in K

Equations
• = .symm.toRingEquiv
Instances For
Equations
• β― = β―
Equations
• β― = β―
theorem NumberField.RingOfIntegers.not_isField (K : Type u_1) [] [nf : ] :

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

Equations
• β― = β―
instance NumberField.RingOfIntegers.instFreeInt (K : Type u_1) [] [nf : ] :
Equations
• β― = β―
Equations
• β― = β―
noncomputable def NumberField.RingOfIntegers.basis (K : Type u_1) [] [nf : ] :

A β€-basis of the ring of integers of K.

Equations
Instances For
def NumberField.RingOfIntegers.restrict {K : Type u_1} [] {M : Type u_3} (f : M β K) (h : β (x : M), IsIntegral β€ (f x)) (x : M) :

Given f : M β K such that β x, IsIntegral β€ (f x), the corresponding function M β π K.

Equations
• = β¨f x, β―β©
Instances For
def NumberField.RingOfIntegers.restrict_addMonoidHom {K : Type u_1} [] {M : Type u_3} [] (f : M β+ K) (h : β (x : M), IsIntegral β€ (f x)) :

Given f : M β+ K such that β x, IsIntegral β€ (f x), the corresponding function M β+ π K.

Equations
• = { toFun := , map_zero' := β―, map_add' := β― }
Instances For
def NumberField.RingOfIntegers.restrict_monoidHom {K : Type u_1} [] {M : Type u_3} [] (f : M β* K) (h : β (x : M), IsIntegral β€ (f x)) :

Given f : M β* K such that β x, IsIntegral β€ (f x), the corresponding function M β* π K.

Equations
• = { toFun := , map_one' := β―, map_mul' := β― }
Instances For
noncomputable def NumberField.integralBasis (K : Type u_1) [] [nf : ] :

A basis of K over β that is also a basis of π K over β€.

Equations
Instances For
@[simp]
theorem NumberField.integralBasis_apply (K : Type u_1) [] [nf : ] :
= () ()
@[simp]
theorem NumberField.integralBasis_repr_apply (K : Type u_1) [] [nf : ] (x : ) :
(.repr (() x)) i = () ((.repr x) i)
theorem NumberField.mem_span_integralBasis (K : Type u_1) [] [nf : ] {x : K} :
β x β ().range
theorem NumberField.RingOfIntegers.rank (K : Type u_1) [] [nf : ] :
instance Rat.numberField :
Equations
noncomputable def Rat.ringOfIntegersEquiv :

The ring of integers of β as a number field is just β€.

Equations
Instances For
instance AdjoinRoot.instNumberFieldRat {f : } [hf : Fact ()] :

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

Equations
• β― = β―