mathlib3documentation

number_theory.number_field.embeddings

Embeddings of number fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines the embeddings of a number field into an algebraic closed field.

Main Results #

• number_field.embeddings.range_eval_eq_root_set_minpoly: 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 ℚ.
• number_field.embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.

Tags #

number field, embeddings, places, infinite places

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

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

@[protected, instance]
theorem number_field.embeddings.range_eval_eq_root_set_minpoly (K : Type u_1) (A : Type u_2) [field K] [number_field K] [field A] [ A] (x : K) :
set.range (λ (φ : K →+* A), φ x) = 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 ℚ.

theorem number_field.embeddings.coeff_bdd_of_norm_le {K : Type u_1} [field K] [number_field K] {A : Type u_2} [normed_field A] [ A] {B : } {x : K} (h : (φ : K →+* A), φ x B) (i : ) :
theorem number_field.embeddings.finite_of_norm_le (K : Type u_1) [field K] [number_field K] (A : Type u_2) [normed_field A] [ A] (B : ) :
{x : K | (φ : K →+* A), φ x B}.finite

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

theorem number_field.embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [field K] [number_field K] (A : Type u_2) [normed_field A] [ A] {x : K} (hxi : x) (hx : (φ : K →+* A), φ x = 1) :
(n : ) (hn : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

def number_field.place {K : Type u_1} [field K] {A : Type u_2} [nontrivial A] (φ : K →+* A) :

An embedding into a normed division ring defines a place of K

Equations
@[simp]
theorem number_field.place_apply {K : Type u_1} [field K] {A : Type u_2} [nontrivial A] (φ : K →+* A) (x : K) :
x = φ x
@[reducible]

The conjugate of a complex embedding as a complex embedding.

Equations
@[simp]
theorem number_field.complex_embedding.conjugate_coe_eq {K : Type u_1} [field K] (φ : K →+* ) (x : K) :
= (φ x)
@[reducible]
def number_field.complex_embedding.is_real {K : Type u_1} [field K] (φ : K →+* ) :
Prop

A embedding into ℂ is real if it is fixed by complex conjugation.

Equations

A real embedding as a ring homomorphism from K to ℝ .

Equations
@[simp]
theorem number_field.complex_embedding.is_real.coe_embedding_apply {K : Type u_1} [field K] {φ : K →+* } (x : K) :
((hφ.embedding) x) = φ x
def number_field.infinite_place (K : Type u_1) [field K] :
Type u_1

An infinite place of a number field K is a place associated to a complex embedding.

Equations
Instances for number_field.infinite_place
@[protected, instance]
noncomputable def number_field.infinite_place.mk {K : Type u_1} [field K] (φ : K →+* ) :

Return the infinite place defined by a complex embedding φ.

Equations
@[protected, instance]
def number_field.infinite_place.has_coe_to_fun {K : Type u_1} [field K] :
(λ (_x : , K )
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem number_field.infinite_place.coe_mk {K : Type u_1} [field K] (φ : K →+* ) :
theorem number_field.infinite_place.apply {K : Type u_1} [field K] (φ : K →+* ) (x : K) :
noncomputable def number_field.infinite_place.embedding {K : Type u_1} [field K]  :

For an infinite place w, return an embedding φ such that w = infinite_place φ .

Equations
@[simp]
@[simp]
theorem number_field.infinite_place.eq_iff_eq {K : Type u_1} [field K] (x : K) (r : ) :
( (w : , w x = r) (φ : K →+* ), φ x = r
theorem number_field.infinite_place.le_iff_le {K : Type u_1} [field K] (x : K) (r : ) :
( (w : , w x r) (φ : K →+* ), φ x r
theorem number_field.infinite_place.pos_iff {K : Type u_1} [field K] {x : K} :
0 < w x x 0
@[simp]
theorem number_field.infinite_place.mk_conjugate_eq {K : Type u_1} [field K] (φ : K →+* ) :
@[simp]
theorem number_field.infinite_place.mk_eq_iff {K : Type u_1} [field K] {φ ψ : K →+* } :
def number_field.infinite_place.is_real {K : Type u_1} [field K]  :
Prop

An infinite place is real if it is defined by a real embedding.

Equations

An infinite place is complex if it is defined by a complex (ie. not real) embedding.

Equations
@[simp]
noncomputable def number_field.infinite_place.is_real.embedding {K : Type u_1} [field K] (hw : w.is_real) :

For w a real infinite place, return the corresponding embedding as a morphism K →+* ℝ.

Equations
@[simp]
theorem number_field.infinite_place.is_real.place_embedding_apply {K : Type u_1} [field K] (hw : w.is_real) (x : K) :
x = w x
@[simp]
theorem number_field.infinite_place.is_real.abs_embedding_apply {K : Type u_1} [field K] (hw : w.is_real) (x : K) :
|(hw.embedding) x| = w x
noncomputable def number_field.infinite_place.mk_real (K : Type u_1) [field K] :
{w // w.is_real}

The map from real embeddings to real infinite places as an equiv

Equations
noncomputable def number_field.infinite_place.mk_complex (K : Type u_1) [field K] :
{w // w.is_complex}

The map from nonreal embeddings to complex infinite places

Equations
theorem number_field.infinite_place.mk_complex_embedding (K : Type u_1) [field K] (φ : {φ // ) :
@[simp]
theorem number_field.infinite_place.mk_real_coe (K : Type u_1) [field K] (φ : {φ // ) :
@[simp]
theorem number_field.infinite_place.mk_complex_coe (K : Type u_1) [field K] (φ : {φ // ) :
@[simp]
theorem number_field.infinite_place.mk_real.apply (K : Type u_1) [field K] (φ : {φ // ) (x : K) :
@[simp]
theorem number_field.infinite_place.mk_complex.apply (K : Type u_1) [field K] (φ : {φ // ) (x : K) :
@[protected, instance]
Equations
theorem number_field.infinite_place.prod_eq_abs_norm (K : Type u_1) [field K] [number_field K] (x : K) :
finset.univ.prod (λ (w : , (w x) (w x ^ 2)) = |( x)|

The infinite part of the product formula : for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where ‖·‖_w is the normalized absolute value for w.