Embeddings of number fields #
This file defines the embeddings of a number field and, in particular, the embeddings into the field of complex numbers.
Main Definitions and Results #
NumberField.Embeddings.range_eval_eq_rootSet_minpoly
: letx ∈ K
withK
a number field and letA
be an algebraically closed field of char. 0. Then the images ofx
under the embeddings ofK
inA
are exactly the roots inA
of the minimal polynomial ofx
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.
Tags #
number field, embeddings
There are finitely many embeddings of a number field.
Equations
The number of embeddings of a number field is equal to its finrank.
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 ℚ
.
Let B
be a real number. The set of algebraic integers in K
whose conjugates are all
smaller in norm than B
is finite.
An algebraic integer whose conjugates are all of norm one is a root of unity.
An embedding into a normed division ring defines a place of K
Equations
Instances For
A (random) lift of the complex embedding φ : k →+* ℂ
to an extension K
of k
.
Equations
Instances For
An embedding into ℂ
is real if it is fixed by complex conjugation.
Equations
Instances For
If L/K
and ψ : K →+* ℂ
, then the type of ComplexEmbedding.Extension L ψ
consists of all
φ : L →+* ℂ
such that φ.comp (algebraMap K L) = ψ
.
Equations
Instances For
If L/K
and φ : L →+* ℂ
, then IsMixed K φ
if the image of φ
is complex while the image
of φ
restricted to K
is real.
This is the complex embedding analogue of InfinitePlace.IsRamified K w
, where
w : InfinitePlace L
. It is not the same concept because conjugation of φ
in this case
leads to two distinct mixed embeddings but only a single ramified place w
, leading to a
two-to-one isomorphism between them.
Equations
Instances For
If L/K
and φ : L →+* ℂ
, then IsMixed K φ
if φ
is not mixed in K
, i.e., φ
is real
if and only if it's restriction to K
is.
This is the complex embedding analogue of InfinitePlace.IsUnramified K w
, where
w : InfinitePlace L
. In this case there is an isomorphism between unmixed embeddings and
unramified infinite places.