Number fields #

This file defines a number field and the ring of integers corresponding to it.

Main definitions #

number_field defines a number field as a field which has characteristic zero and is finite dimensional over ℚ.
ring_of_integers 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

source

@[class]

structure number_field (K : Type u_1) [field K] :

Prop

to_char_zero : char_zero K
to_finite_dimensional : finite_dimensional ℚ K

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

Instances

rat.rat.number_field

source

theorem int.not_is_field :

¬is_field ℤ

ℤ with its usual ring structure is not a field.

source

@[protected]

theorem number_field.is_algebraic (K : Type u_1) [field K] [nf : number_field K] :

algebra.is_algebraic ℚ K

source

def number_field.ring_of_integers (K : Type u_1) [field K] :

subalgebra ℤ K

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

Equations

𝓞 K = integral_closure ℤ K

source

theorem number_field.mem_ring_of_integers (K : Type u_1) [field K] (x : K) :

x ∈ 𝓞 K ↔ is_integral ℤ x

source

def number_field.ring_of_integers_algebra (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :

algebra ↥(𝓞 K) ↥(𝓞 L)

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

For now, this is not an instance by default as it creates an equal-but-not-defeq diamond with algebra.id when K = L. This is caused by x = ⟨x, x.prop⟩ not being defeq on subtypes. This will likely change in Lean 4.

Equations

number_field.ring_of_integers_algebra K L = {to_fun := λ (k : ↥(𝓞 K)), ⟨⇑(algebra_map K L) ↑k, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}.to_algebra

source

@[protected, instance]

def number_field.ring_of_integers.is_fraction_ring {K : Type u_1} [field K] [number_field K] :

is_fraction_ring ↥(𝓞 K) K

source

@[protected, instance]

def number_field.ring_of_integers.is_integral_closure {K : Type u_1} [field K] :

is_integral_closure ↥(𝓞 K) ℤ K

source

@[protected, instance]

def number_field.ring_of_integers.is_integrally_closed {K : Type u_1} [field K] [number_field K] :

is_integrally_closed ↥(𝓞 K)

source

theorem number_field.ring_of_integers.is_integral_coe {K : Type u_1} [field K] (x : ↥(𝓞 K)) :

is_integral ℤ ↑x

source

@[protected]

noncomputable def number_field.ring_of_integers.equiv {K : Type u_1} [field K] (R : Type u_2) [comm_ring R] [algebra R K] [is_integral_closure R ℤ K] :

↥(𝓞 K) ≃+* R

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

Equations

number_field.ring_of_integers.equiv R = (is_integral_closure.equiv ℤ R K ↥(𝓞 K)).symm.to_ring_equiv

source

@[protected, instance]

def number_field.ring_of_integers.char_zero (K : Type u_1) [field K] [number_field K] :

char_zero ↥(𝓞 K)

source

theorem number_field.ring_of_integers.not_is_field (K : Type u_1) [field K] [number_field K] :

¬is_field ↥(𝓞 K)

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

source

@[protected, instance]

def number_field.ring_of_integers.is_dedekind_domain (K : Type u_1) [field K] [number_field K] :

is_dedekind_domain ↥(𝓞 K)

source

@[protected, instance]

def rat.rat.number_field :

number_field ℚ

source

noncomputable def rat.ring_of_integers_equiv :

↥(𝓞 ℚ) ≃+* ℤ

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

Equations

rat.ring_of_integers_equiv = number_field.ring_of_integers.equiv ℤ