mathlib3 documentation

number_theory.number_field.basic

Number fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines a number field and the ring of integers corresponding to it.

Main definitions #

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

source
@[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
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
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
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
theorem number_field.ring_of_integers.map_mem {K : Type u_1} [field K] {F : Type u_2} {L : Type u_3} [field L] [char_zero K] [char_zero L] [alg_hom_class F ℚ K L] (f : F) (x : ↥(number_field.ring_of_integers K)) :
⇑f ↑x ∈ number_field.ring_of_integers L
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
source
@[protected, instance]
def number_field.ring_of_integers.char_zero (K : Type u_1) [field K] [nf : 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] [nf : 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] [nf : 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] [nf : number_field K] :
is_dedekind_domain ↥(number_field.ring_of_integers K)
source
@[protected, instance]
def number_field.ring_of_integers.module.free (K : Type u_1) [field K] [nf : number_field K] :
module.free ℤ ↥(number_field.ring_of_integers K)
source
@[protected, instance]
def number_field.ring_of_integers.is_localization (K : Type u_1) [field K] [nf : number_field K] :
is_localization (algebra.algebra_map_submonoid ↥(number_field.ring_of_integers K) (non_zero_divisors ℤ)) K
source
noncomputable def number_field.ring_of_integers.basis (K : Type u_1) [field K] [nf : number_field K] :
basis (module.free.choose_basis_index ℤ ↥(number_field.ring_of_integers K)) ℤ ↥(number_field.ring_of_integers K)

A ℤ-basis of the ring of integers of K.

Equations
source
noncomputable def number_field.integral_basis (K : Type u_1) [field K] [nf : number_field K] :
basis (module.free.choose_basis_index ℤ ↥(number_field.ring_of_integers K)) ℚ K

A basis of K over ℚ that is also a basis of 𝓞 K over ℤ.

Equations
source
@[simp]
theorem number_field.integral_basis_apply (K : Type u_1) [field K] [nf : number_field K] (i : module.free.choose_basis_index ℤ ↥(number_field.ring_of_integers K)) :
⇑(number_field.integral_basis K) i = ⇑(algebra_map ↥(number_field.ring_of_integers K) K) (⇑(number_field.ring_of_integers.basis K) i)
source
theorem number_field.ring_of_integers.rank (K : Type u_1) [field K] [nf : number_field K] :
finite_dimensional.finrank ℤ ↥(number_field.ring_of_integers K) = finite_dimensional.finrank ℚ 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
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.