# Documentation

Mathlib.NumberTheory.NumberField.Embeddings

# Embeddings of number fields #

This file defines the embeddings of a number field into an algebraic closed field.

## Main Definitions and Results #

• NumberField.Embeddings.range_eval_eq_rootSet_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 ℚ.
• NumberField.Embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.
• NumberField.InfinitePlace: the type of infinite places of a number field K.
• NumberField.InfinitePlace.mk_eq_iff: two complex embeddings define the same infinite place iff they are equal or complex conjugates.
• NumberField.InfinitePlace.prod_eq_abs_norm: the infinite part of the product formula, that is for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where the product is over the infinite place w and ‖·‖_w is the normalized absolute value for w.

## Tags #

number field, embeddings, places, infinite places

theorem NumberField.Embeddings.card (K : Type u_1) [] [] (A : Type u_2) [] [] [] :

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

theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly (K : Type u_1) (A : Type u_2) [] [] [] [] [] (x : K) :
(Set.range fun φ => φ x) =

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 NumberField.Embeddings.coeff_bdd_of_norm_le {K : Type u_1} [] [] {A : Type u_2} [] [] [] {B : } {x : K} (h : ∀ (φ : K →+* A), φ x B) (i : ) :
theorem NumberField.Embeddings.finite_of_norm_le (K : Type u_1) [] [] (A : Type u_2) [] [] [] (B : ) :
Set.Finite {x | ∀ (φ : K →+* A), φ x B}

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 NumberField.Embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [] [] (A : Type u_2) [] [] [] {x : K} (hxi : ) (hx : ∀ (φ : K →+* A), φ x = 1) :
n x, x ^ n = 1

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

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

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

Instances For
@[simp]
theorem NumberField.place_apply {K : Type u_1} [] {A : Type u_2} [] (φ : K →+* A) (x : K) :
↑() x = φ x
@[reducible]

The conjugate of a complex embedding as a complex embedding.

Instances For
@[simp]
theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [] (φ : K →+* ) (x : K) :
= ↑(starRingEnd ((fun x => ) x)) (φ x)
@[reducible]

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

Instances For

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

Instances For
@[simp]
theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply {K : Type u_1} [] {φ : K →+* } (x : K) :
= φ x
def NumberField.InfinitePlace (K : Type u_1) [] :
Type u_1

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

Instances For
instance instNonemptyInfinitePlace (K : Type u_1) [] [] :
noncomputable def NumberField.InfinitePlace.mk {K : Type u_1} [] (φ : K →+* ) :

Return the infinite place defined by a complex embedding φ.

Instances For
@[simp]
theorem NumberField.InfinitePlace.apply {K : Type u_1} [] (φ : K →+* ) (x : K) :
= Complex.abs (φ x)
noncomputable def NumberField.InfinitePlace.embedding {K : Type u_1} [] (w : ) :

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

Instances For
@[simp]
theorem NumberField.InfinitePlace.mk_embedding {K : Type u_1} [] (w : ) :
@[simp]
theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_1} [] (w : ) (x : K) :
= w x
theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_1} [] (x : K) (r : ) :
(∀ (w : ), w x = r) ∀ (φ : K →+* ), φ x = r
theorem NumberField.InfinitePlace.le_iff_le {K : Type u_1} [] (x : K) (r : ) :
(∀ (w : ), w x r) ∀ (φ : K →+* ), φ x r
theorem NumberField.InfinitePlace.pos_iff {K : Type u_1} [] {w : } {x : K} :
0 < w x x 0
@[simp]
theorem NumberField.InfinitePlace.mk_eq_iff {K : Type u_1} [] {φ : K →+* } {ψ : K →+* } :
def NumberField.InfinitePlace.IsReal {K : Type u_1} [] (w : ) :

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

Instances For

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

Instances For
@[simp]
noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_1} [] {w : } (hw : ) :

The real embedding associated to a real infinite place.

Instances For
@[simp]
theorem NumberField.InfinitePlace.embedding_of_isReal_apply {K : Type u_1} [] {w : } (hw : ) (x : K) :
@[simp]
noncomputable def NumberField.InfinitePlace.mult {K : Type u_1} [] (w : ) :

The multiplicity of an infinite place, that is the number of distinct complex embeddings that define it, see card_filter_mk_eq.

Instances For
theorem NumberField.InfinitePlace.card_filter_mk_eq {K : Type u_1} [] [] (w : ) :
Finset.card (Finset.filter (fun φ => ) Finset.univ) =
noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_1} [] :

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

Instances For
noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_1} [] :

The map from nonreal embeddings to complex infinite places

Instances For
@[simp]
theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_1} [] (φ : ) :
↑(NumberField.InfinitePlace.mkReal φ) =
@[simp]
theorem NumberField.InfinitePlace.mkComplex_coe {K : Type u_1} [] (φ : ) :
theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_1} [] [] (x : K) :
(Finset.prod Finset.univ fun w => ) = |↑() 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.