Number fields #

This file defines a number field, the ring of integers corresponding to it and includes some basic facts about the embeddings into an algebraic closed field.

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.

Main Result #

eq_roots: let x ∈ K with K number field and let A be an algebraic closed field of char. 0, then the images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.

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 of this typeclass

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

number_field.ring_of_integers K = integral_closure ℤ K

Instances for ↥number_field.ring_of_integers

source

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

x ∈ number_field.ring_of_integers K ↔ is_integral ℤ x

source

theorem number_field.is_integral_of_mem_ring_of_integers {K : Type u_1} [field K] {x : K} (hx : x ∈ number_field.ring_of_integers K) :

is_integral ℤ ⟨x, hx⟩

source

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

algebra ↥(number_field.ring_of_integers K) ↥(number_field.ring_of_integers 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 : ↥(number_field.ring_of_integers 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 ↥(number_field.ring_of_integers K) K

source

@[protected, instance]

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

is_integral_closure ↥(number_field.ring_of_integers 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 ↥(number_field.ring_of_integers K)

source

theorem number_field.ring_of_integers.is_integral_coe {K : Type u_1} [field K] (x : ↥(number_field.ring_of_integers 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] :

↥(number_field.ring_of_integers 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 ↥(number_field.ring_of_integers 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 ↥(number_field.ring_of_integers K)

source

@[protected, instance]

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

is_noetherian ℤ ↥(number_field.ring_of_integers K)

source

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

¬is_field ↥(number_field.ring_of_integers 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 ↥(number_field.ring_of_integers K)

source

@[protected, instance]

def rat.number_field :

number_field ℚ

source

noncomputable def rat.ring_of_integers_equiv :

↥(number_field.ring_of_integers ℚ) ≃+* ℤ

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

Equations

rat.ring_of_integers_equiv = number_field.ring_of_integers.equiv ℤ

source

@[protected, instance]

def adjoin_root.number_field {f : polynomial ℚ} [hf : fact (irreducible f)] :

number_field (adjoin_root f)

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

source

@[protected, instance]

noncomputable def number_field.embeddings.ring_hom.fintype (K : Type u_1) [field K] [number_field K] (A : Type u_2) [field A] [char_zero A] :

fintype (K →+* A)

There are finitely many embeddings of a number field.

Equations

number_field.embeddings.ring_hom.fintype K A = fintype.of_equiv (K →ₐ[ℚ ] A) ring_hom.equiv_rat_alg_hom.symm

source

theorem number_field.embeddings.card (K : Type u_1) [field K] [number_field K] (A : Type u_2) [field A] [char_zero A] [is_alg_closed A] :

fintype.card (K →+* A) = finite_dimensional.finrank ℚ K

The number of embeddings of a number field is equal to its finrank.

source

theorem number_field.embeddings.range_eq_roots (F : Type u_1) (K : Type u_2) (A : Type u_3) [field F] [number_field F] [field K] [number_field K] [field A] [is_alg_closed A] [algebra F K] [algebra F A] (x : K) :

set.range (λ (ψ : K →ₐ[F] A), ⇑ψ x) = (minpoly F x).root_set A

Let A an algebraically closed field and let x ∈ K, with K a number field. For F, subfield of K, the images of x by the F-algebra morphisms from K to A are exactly the roots in A of the minimal polynomial of x over F

source

theorem number_field.embeddings.rat_range_eq_roots (K : Type u_1) (A : Type u_2) [field K] [number_field K] [field A] [char_zero A] [is_alg_closed A] (x : K) :

set.range (λ (φ : K →+* A), ⇑φ x) = (minpoly ℚ x).root_set A

Let A be an algebraically closed field and let x ∈ K, with K a number field. The images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ