# Documentation

Mathlib.NumberTheory.NumberField.CanonicalEmbedding

# 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 #

• canonicalEmbedding: the ring homorphism K →+* ((K →+* ℂ) → ℂ) defined by sending x : K to the vector (φ x) indexed by φ : K →+* ℂ.

• canonicalEmbedding.integerLattice.inter_ball_finite: the intersection of the image of the ring of integers by the canonical embedding and any ball centered at 0 of finite radius is finite.

• mixedEmbedding: the ring homomorphism from K →+* ({ w // IsReal w } → ℝ) × ({ w // IsComplex w } → ℂ) that sends x ∈ K to (φ_w x)_w where φ_w is the embedding associated to the infinite place w. In particular, if w is real then φ_w : K →+* ℝ and, if w is complex, φ_w is an arbitrary choice between the two complex embeddings defining the place w.

• exists_ne_zero_mem_ringOfIntegers_lt: let f : InfinitePlace K → ℝ≥0, if the product ∏ w, f w is large enough, then there exists a nonzero algebraic integer a in K such that w a < f w for all infinite places w.

## Tags #

number field, infinite places

The canonical embedding of a number field K of degree n into ℂ^n.

Instances For
@[simp]
theorem NumberField.canonicalEmbedding.apply_at {K : Type u_1} [] (φ : K →+* ) (x : K) :
= φ x
theorem NumberField.canonicalEmbedding.conj_apply {K : Type u_1} [] {x : (K →+* ) → } (φ : K →+* ) (hx : ) :
↑() (x φ) =

The image of canonicalEmbedding lives in the ℝ-submodule of the x ∈ ((K →+* ℂ) → ℂ) such that conj x_φ = x_(conj φ) for all ∀ φ : K →+* ℂ.

theorem NumberField.canonicalEmbedding.nnnorm_eq {K : Type u_1} [] [] (x : K) :
= Finset.sup Finset.univ fun φ => φ x‖₊
theorem NumberField.canonicalEmbedding.norm_le_iff {K : Type u_1} [] [] (x : K) (r : ) :
∀ (φ : K →+* ), φ x r

The image of 𝓞 K as a subring of ℂ^n.

Instances For

A ℂ-basis of ℂ^n that is also a ℤ-basis of the integerLattice.

Instances For
noncomputable def NumberField.mixedEmbedding (K : Type u_1) [] :
K →+* () × ()

The mixed embedding of a number field K of signature (r₁, r₂) into ℝ^r₁ × ℂ^r₂.

Instances For
noncomputable def NumberField.mixedEmbedding.commMap (K : Type u_1) [] :
((K →+* ) → ) →ₗ[] () × ()

The linear map that makes canonicalEmbedding and mixedEmbedding commute, see commMap_canonical_eq_mixed.

Instances For
theorem NumberField.mixedEmbedding.commMap_apply_of_isReal (K : Type u_1) [] (x : (K →+* ) → ) {w : } (hw : ) :
Prod.fst () { val := w, property := hw } = ().re
theorem NumberField.mixedEmbedding.commMap_apply_of_isComplex (K : Type u_1) [] (x : (K →+* ) → ) {w : } :
Prod.snd () { val := w, property := hw } =

This is a technical result to ensure that the image of the ℂ-basis of ℂ^n defined in canonicalEmbedding.latticeBasis is a ℝ-basis of ℝ^r₁ × ℂ^r₂, see mixedEmbedding.latticeBasis.

noncomputable def NumberField.mixedEmbedding.latticeBasis (K : Type u_1) [] [] :
Basis (Module.Free.ChooseBasisIndex { x // }) (() × ())

A ℝ-basis of ℝ^r₁ × ℂ^r₂ that is also a ℤ-basis of the image of 𝓞 K.

Instances For
theorem NumberField.mixedEmbedding.mem_span_latticeBasis (K : Type u_1) [] [] (x : () × ()) :
@[inline, reducible]
abbrev NumberField.mixedEmbedding.convexBodyLt (K : Type u_1) [] (f : ) :
Set (() × ())

The convex body defined by f: the set of points x : E such that ‖x w‖ < f w for all infinite places w.

Instances For
theorem NumberField.mixedEmbedding.convexBodyLt_mem (K : Type u_1) [] (f : ) {x : K} :
∀ (w : ), w x < ↑(f w)
theorem NumberField.mixedEmbedding.convexBodyLt_symmetric (K : Type u_1) [] (f : ) (x : () × ()) (hx : ) :
@[inline, reducible]
noncomputable abbrev NumberField.mixedEmbedding.convexBodyLtFactor (K : Type u_1) [] [] :

The fudge factor that appears in the formula for the volume of convexBodyLt.

Instances For
theorem NumberField.mixedEmbedding.convexBodyLt_volume (K : Type u_1) [] (f : ) [] :
MeasureTheory.volume () = * ↑(Finset.prod Finset.univ fun w => )

The volume of (ConvexBodyLt K f) where convexBodyLt K f is the set of points x such that ‖x w‖ < f w for all infinite places w.

theorem NumberField.mixedEmbedding.adjust_f (K : Type u_1) [] {f : } [] {w₁ : } (B : NNReal) (hf : ∀ (w : ), w w₁f w 0) :
g, (∀ (w : ), w w₁g w = f w) (Finset.prod Finset.univ fun w => ) = B

This is a technical result: quite often, we want to impose conditions at all infinite places but one and choose the value at the remaining place so that we can apply exists_ne_zero_mem_ringOfIntegers_lt.

noncomputable def NumberField.mixedEmbedding.minkowskiBound (K : Type u_1) [] [] :

The bound that appears in Minkowski Convex Body theorem, see MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure.

Instances For
theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt (K : Type u_1) [] [] {f : } (h : < MeasureTheory.volume ()) :
a, a 0 ∀ (w : ), w a < ↑(f w)

Assume that f : InfinitePlace K → ℝ≥0 is such that minkowskiBound K < volume (convexBodyLt K f) where convexBodyLt K f is the set of points x such that ‖x w‖ < f w for all infinite places w (see convexBodyLt_volume for the computation of this volume), then there exists a nonzero algebraic integer a in 𝓞 K such that w a < f w for all infinite places w.