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

def NumberField.canonicalEmbedding (K : Type u_1) [Field K] : K →+* (K →+* ℂ) → ℂ

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

theorem NumberField.canonicalEmbedding_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective ↑(NumberField.canonicalEmbedding K)

@[simp]

theorem NumberField.canonicalEmbedding.apply_at {K : Type u_1} [Field K] (φ : K →+* ℂ) (x : K) : ↑(NumberField.canonicalEmbedding K) x φ = ↑φ x

theorem NumberField.canonicalEmbedding.conj_apply {K : Type u_1} [Field K] {x : (K →+* ℂ) → ℂ} (φ : K →+* ℂ) (hx : x ∈ Submodule.span ℝ (Set.range ↑(NumberField.canonicalEmbedding K))) : ↑(starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)

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} [Field K] [NumberField K] (x : K) : ‖↑(NumberField.canonicalEmbedding K) x‖₊ = Finset.sup Finset.univ fun φ => ‖↑φ x‖₊

theorem NumberField.canonicalEmbedding.norm_le_iff {K : Type u_1} [Field K] [NumberField K] (x : K) (r : ℝ) : ‖↑(NumberField.canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r

def NumberField.canonicalEmbedding.integerLattice (K : Type u_1) [Field K] : Subring ((K →+* ℂ) → ℂ)

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

theorem NumberField.canonicalEmbedding.integerLattice.inter_ball_finite (K : Type u_1) [Field K] [NumberField K] (r : ℝ) : Set.Finite (↑(NumberField.canonicalEmbedding.integerLattice K) ∩ Metric.closedBall 0 r)

noncomputable def NumberField.canonicalEmbedding.latticeBasis (K : Type u_1) [Field K] [NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) ℂ ((K →+* ℂ) → ℂ)

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

@[simp]

theorem NumberField.canonicalEmbedding.latticeBasis_apply (K : Type u_1) [Field K] [NumberField K] (i : Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) : ↑(NumberField.canonicalEmbedding.latticeBasis K) i = ↑(NumberField.canonicalEmbedding K) (↑(NumberField.integralBasis K) i)

theorem NumberField.canonicalEmbedding.mem_span_latticeBasis (K : Type u_1) [Field K] [NumberField K] (x : (K →+* ℂ) → ℂ) : x ∈ Submodule.span ℤ (Set.range ↑(NumberField.canonicalEmbedding.latticeBasis K)) ↔ x ∈ ↑(NumberField.canonicalEmbedding K) '' ↑(NumberField.ringOfIntegers K)

noncomputable def NumberField.mixedEmbedding (K : Type u_1) [Field K] : K →+* ({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ)

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

instance NumberField.mixedEmbedding.instNontrivialProdForAllSubtypeInfinitePlaceIsRealRealForAllIsComplexComplex (K : Type u_1) [Field K] [NumberField K] : Nontrivial (({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ))

theorem NumberField.mixedEmbedding.finrank (K : Type u_1) [Field K] [NumberField K] : FiniteDimensional.finrank ℝ (({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ)) = FiniteDimensional.finrank ℚ K

theorem NumberField.mixedEmbedding_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective ↑(NumberField.mixedEmbedding K)

noncomputable def NumberField.mixedEmbedding.commMap (K : Type u_1) [Field K] : ((K →+* ℂ) → ℂ) →ₗ[ℝ] ({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ)

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

theorem NumberField.mixedEmbedding.commMap_apply_of_isReal (K : Type u_1) [Field K] (x : (K →+* ℂ) → ℂ) {w : NumberField.InfinitePlace K} (hw : NumberField.InfinitePlace.IsReal w) : Prod.fst (↑(NumberField.mixedEmbedding.commMap K) x) { val := w, property := hw } = (x (NumberField.InfinitePlace.embedding w)).re

theorem NumberField.mixedEmbedding.commMap_apply_of_isComplex (K : Type u_1) [Field K] (x : (K →+* ℂ) → ℂ) {w : NumberField.InfinitePlace K} (hw : NumberField.InfinitePlace.IsComplex w) : Prod.snd (↑(NumberField.mixedEmbedding.commMap K) x) { val := w, property := hw } = x (NumberField.InfinitePlace.embedding w)

@[simp]

theorem NumberField.mixedEmbedding.commMap_canonical_eq_mixed (K : Type u_1) [Field K] (x : K) : ↑(NumberField.mixedEmbedding.commMap K) (↑(NumberField.canonicalEmbedding K) x) = ↑(NumberField.mixedEmbedding K) x

theorem NumberField.mixedEmbedding.disjoint_span_commMap_ker (K : Type u_1) [Field K] [NumberField K] : Disjoint (Submodule.span ℝ (Set.range ↑(NumberField.canonicalEmbedding.latticeBasis K))) (LinearMap.ker (NumberField.mixedEmbedding.commMap K))

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) [Field K] [NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) ℝ (({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ))

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

@[simp]

theorem NumberField.mixedEmbedding.latticeBasis_apply (K : Type u_1) [Field K] [NumberField K] (i : Module.Free.ChooseBasisIndex ℤ { x // x ∈ NumberField.ringOfIntegers K }) : ↑(NumberField.mixedEmbedding.latticeBasis K) i = ↑(NumberField.mixedEmbedding K) (↑(NumberField.integralBasis K) i)

theorem NumberField.mixedEmbedding.mem_span_latticeBasis (K : Type u_1) [Field K] [NumberField K] (x : ({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ)) : x ∈ Submodule.span ℤ (Set.range ↑(NumberField.mixedEmbedding.latticeBasis K)) ↔ x ∈ ↑(NumberField.mixedEmbedding K) '' ↑(NumberField.ringOfIntegers K)

@[inline, reducible]

abbrev NumberField.mixedEmbedding.convexBodyLt (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) : Set (({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ))

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

theorem NumberField.mixedEmbedding.convexBodyLt_mem (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) {x : K} : ↑(NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodyLt K f ↔ ∀ (w : NumberField.InfinitePlace K), ↑w x < ↑(f w)

theorem NumberField.mixedEmbedding.convexBodyLt_symmetric (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (x : ({ w // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w // NumberField.InfinitePlace.IsComplex w } → ℂ)) (hx : x ∈ NumberField.mixedEmbedding.convexBodyLt K f) : -x ∈ NumberField.mixedEmbedding.convexBodyLt K f

theorem NumberField.mixedEmbedding.convexBodyLt_convex (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) : Convex ℝ (NumberField.mixedEmbedding.convexBodyLt K f)

@[inline, reducible]

noncomputable abbrev NumberField.mixedEmbedding.convexBodyLtFactor (K : Type u_1) [Field K] [NumberField K] : ENNReal

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

theorem NumberField.mixedEmbedding.convexBodyLtFactor_pos (K : Type u_1) [Field K] [NumberField K] : 0 < NumberField.mixedEmbedding.convexBodyLtFactor K

theorem NumberField.mixedEmbedding.convexBodyLtFactor_lt_top (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.convexBodyLtFactor K < ⊤

theorem NumberField.mixedEmbedding.convexBodyLt_volume (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) [NumberField K] : ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLt K f) = NumberField.mixedEmbedding.convexBodyLtFactor K * ↑(Finset.prod Finset.univ fun w => f w ^ NumberField.InfinitePlace.mult 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) [Field K] {f : NumberField.InfinitePlace K → NNReal} [NumberField K] {w₁ : NumberField.InfinitePlace K} (B : NNReal) (hf : ∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → f w ≠ 0) : ∃ g, (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ (Finset.prod Finset.univ fun w => g w ^ NumberField.InfinitePlace.mult 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) [Field K] [NumberField K] : ENNReal

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

theorem NumberField.mixedEmbedding.minkowskiBound_lt_top (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.minkowskiBound K < ⊤

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt (K : Type u_1) [Field K] [NumberField K] {f : NumberField.InfinitePlace K → NNReal} (h : NumberField.mixedEmbedding.minkowskiBound K < ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLt K f)) : ∃ a, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), ↑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.