mathlib documentation

number_theory.number_field

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 #

Main Result #

Implementation notes #

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice.

References #

Tags #

number field, ring of integers

@[class]
structure number_field (K : Type u_1) [field K] :
Prop

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

Instances of this typeclass

with its usual ring structure is not a field.

@[protected]
theorem number_field.is_algebraic (K : Type u_1) [field K] [nf : number_field K] :
def number_field.ring_of_integers (K : Type u_1) [field K] :

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

Equations
Instances for number_field.ring_of_integers

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

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

Equations

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

@[protected, instance]

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

Equations
@[protected, instance]

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

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

There are finitely many embeddings of a number field.

Equations
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] :

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

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

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