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 to the mixed space 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.

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 ⇑(canonicalEmbedding K)

@[simp]

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

theorem NumberField.canonicalEmbedding.conj_apply {K : Type u_1} [Field K] {x : (K →+* ℂ) → ℂ} (φ : K →+* ℂ) (hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))) : (starRingEnd ℂ) (x φ) = x (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) : ‖(canonicalEmbedding K) x‖₊ = Finset.univ.sup fun (φ : K →+* ℂ) => ‖φ x‖₊

theorem NumberField.canonicalEmbedding.norm_le_iff {K : Type u_1} [Field K] [NumberField K] (x : K) (r : ℝ) : ‖(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 : ℝ) : (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite

noncomputable def NumberField.canonicalEmbedding.latticeBasis (K : Type u_1) [Field K] [NumberField K] : Module.Basis (Module.Free.ChooseBasisIndex ℤ (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 ℤ (RingOfIntegers K)) : (latticeBasis K) i = (canonicalEmbedding K) ((integralBasis K) i)

theorem NumberField.canonicalEmbedding.mem_span_latticeBasis (K : Type u_1) [Field K] [NumberField K] {x : (K →+* ℂ) → ℂ} : x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (RingOfIntegers K) K)).range

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

theorem NumberField.canonicalEmbedding.integralBasis_repr_apply (K : Type u_1) [Field K] [NumberField K] (x : K) (i : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) : ((latticeBasis K).repr ((canonicalEmbedding K) x)) i = ↑(((integralBasis K).repr x) i)

@[reducible, inline]

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

The mixed space ℝ^r₁ × ℂ^r₂ with (r₁, r₂) the signature of K.

noncomputable def NumberField.mixedEmbedding (K : Type u_1) [Field K] : K →+* mixedEmbedding.mixedSpace K

The mixed embedding of a number field K into the mixed space of K.

@[simp]

theorem NumberField.mixedEmbedding.mixedEmbedding_apply_isReal (K : Type u_1) [Field K] (x : K) (w : { w : InfinitePlace K // w.IsReal }) : ((mixedEmbedding K) x).1 w = (InfinitePlace.embedding_of_isReal ⋯) x

@[simp]

theorem NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex (K : Type u_1) [Field K] (x : K) (w : { w : InfinitePlace K // w.IsComplex }) : ((mixedEmbedding K) x).2 w = (↑w).embedding x

instance NumberField.mixedEmbedding.instNontrivialMixedSpace (K : Type u_1) [Field K] [NumberField K] : Nontrivial (mixedSpace K)

theorem NumberField.mixedEmbedding.finrank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℝ (mixedSpace K) = Module.finrank ℚ K

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

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

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

theorem NumberField.mixedEmbedding.volume_eq_zero {K : Type u_1} [Field K] [NumberField K] (w : { w : InfinitePlace K // w.IsReal }) : MeasureTheory.volume {x : mixedSpace K | x.1 w = 0} = 0

The set of points in the mixedSpace that are equal to 0 at a fixed (real) place has volume zero.

noncomputable def NumberField.mixedEmbedding.commMap (K : Type u_1) [Field K] : ((K →+* ℂ) → ℂ) →ₗ[ℝ] mixedSpace K

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 : InfinitePlace K} (hw : w.IsReal) : ((commMap K) x).1 ⟨w, hw⟩ = (x w.embedding).re

theorem NumberField.mixedEmbedding.commMap_apply_of_isComplex (K : Type u_1) [Field K] (x : (K →+* ℂ) → ℂ) {w : InfinitePlace K} (hw : w.IsComplex) : ((commMap K) x).2 ⟨w, hw⟩ = x w.embedding

@[simp]

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

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

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.

noncomputable def NumberField.mixedEmbedding.normAtPlace {K : Type u_1} [Field K] (w : InfinitePlace K) : mixedSpace K →*₀ ℝ

The norm at the infinite place w of an element of the mixed space

theorem NumberField.mixedEmbedding.normAtPlace_nonneg {K : Type u_1} [Field K] (w : InfinitePlace K) (x : mixedSpace K) : 0 ≤ (normAtPlace w) x

theorem NumberField.mixedEmbedding.normAtPlace_neg {K : Type u_1} [Field K] (w : InfinitePlace K) (x : mixedSpace K) : (normAtPlace w) (-x) = (normAtPlace w) x

theorem NumberField.mixedEmbedding.normAtPlace_add_le {K : Type u_1} [Field K] (w : InfinitePlace K) (x y : mixedSpace K) : (normAtPlace w) (x + y) ≤ (normAtPlace w) x + (normAtPlace w) y

theorem NumberField.mixedEmbedding.normAtPlace_smul {K : Type u_1} [Field K] (w : InfinitePlace K) (x : mixedSpace K) (c : ℝ) : (normAtPlace w) (c • x) = |c| * (normAtPlace w) x

theorem NumberField.mixedEmbedding.normAtPlace_real {K : Type u_1} [Field K] (w : InfinitePlace K) (c : ℝ) : (normAtPlace w) (fun (x : { w : InfinitePlace K // w.IsReal }) => c, fun (x : { w : InfinitePlace K // w.IsComplex }) => ↑c) = |c|

theorem NumberField.mixedEmbedding.normAtPlace_apply_of_isReal {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : mixedSpace K) : (normAtPlace w) x = ‖x.1 ⟨w, hw⟩‖

theorem NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsComplex) (x : mixedSpace K) : (normAtPlace w) x = ‖x.2 ⟨w, hw⟩‖

@[simp]

theorem NumberField.mixedEmbedding.normAtPlace_apply {K : Type u_1} [Field K] (w : InfinitePlace K) (x : K) : (normAtPlace w) ((mixedEmbedding K) x) = w x

theorem NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff {K : Type u_1} [Field K] {x : mixedSpace K} : (∀ (w : InfinitePlace K), (normAtPlace w) x = 0) ↔ x = 0

@[simp]

theorem NumberField.mixedEmbedding.exists_normAtPlace_ne_zero_iff {K : Type u_1} [Field K] {x : mixedSpace K} : (∃ (w : InfinitePlace K), (normAtPlace w) x ≠ 0) ↔ x ≠ 0

theorem NumberField.mixedEmbedding.continuous_normAtPlace {K : Type u_1} [Field K] (w : InfinitePlace K) : Continuous ⇑(normAtPlace w)

theorem NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : ‖x‖₊ = Finset.univ.sup fun (w : InfinitePlace K) => ⟨(normAtPlace w) x, ⋯⟩

theorem NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : ‖x‖ = Finset.univ.sup' ⋯ fun (w : InfinitePlace K) => (normAtPlace w) x

noncomputable def NumberField.mixedEmbedding.norm {K : Type u_1} [Field K] [NumberField K] : mixedSpace K →*₀ ℝ

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.

theorem NumberField.mixedEmbedding.norm_apply {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : mixedEmbedding.norm x = ∏ w : InfinitePlace K, (normAtPlace w) x ^ w.mult

theorem NumberField.mixedEmbedding.norm_nonneg {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : 0 ≤ mixedEmbedding.norm x

theorem NumberField.mixedEmbedding.norm_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} : mixedEmbedding.norm x = 0 ↔ ∃ (w : InfinitePlace K), (normAtPlace w) x = 0

theorem NumberField.mixedEmbedding.norm_ne_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} : mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0

theorem NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq {K : Type u_1} [Field K] [NumberField K] {x y : mixedSpace K} (h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y) : mixedEmbedding.norm x = mixedEmbedding.norm y

theorem NumberField.mixedEmbedding.norm_smul {K : Type u_1} [Field K] [NumberField K] (c : ℝ) (x : mixedSpace K) : mixedEmbedding.norm (c • x) = |c| ^ Module.finrank ℚ K * mixedEmbedding.norm x

theorem NumberField.mixedEmbedding.norm_real {K : Type u_1} [Field K] [NumberField K] (c : ℝ) : mixedEmbedding.norm (fun (x : { w : InfinitePlace K // w.IsReal }) => c, fun (x : { w : InfinitePlace K // w.IsComplex }) => ↑c) = |c| ^ Module.finrank ℚ K

@[simp]

theorem NumberField.mixedEmbedding.norm_eq_norm {K : Type u_1} [Field K] [NumberField K] (x : K) : mixedEmbedding.norm ((mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|

theorem NumberField.mixedEmbedding.norm_unit {K : Type u_1} [Field K] [NumberField K] (u : (RingOfIntegers K)ˣ) : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (RingOfIntegers K) K) ↑u)) = 1

theorem NumberField.mixedEmbedding.norm_eq_zero_iff' {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : x ∈ Set.range ⇑(mixedEmbedding K)) : mixedEmbedding.norm x = 0 ↔ x = 0

theorem NumberField.mixedEmbedding.continuous_norm (K : Type u_1) [Field K] [NumberField K] : Continuous ⇑mixedEmbedding.norm

@[reducible, inline]

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

The type indexing the basis stdBasis.

noncomputable def NumberField.mixedEmbedding.stdBasis (K : Type u_1) [Field K] [NumberField K] : Module.Basis (index K) ℝ (mixedSpace K)

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.

@[simp]

theorem NumberField.mixedEmbedding.stdBasis_apply_isReal {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsReal }) : ((stdBasis K).repr x) (Sum.inl w) = x.1 w

@[simp]

theorem NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) : ((stdBasis K).repr x) (Sum.inr (w, 0)) = (x.2 w).re

@[simp]

theorem NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) : ((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 (stdBasis K) = (Set.univ.pi fun (x : { w : InfinitePlace K // w.IsReal }) => Set.Ico 0 1) ×ˢ Set.univ.pi fun (x : { w : InfinitePlace K // w.IsComplex }) => ⇑Complex.measurableEquivPi ⁻¹' Set.univ.pi 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 (stdBasis K)) = 1

noncomputable def NumberField.mixedEmbedding.indexEquiv (K : Type u_1) [Field K] [NumberField K] : 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).

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def NumberField.mixedEmbedding.matrixToStdBasis (K : Type u_1) [Field K] : Matrix (index K) (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.

theorem NumberField.mixedEmbedding.det_matrixToStdBasis (K : Type u_1) [Field K] [NumberField K] : (matrixToStdBasis K).det = (2⁻¹ * Complex.I) ^ 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 (ComplexEmbedding.conjugate φ)) (c : index K) : ↑(((stdBasis K).repr ((commMap K) x)) c) = (matrixToStdBasis K).mulVec (x ∘ ⇑(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.

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.integerLattice (K : Type u_1) [Field K] : Submodule ℤ (mixedSpace K)

The image of the ring of integers of K in the mixed space.

noncomputable def NumberField.mixedEmbedding.latticeBasis (K : Type u_1) [Field K] [NumberField K] : Module.Basis (Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)) ℝ (mixedSpace K)

A ℝ-basis of the mixed space 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 ℤ (RingOfIntegers K)) : (latticeBasis K) i = (mixedEmbedding K) ((integralBasis K) i)

theorem NumberField.mixedEmbedding.mem_span_latticeBasis (K : Type u_1) [Field K] [NumberField K] {x : mixedSpace K} : x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ mixedEmbedding.integerLattice K

theorem NumberField.mixedEmbedding.span_latticeBasis (K : Type u_1) [Field K] [NumberField K] : Submodule.span ℤ (Set.range ⇑(latticeBasis K)) = mixedEmbedding.integerLattice K

instance NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(mixedEmbedding.integerLattice K)

instance NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice (K : Type u_1) [Field K] [NumberField K] : IsZLattice ℝ (mixedEmbedding.integerLattice K)

theorem NumberField.mixedEmbedding.fundamentalDomain_integerLattice (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.IsAddFundamentalDomain (↥(mixedEmbedding.integerLattice K)) (ZSpan.fundamentalDomain (latticeBasis K)) MeasureTheory.volume

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

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

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.idealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule ℤ (mixedSpace K)

The image of the fractional ideal I in the mixed space.

theorem NumberField.mixedEmbedding.mem_idealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {x : mixedSpace K} : x ∈ idealLattice K I ↔ ∃ y ∈ ↑↑I, (mixedEmbedding K) y = x

theorem NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (e : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : |(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(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 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.

noncomputable def NumberField.mixedEmbedding.fractionalIdealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℝ (mixedSpace K)

A ℝ-basis of the mixed space of K that is also a ℤ-basis of the image of the fractional ideal I.

@[simp]

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

theorem NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {x : mixedSpace K} : x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

theorem NumberField.mixedEmbedding.span_idealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) = idealLattice K I

instance NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : DiscreteTopology ↥(idealLattice K I)

instance NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : IsZLattice ℝ (idealLattice K I)

theorem NumberField.mixedEmbedding.fundamentalDomain_idealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : MeasureTheory.IsAddFundamentalDomain (↥(idealLattice K I)) (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I)) MeasureTheory.volume

@[reducible, inline]

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

The mixed space ℝ^r₁ × ℂ^r₂, with (r₁, r₂) the signature of K, as a Euclidean space.

@[implicit_reducible]

instance NumberField.mixedEmbedding.euclidean.instRingMixedSpace (K : Type u_1) [Field K] : Ring (euclidean.mixedSpace K)

noncomputable def NumberField.mixedEmbedding.euclidean.toMixed (K : Type u_1) [Field K] [NumberField K] : euclidean.mixedSpace K ≃L[ℝ] mixedSpace K

The continuous linear equivalence between the Euclidean mixed space and the mixed space.

instance NumberField.mixedEmbedding.euclidean.instNontrivialMixedSpace (K : Type u_1) [Field K] [NumberField K] : Nontrivial (euclidean.mixedSpace K)

theorem NumberField.mixedEmbedding.euclidean.finrank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℝ (euclidean.mixedSpace K) = Module.finrank ℚ K

noncomputable def NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis (K : Type u_1) [Field K] [NumberField K] : OrthonormalBasis (index K) ℝ (euclidean.mixedSpace K)

An orthonormal basis of the Euclidean mixed space.

theorem NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq (K : Type u_1) [Field K] [NumberField K] : (stdOrthonormalBasis K).toBasis.map (toMixed K).toLinearEquiv = stdBasis K

theorem NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.MeasurePreserving (⇑(toMixed K)) MeasureTheory.volume MeasureTheory.volume

theorem NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.MeasurePreserving (⇑(toMixed K).symm) MeasureTheory.volume MeasureTheory.volume

noncomputable def NumberField.mixedEmbedding.euclidean.integerLattice (K : Type u_1) [Field K] [NumberField K] : Submodule ℤ (euclidean.mixedSpace K)

The image of ring of integers 𝓞 K in the Euclidean mixed space.

instance NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(euclidean.integerLattice K)

instance NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice (K : Type u_1) [Field K] [NumberField K] : IsZLattice ℝ (euclidean.integerLattice K)

noncomputable def NumberField.mixedEmbedding.negAt {K : Type u_1} [Field K] (s : Set { w : InfinitePlace K // w.IsReal }) : mixedSpace K ≃L[ℝ] mixedSpace K

Let s be a set of real places, define the continuous linear equiv of the mixed space that swaps sign at places in s and leaves the rest unchanged.

@[simp]

theorem NumberField.mixedEmbedding.negAt_apply_isReal_and_mem {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (x : mixedSpace K) {w : { w : InfinitePlace K // w.IsReal }} (hw : w ∈ s) : ((negAt s) x).1 w = -x.1 w

@[simp]

theorem NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (x : mixedSpace K) {w : { w : InfinitePlace K // w.IsReal }} (hw : w ∉ s) : ((negAt s) x).1 w = x.1 w

@[simp]

theorem NumberField.mixedEmbedding.negAt_apply_isComplex {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) : ((negAt s) x).2 w = x.2 w

@[simp]

theorem NumberField.mixedEmbedding.negAt_apply_snd {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (x : mixedSpace K) : ((negAt s) x).2 = x.2

theorem NumberField.mixedEmbedding.negAt_apply_norm_isReal {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsReal }) : ‖((negAt s) x).1 w‖ = ‖x.1 w‖

theorem NumberField.mixedEmbedding.volume_preserving_negAt {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} [NumberField K] : MeasureTheory.MeasurePreserving (⇑(negAt s)) MeasureTheory.volume MeasureTheory.volume

negAt preserves the volume .

@[simp]

theorem NumberField.mixedEmbedding.normAtPlace_negAt {K : Type u_1} [Field K] (s : Set { w : InfinitePlace K // w.IsReal }) (x : mixedSpace K) (w : InfinitePlace K) : (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

negAt preserves normAtPlace.

@[simp]

theorem NumberField.mixedEmbedding.norm_negAt {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} [NumberField K] (x : mixedSpace K) : mixedEmbedding.norm ((negAt s) x) = mixedEmbedding.norm x

negAt preserves the norm.

@[simp]

theorem NumberField.mixedEmbedding.negAt_symm {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} : (negAt s).symm = negAt s

negAt is its own inverse.

def NumberField.mixedEmbedding.signSet {K : Type u_1} [Field K] (x : mixedSpace K) : Set { w : InfinitePlace K // w.IsReal }

For x : mixedSpace K, the set signSet x is the set of real places w s.t. x w ≤ 0.

@[simp]

theorem NumberField.mixedEmbedding.negAt_signSet_apply_isReal {K : Type u_1} [Field K] (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsReal }) : ((negAt (signSet x)) x).1 w = ‖x.1 w‖

@[simp]

theorem NumberField.mixedEmbedding.negAt_signSet_apply_isComplex {K : Type u_1} [Field K] (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) : ((negAt (signSet x)) x).2 w = x.2 w

theorem NumberField.mixedEmbedding.negAt_preimage {K : Type u_1} [Field K] (s : Set { w : InfinitePlace K // w.IsReal }) (A : Set (mixedSpace K)) : ⇑(negAt s) ⁻¹' A = ⇑(negAt s) '' A

negAt s A is also equal to the preimage of A by negAt s. This fact is used to simplify some proofs.

@[reducible, inline]

abbrev NumberField.mixedEmbedding.plusPart {K : Type u_1} [Field K] (A : Set (mixedSpace K)) : Set (mixedSpace K)

The plusPart of a subset A of the mixedSpace is the set of points in A that are positive at all real places.

theorem NumberField.mixedEmbedding.neg_of_mem_negA_plusPart {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (A : Set (mixedSpace K)) {x : mixedSpace K} (hx : x ∈ ⇑(negAt s) '' plusPart A) {w : { w : InfinitePlace K // w.IsReal }} (hw : w ∈ s) : x.1 w < 0

theorem NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (A : Set (mixedSpace K)) {x : mixedSpace K} (hx : x ∈ ⇑(negAt s) '' plusPart A) {w : { w : InfinitePlace K // w.IsReal }} (hw : w ∉ s) : 0 < x.1 w

theorem NumberField.mixedEmbedding.disjoint_negAt_plusPart {K : Type u_1} [Field K] (A : Set (mixedSpace K)) : Pairwise (Function.onFun Disjoint fun (s : Set { w : InfinitePlace K // w.IsReal }) => ⇑(negAt s) '' plusPart A)

The images of plusPart by negAt are pairwise disjoint.

theorem NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} (A : Set (mixedSpace K)) {x : mixedSpace K} (hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) => ‖x.1 w‖, x.2) ∈ A) (hx₁ : x ∈ A) (hx₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w ≠ 0) : x ∈ ⇑(negAt s) '' plusPart A ↔ (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0

theorem NumberField.mixedEmbedding.iUnion_negAt_plusPart_union {K : Type u_1} [Field K] (A : Set (mixedSpace K)) (hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) => ‖x.1 w‖, x.2) ∈ A) : (⋃ (s : Set { w : InfinitePlace K // w.IsReal }), ⇑(negAt s) '' plusPart A) ∪ A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0} = A

Assume that A is symmetric at real places then, the union of the images of plusPart by negAt and of the set of elements of A that are zero at at least one real place is equal to A.

theorem NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae {K : Type u_1} [Field K] (A : Set (mixedSpace K)) (hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) => ‖x.1 w‖, x.2) ∈ A) [NumberField K] : ⋃ (s : Set { w : InfinitePlace K // w.IsReal }), ⇑(negAt s) '' plusPart A =ᵐ[MeasureTheory.volume] A

theorem NumberField.mixedEmbedding.measurableSet_plusPart {K : Type u_1} [Field K] {A : Set (mixedSpace K)} [NumberField K] (hm : MeasurableSet A) : MeasurableSet (plusPart A)

theorem NumberField.mixedEmbedding.measurableSet_negAt_plusPart {K : Type u_1} [Field K] (s : Set { w : InfinitePlace K // w.IsReal }) (A : Set (mixedSpace K)) [NumberField K] (hm : MeasurableSet A) : MeasurableSet (⇑(negAt s) '' plusPart A)

theorem NumberField.mixedEmbedding.volume_negAt_plusPart {K : Type u_1} [Field K] {s : Set { w : InfinitePlace K // w.IsReal }} {A : Set (mixedSpace K)} [NumberField K] (hm : MeasurableSet A) : MeasureTheory.volume (⇑(negAt s) '' plusPart A) = MeasureTheory.volume (plusPart A)

The image of the plusPart of A by negAt have all the same volume as plusPart A.

theorem NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart {K : Type u_1} [Field K] {A : Set (mixedSpace K)} (hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) => ‖x.1 w‖, x.2) ∈ A) [NumberField K] (hm : MeasurableSet A) : MeasureTheory.volume A = 2 ^ InfinitePlace.nrRealPlaces K * MeasureTheory.volume (plusPart A)

If a subset A of the mixedSpace is symmetric at real places, then its volume is 2^ nrRealPlaces K times the volume of its plusPart.

@[reducible, inline]

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

The realSpace associated to a number field K is the real vector space indexed by the infinite places of K.

theorem NumberField.mixedEmbedding.realSpace.volume_eq_zero {K : Type u_1} [Field K] [NumberField K] (w : InfinitePlace K) : MeasureTheory.volume {x : realSpace K | x w = 0} = 0

The set of points in the realSpace that are equal to 0 at a fixed place has volume zero.

noncomputable def NumberField.mixedEmbedding.mixedSpaceOfRealSpace {K : Type u_1} [Field K] : realSpace K →L[ℝ] mixedSpace K

The continuous linear map from realSpace K to mixedSpace K which is the identity at real places and the natural map ℝ → ℂ at complex places.

theorem NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply {K : Type u_1} [Field K] (x : realSpace K) : mixedSpaceOfRealSpace x = (fun (w : { w : InfinitePlace K // w.IsReal }) => x ↑w, fun (w : { w : InfinitePlace K // w.IsComplex }) => ↑(x ↑w))

theorem NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace (K : Type u_1) [Field K] : Function.Injective ⇑mixedSpaceOfRealSpace

theorem NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace {K : Type u_1} [Field K] {x : realSpace K} {w : InfinitePlace K} (hx : 0 ≤ x w) : (normAtPlace w) (mixedSpaceOfRealSpace x) = x w

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.normAtComplexPlaces {K : Type u_1} [Field K] (x : mixedSpace K) : realSpace K

The map from the mixedSpace K to realSpace K that sends the values at complex places to their norm.

@[simp]

theorem NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal {K : Type u_1} [Field K] {x : mixedSpace K} (w : { w : InfinitePlace K // w.IsReal }) : normAtComplexPlaces x ↑w = x.1 w

@[simp]

theorem NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex {K : Type u_1} [Field K] {x : mixedSpace K} (w : { w : InfinitePlace K // w.IsComplex }) : normAtComplexPlaces x ↑w = ‖x.2 w‖

theorem NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace {K : Type u_1} [Field K] {x : realSpace K} (hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w) : normAtComplexPlaces (mixedSpaceOfRealSpace x) = x

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.normAtAllPlaces {K : Type u_1} [Field K] (x : mixedSpace K) : realSpace K

The map from the mixedSpace K to realSpace K that sends each component to its norm.

@[simp]

theorem NumberField.mixedEmbedding.normAtAllPlaces_apply {K : Type u_1} [Field K] (x : mixedSpace K) (w : InfinitePlace K) : normAtAllPlaces x w = (normAtPlace w) x

theorem NumberField.mixedEmbedding.continuous_normAtAllPlaces (K : Type u_1) [Field K] : Continuous normAtAllPlaces

theorem NumberField.mixedEmbedding.normAtAllPlaces_nonneg {K : Type u_1} [Field K] (x : mixedSpace K) (w : InfinitePlace K) : 0 ≤ normAtAllPlaces x w

theorem NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace {K : Type u_1} [Field K] {x : realSpace K} (hx : ∀ (w : InfinitePlace K), 0 ≤ x w) : normAtAllPlaces (mixedSpaceOfRealSpace x) = x

theorem NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding {K : Type u_1} [Field K] (x : K) (w : InfinitePlace K) : normAtAllPlaces ((mixedEmbedding K) x) w = w x

theorem NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces {K : Type u_1} [Field K] (x : mixedSpace K) : normAtAllPlaces (mixedSpaceOfRealSpace (normAtAllPlaces x)) = normAtAllPlaces x

theorem NumberField.mixedEmbedding.normAtAllPlaces_norm_at_real_places {K : Type u_1} [Field K] (x : mixedSpace K) : normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) => ‖x.1 w‖, x.2) = normAtAllPlaces x

theorem NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces {K : Type u_1} [Field K] (x : mixedSpace K) : normAtComplexPlaces (mixedSpaceOfRealSpace (normAtAllPlaces x)) = normAtAllPlaces x

theorem NumberField.mixedEmbedding.normAtAllPlaces_eq_of_normAtComplexPlaces_eq {K : Type u_1} [Field K] {x y : mixedSpace K} (h : normAtComplexPlaces x = normAtComplexPlaces y) : normAtAllPlaces x = normAtAllPlaces y

theorem NumberField.mixedEmbedding.normAtAllPlaces_image_preimage_of_nonneg {K : Type u_1} [Field K] {s : Set (realSpace K)} (hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w) : normAtAllPlaces '' (normAtAllPlaces ⁻¹' s) = s