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 homomorphism K →+* ((K →+* ℂ) → ℂ) defined by sending x : 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 at 0 of finite radius is finite.

• NumberField.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.

• NumberField.mixedEmbedding.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.

Equations

• NumberField.canonicalEmbedding K = Pi.ringHom fun (φ : K →+* ℂ) => φ

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 (φ : K →+* ℂ) => ‖φ 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.

Equations

• NumberField.canonicalEmbedding.integerLattice K = Subring.map (NumberField.canonicalEmbedding K) (RingHom.range (algebraMap (↥(NumberField.ringOfIntegers K)) K))

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 ℤ ↥(NumberField.ringOfIntegers K)) ℂ ((K →+* ℂ) → ℂ)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.canonicalEmbedding.latticeBasis_apply (K : Type u_1) [Field K] [NumberField K] (i : Module.Free.ChooseBasisIndex ℤ ↥(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 K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

theorem NumberField.mixedEmbedding.finrank (K : Type u_1) [Field K] [NumberField K] : FiniteDimensional.finrank ℝ (({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // 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 K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)

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.

theorem NumberField.mixedEmbedding.commMap_apply_of_isReal (K : Type u_1) [Field K] (x : (K →+* ℂ) → ℂ) {w : NumberField.InfinitePlace K} (hw : NumberField.InfinitePlace.IsReal w) : ((NumberField.mixedEmbedding.commMap K) x).1 { 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) : ((NumberField.mixedEmbedding.commMap K) x).2 { 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.

@[inline, reducible]

abbrev NumberField.mixedEmbedding.index (K : Type u_1) [Field K] : Type u_1

The type indexing the basis stdBasis.

Equations

• One or more equations did not get rendered due to their size.

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

The ℝ-basis of ({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ) 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.

@[simp]

theorem NumberField.mixedEmbedding.stdBasis_apply_ofIsReal {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) (w : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w }) : ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inl w) = x.1 w

@[simp]

theorem NumberField.mixedEmbedding.stdBasis_apply_ofIsComplex_fst {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) (w : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) : ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 0)) = (x.2 w).re

@[simp]

theorem NumberField.mixedEmbedding.stdBasis_apply_ofIsComplex_snd {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) (w : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) : ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 1)) = (x.2 w).im

theorem NumberField.mixedEmbedding.fundamentalDomain_stdBasis (K : Type u_1) [Field K] [NumberField K] : Zspan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K) = (Set.pi Set.univ fun (x : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w }) => Set.Ico 0 1) ×ˢ Set.pi Set.univ fun (x : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) => ⇑Complex.measurableEquivPi ⁻¹' Set.pi Set.univ fun (x : Fin 2) => Set.Ico 0 1

theorem NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis (K : Type u_1) [Field K] [NumberField K] : ↑↑MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K)) = 1

def NumberField.mixedEmbedding.indexEquiv (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.index K ≃ (K →+* ℂ)

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.

@[simp]

theorem NumberField.mixedEmbedding.indexEquiv_apply_ofIsReal {K : Type u_1} [Field K] [NumberField K] (w : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w }) : (NumberField.mixedEmbedding.indexEquiv K) (Sum.inl w) = NumberField.InfinitePlace.embedding ↑w

@[simp]

theorem NumberField.mixedEmbedding.indexEquiv_apply_ofIsComplex_fst {K : Type u_1} [Field K] [NumberField K] (w : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) : (NumberField.mixedEmbedding.indexEquiv K) (Sum.inr (w, 0)) = NumberField.InfinitePlace.embedding ↑w

@[simp]

theorem NumberField.mixedEmbedding.indexEquiv_apply_ofIsComplex_snd {K : Type u_1} [Field K] [NumberField K] (w : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) : (NumberField.mixedEmbedding.indexEquiv K) (Sum.inr (w, 1)) = NumberField.ComplexEmbedding.conjugate (NumberField.InfinitePlace.embedding ↑w)

def NumberField.mixedEmbedding.matrixToStdBasis (K : Type u_1) [Field K] : Matrix (NumberField.mixedEmbedding.index K) (NumberField.mixedEmbedding.index K) ℂ

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.

theorem NumberField.mixedEmbedding.det_matrixToStdBasis (K : Type u_1) [Field K] [NumberField K] : Matrix.det (NumberField.mixedEmbedding.matrixToStdBasis K) = (2⁻¹ * Complex.I) ^ NumberField.InfinitePlace.NrComplexPlaces K

theorem NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul (K : Type u_1) [Field K] [NumberField K] (x : (K →+* ℂ) → ℂ) (hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)) (c : NumberField.mixedEmbedding.index K) : ↑(((NumberField.mixedEmbedding.stdBasis K).repr ((NumberField.mixedEmbedding.commMap K) x)) c) = Matrix.mulVec (NumberField.mixedEmbedding.matrixToStdBasis K) (x ∘ ⇑(NumberField.mixedEmbedding.indexEquiv K)) c

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.

def NumberField.mixedEmbedding.latticeBasis (K : Type u_1) [Field K] [NumberField K] : Basis (Module.Free.ChooseBasisIndex ℤ ↥(NumberField.ringOfIntegers K)) ℝ (({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ))

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

Equations

• NumberField.mixedEmbedding.latticeBasis K = let_fun this := ⋯; basisOfLinearIndependentOfCardEqFinrank this ⋯

@[simp]

theorem NumberField.mixedEmbedding.latticeBasis_apply (K : Type u_1) [Field K] [NumberField K] (i : Module.Free.ChooseBasisIndex ℤ ↥(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 K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K)) ↔ x ∈ ⇑(NumberField.mixedEmbedding K) '' ↑(NumberField.ringOfIntegers K)

theorem NumberField.mixedEmbedding.mem_rat_span_latticeBasis (K : Type u_1) [Field K] [NumberField K] (x : K) : (NumberField.mixedEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K))

theorem NumberField.mixedEmbedding.latticeBasis_repr_apply (K : Type u_1) [Field K] [NumberField K] (x : K) (i : Module.Free.ChooseBasisIndex ℤ ↥(NumberField.ringOfIntegers K)) : ((NumberField.mixedEmbedding.latticeBasis K).repr ((NumberField.mixedEmbedding K) x)) i = ↑(((NumberField.integralBasis K).repr x) i)

theorem NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) (e : Module.Free.ChooseBasisIndex ℤ ↥(NumberField.ringOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : |(Basis.det (NumberField.mixedEmbedding.latticeBasis K)) (⇑(NumberField.mixedEmbedding K) ∘ ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)

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 ℝ^r₁ × ℂ^r₂. This is useful, in particular, to prove that the family obtained from the ℤ-basis of I is actually an ℝ-basis of ℝ^r₁ × ℂ^r₂, see fractionalIdealLatticeBasis.

def NumberField.mixedEmbedding.fractionalIdealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) : Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℝ (({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ))

A ℝ-basis of ℝ^r₁ × ℂ^r₂ that is also a ℤ-basis of the image of the fractional ideal I.

Equations

• NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I = let e := Fintype.equivOfCardEq ⋯; Basis.reindex (let_fun this := ⋯; Basis.mk ⋯ ⋯) e

@[simp]

theorem NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I) i = (NumberField.mixedEmbedding K) ((NumberField.basisOfFractionalIdeal K I) i)

theorem NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(NumberField.mixedEmbedding K) '' ↑↑I

@[inline, reducible]

abbrev NumberField.mixedEmbedding.convexBodyLT (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) : Set (({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // 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.

Equations

• One or more equations did not get rendered due to their size.

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_neg_mem (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // 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)

instance NumberField.mixedEmbedding.instIsAddHaarMeasureProdForAllSubtypeInfinitePlaceIsRealRealForAllIsComplexComplexInstAddGroupAddGroupInstAddGroupRealToAddGroupToNormedAddGroupInstNormedAddCommGroupComplexInstTopologicalSpaceProdTopologicalSpaceToTopologicalSpaceToUniformSpacePseudoMetricSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToMeasurableSpaceMeasureSpacePiFintypePropDecidableFintypeMeasureSpaceMeasureSpaceOfInnerProductSpaceComplexToRealInnerProductSpaceInstIsROrCComplexInstFiniteDimensionalRealComplexInstDivisionRingRealAddCommGroupInstModuleToSemiringToDivisionSemiringToModuleMeasurableSpaceBorelSpaceVolume (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.Measure.IsAddHaarMeasure MeasureTheory.volume

Equations

• ⋯ = ⋯

instance NumberField.mixedEmbedding.instNoAtomsProdForAllSubtypeInfinitePlaceIsRealRealForAllIsComplexComplexToMeasurableSpaceMeasureSpacePiFintypePropDecidableFintypeMeasureSpaceMeasureSpaceOfInnerProductSpaceInstNormedAddCommGroupComplexComplexToRealInnerProductSpaceInstIsROrCComplexInstFiniteDimensionalRealComplexInstDivisionRingRealAddCommGroupInstModuleToSemiringToDivisionSemiringToModuleMeasurableSpaceBorelSpaceVolume (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.NoAtoms MeasureTheory.volume

Equations

• ⋯ = ⋯

@[inline, reducible]

noncomputable abbrev NumberField.mixedEmbedding.convexBodyLTFactor (K : Type u_1) [Field K] [NumberField K] : NNReal

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

Equations

• NumberField.mixedEmbedding.convexBodyLTFactor K = 2 ^ NumberField.InfinitePlace.NrRealPlaces K * NNReal.pi ^ NumberField.InfinitePlace.NrComplexPlaces K

theorem NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.convexBodyLTFactor K ≠ 0

theorem NumberField.mixedEmbedding.one_le_convexBodyLTFactor (K : Type u_1) [Field K] [NumberField K] : 1 ≤ 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 : NumberField.InfinitePlace K) => 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 : NumberField.InfinitePlace K → NNReal), (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ (Finset.prod Finset.univ fun (w : NumberField.InfinitePlace K) => 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.

@[inline, reducible]

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

A version of convexBodyLT with an additional condition at a fixed complex place. This is needed to ensure the element constructed is not real, see for example exists_primitive_element_lt_of_isComplex.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.convexBodyLT'_mem (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) {x : K} : (NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀ ↔ (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧ |((NumberField.InfinitePlace.embedding ↑w₀) x).re| < 1 ∧ |((NumberField.InfinitePlace.embedding ↑w₀) x).im| < ↑(f ↑w₀) ^ 2

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

theorem NumberField.mixedEmbedding.convexBodyLT'_convex (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) : Convex ℝ (NumberField.mixedEmbedding.convexBodyLT' K f w₀)

@[inline, reducible]

noncomputable abbrev NumberField.mixedEmbedding.convexBodyLT'Factor (K : Type u_1) [Field K] [NumberField K] : NNReal

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

Equations

• NumberField.mixedEmbedding.convexBodyLT'Factor K = 2 ^ (NumberField.InfinitePlace.NrRealPlaces K + 2) * NNReal.pi ^ (NumberField.InfinitePlace.NrComplexPlaces K - 1)

theorem NumberField.mixedEmbedding.convexBodyLT'Factor_ne_zero (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.convexBodyLT'Factor K ≠ 0

theorem NumberField.mixedEmbedding.one_le_convexBodyLT'Factor (K : Type u_1) [Field K] [NumberField K] : 1 ≤ NumberField.mixedEmbedding.convexBodyLT'Factor K

theorem NumberField.mixedEmbedding.convexBodyLT'_volume (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) [NumberField K] : ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀) = ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑(Finset.prod Finset.univ fun (w : NumberField.InfinitePlace K) => f w ^ NumberField.InfinitePlace.mult w)

@[inline, reducible]

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

The function that sends x : ({w // IsReal w} → ℝ) × ({w // IsComplex w} → ℂ) to ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖. It defines a norm and it used to define convexBodySum.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.convexBodySumFun_nonneg {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : 0 ≤ NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_neg {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun (-x) = NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_add_le {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) (y : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun (x + y) ≤ NumberField.mixedEmbedding.convexBodySumFun x + NumberField.mixedEmbedding.convexBodySumFun y

theorem NumberField.mixedEmbedding.convexBodySumFun_smul {K : Type u_1} [Field K] [NumberField K] (c : ℝ) (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun (c • x) = |c| * NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun x = 0 ↔ x = 0

theorem NumberField.mixedEmbedding.norm_le_convexBodySumFun {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w } → ℝ) × ({ w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w } → ℂ)) : ‖x‖ ≤ NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_continuous (K : Type u_1) [Field K] [NumberField K] : Continuous NumberField.mixedEmbedding.convexBodySumFun

@[inline, reducible]

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

The convex body equal to the set of points x : E such that ∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero (K : Type u_1) [Field K] [NumberField K] {B : ℝ} (hB : B ≤ 0) : ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) = 0

theorem NumberField.mixedEmbedding.convexBodySum_mem (K : Type u_1) [Field K] [NumberField K] (B : ℝ) {x : K} : (NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodySum K B ↔ (Finset.sum Finset.univ fun (w : NumberField.InfinitePlace K) => ↑(NumberField.InfinitePlace.mult w) * ↑w x) ≤ B

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

theorem NumberField.mixedEmbedding.convexBodySum_convex (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Convex ℝ (NumberField.mixedEmbedding.convexBodySum K B)

theorem NumberField.mixedEmbedding.convexBodySum_isBounded (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Bornology.IsBounded (NumberField.mixedEmbedding.convexBodySum K B)

theorem NumberField.mixedEmbedding.convexBodySum_compact (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : IsCompact (NumberField.mixedEmbedding.convexBodySum K B)

@[inline, reducible]

noncomputable abbrev NumberField.mixedEmbedding.convexBodySumFactor (K : Type u_1) [Field K] [NumberField K] : NNReal

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

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.convexBodySumFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.convexBodySumFactor K ≠ 0

theorem NumberField.mixedEmbedding.convexBodySum_volume (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) = ↑(NumberField.mixedEmbedding.convexBodySumFactor K) * ENNReal.ofReal B ^ FiniteDimensional.finrank ℚ K

noncomputable def NumberField.mixedEmbedding.minkowskiBound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) 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. See NumberField.mixedEmbedding.volume_fundamentalDomain_idealLatticeBasis_eq and NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis for the computation of volume (fundamentalDomain (idealLatticeBasis K)).

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) : ↑↑MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) = ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * ↑↑MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K))

theorem NumberField.mixedEmbedding.minkowskiBound_lt_top (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) : NumberField.mixedEmbedding.minkowskiBound K I < ⊤

theorem NumberField.mixedEmbedding.minkowskiBound_pos (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) : 0 < NumberField.mixedEmbedding.minkowskiBound K I

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt (K : Type u_1) [Field K] [NumberField K] {f : NumberField.InfinitePlace K → NNReal} (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) (h : NumberField.mixedEmbedding.minkowskiBound K I < ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)) : ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(f w)

Let I be a fractional ideal of K. Assume that f : InfinitePlace K → ℝ≥0 is such that minkowskiBound K I < 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 number a in I such that w a < f w for all infinite places w.

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt' (K : Type u_1) [Field K] [NumberField K] {f : NumberField.InfinitePlace K → NNReal} (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) (w₀ : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) (h : NumberField.mixedEmbedding.minkowskiBound K I < ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀)) : ∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((NumberField.InfinitePlace.embedding ↑w₀) a).re| < 1 ∧ |((NumberField.InfinitePlace.embedding ↑w₀) a).im| < ↑(f ↑w₀) ^ 2

A version of exists_ne_zero_mem_ideal_lt where the absolute value of the real part of a is smaller than 1 at some fixed complex place. This is useful to ensure that a is not real.

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 1 < ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)) : ∃ a ∈ NumberField.ringOfIntegers K, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(f w)

A version of exists_ne_zero_mem_ideal_lt for the ring of integers of K.

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt' (K : Type u_1) [Field K] [NumberField K] {f : NumberField.InfinitePlace K → NNReal} (w₀ : { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }) (h : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀)) : ∃ a ∈ NumberField.ringOfIntegers K, a ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((NumberField.InfinitePlace.embedding ↑w₀) a).re| < 1 ∧ |((NumberField.InfinitePlace.embedding ↑w₀) a).im| < ↑(f ↑w₀) ^ 2

A version of exists_ne_zero_mem_ideal_lt' for the ring of integers of K.

theorem NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal (K : Type u_1) [Field K] [NumberField K] {w₀ : NumberField.InfinitePlace K} (hw₀ : NumberField.InfinitePlace.IsReal w₀) {B : NNReal} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) : ∃ a ∈ NumberField.ringOfIntegers K, ℚ⟮a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(max B 1)

theorem NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex (K : Type u_1) [Field K] [NumberField K] {w₀ : NumberField.InfinitePlace K} (hw₀ : NumberField.InfinitePlace.IsComplex w₀) {B : NNReal} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑B) : ∃ a ∈ NumberField.ringOfIntegers K, ℚ⟮a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w a < Real.sqrt (1 + ↑B ^ 2)

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) {B : ℝ} (h : NumberField.mixedEmbedding.minkowskiBound K I ≤ ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B)) : ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(FiniteDimensional.finrank ℚ K)) ^ FiniteDimensional.finrank ℚ K

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le (K : Type u_1) [Field K] [NumberField K] {B : ℝ} (h : NumberField.mixedEmbedding.minkowskiBound K 1 ≤ ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B)) : ∃ a ∈ NumberField.ringOfIntegers K, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(FiniteDimensional.finrank ℚ K)) ^ FiniteDimensional.finrank ℚ K