Canonical embedding of a number field #
The canonical embedding of a number field K
of degree n
is the ring homomorphism
K →+* ℂ^n
that sends x ∈ K
to (φ_₁(x),...,φ_n(x))
where the φ_i
's are the complex
embeddings of K
. Note that we do not choose an ordering of the embeddings, but instead map K
into the type (K →+* ℂ) → ℂ
of ℂ
-vectors indexed by the complex embeddings.
Main definitions and results #
NumberField.canonicalEmbedding
: the ring homomorphismK →+* ((K →+* ℂ) → ℂ)
defined by sendingx : K
to the vector(φ x)
indexed byφ : K →+* ℂ
.NumberField.canonicalEmbedding.integerLattice.inter_ball_finite
: the intersection of the image of the ring of integers by the canonical embedding and any ball centered at0
of finite radius is finite.NumberField.mixedEmbedding
: the ring homomorphism fromK
to the mixed spaceK →+* ({ w // IsReal w } → ℝ) × ({ w // IsComplex w } → ℂ)
that sendsx ∈ K
to(φ_w x)_w
whereφ_w
is the embedding associated to the infinite placew
. In particular, ifw
is real thenφ_w : K →+* ℝ
and, ifw
is complex,φ_w
is an arbitrary choice between the two complex embeddings defining the placew
.
Tags #
number field, infinite places
The canonical embedding of a number field K
of degree n
into ℂ^n
.
Equations
- NumberField.canonicalEmbedding K = Pi.ringHom fun (φ : K →+* ℂ) => φ
Instances For
The image of canonicalEmbedding
lives in the ℝ
-submodule of the x ∈ ((K →+* ℂ) → ℂ)
such
that conj x_φ = x_(conj φ)
for all ∀ φ : K →+* ℂ
.
The image of 𝓞 K
as a subring of ℂ^n
.
Equations
Instances For
A ℂ
-basis of ℂ^n
that is also a ℤ
-basis of the integerLattice
.
Equations
Instances For
The mixed space ℝ^r₁ × ℂ^r₂
with (r₁, r₂)
the signature of K
.
Equations
- NumberField.mixedEmbedding.mixedSpace K = (({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ))
Instances For
The mixed embedding of a number field K
into the mixed space of K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The linear map that makes canonicalEmbedding
and mixedEmbedding
commute, see
commMap_canonical_eq_mixed
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is a technical result to ensure that the image of the ℂ
-basis of ℂ^n
defined in
canonicalEmbedding.latticeBasis
is a ℝ
-basis of the mixed space ℝ^r₁ × ℂ^r₂
,
see mixedEmbedding.latticeBasis
.
The norm at the infinite place w
of an element of the mixed space. -
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff
.
The norm of x
is ∏ w, (normAtPlace x) ^ mult w
. It is defined such that the norm of
mixedEmbedding K a
for a : K
is equal to the absolute value of the norm of a
over ℚ
,
see norm_eq_norm
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type indexing the basis stdBasis
.
Equations
- NumberField.mixedEmbedding.index K = ({ w : NumberField.InfinitePlace K // w.IsReal } ⊕ { w : NumberField.InfinitePlace K // w.IsComplex } × Fin 2)
Instances For
The ℝ
-basis of the mixed space of K
formed by the vector equal to 1
at w
and 0
elsewhere for IsReal w
and by the couple of vectors equal to 1
(resp. I
) at w
and 0
elsewhere for IsComplex w
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Equiv
between index K
and K →+* ℂ
defined by sending a real infinite place w
to
the unique corresponding embedding w.embedding
, and the pair ⟨w, 0⟩
(resp. ⟨w, 1⟩
) for a
complex infinite place w
to w.embedding
(resp. conjugate w.embedding
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The matrix that gives the representation on stdBasis
of the image by commMap
of an
element x
of (K →+* ℂ) → ℂ
fixed by the map x_φ ↦ conj x_(conjugate φ)
,
see stdBasis_repr_eq_matrixToStdBasis_mul
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let x : (K →+* ℂ) → ℂ
such that x_φ = conj x_(conj φ)
for all φ : K →+* ℂ
, then the
representation of commMap K x
on stdBasis
is given (up to reindexing) by the product of
matrixToStdBasis
by x
.
The image of the ring of integers of K
in the mixed space.
Equations
- NumberField.mixedEmbedding.integerLattice K = LinearMap.range ((NumberField.mixedEmbedding K).comp (algebraMap (NumberField.RingOfIntegers K) K)).toIntAlgHom.toLinearMap
Instances For
A ℝ
-basis of the mixed space that is also a ℤ
-basis of the image of 𝓞 K
.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The generalized index of the lattice generated by I
in the lattice generated by
𝓞 K
is equal to the norm of the ideal I
. The result is stated in terms of base change
determinant and is the translation of NumberField.det_basisOfFractionalIdeal_eq_absNorm
in
the mixed space. This is useful, in particular, to prove that the family obtained from
the ℤ
-basis of I
is actually an ℝ
-basis of the mixed space, see
fractionalIdealLatticeBasis
.
A ℝ
-basis of the mixed space of K
that is also a ℤ
-basis of the image of the fractional
ideal I
.
Equations
- NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I = (let_fun this := ⋯; Basis.mk ⋯ ⋯).reindex (Fintype.equivOfCardEq ⋯)