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.

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.univ.sup 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) (algebraMap (NumberField.RingOfIntegers K) K).range

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

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

• NumberField.canonicalEmbedding.latticeBasis K = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[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).comp (algebraMap (NumberField.RingOfIntegers K) K)).range

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

theorem NumberField.canonicalEmbedding.integralBasis_repr_apply (K : Type u_1) [Field K] [NumberField K] (x : K) (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) : ((NumberField.canonicalEmbedding.latticeBasis K).repr ((NumberField.canonicalEmbedding K) x)) i = ↑(((NumberField.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.

Equations

• NumberField.mixedEmbedding.mixedSpace K = (({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ))

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

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.

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem NumberField.mixedEmbedding.volume_eq_zero {K : Type u_1} [Field K] [NumberField K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) : MeasureTheory.volume {x : NumberField.mixedEmbedding.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 →+* ℂ) → ℂ) →ₗ[ℝ] NumberField.mixedEmbedding.mixedSpace K

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 : w.IsReal) : ((NumberField.mixedEmbedding.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 : NumberField.InfinitePlace K} (hw : w.IsComplex) : ((NumberField.mixedEmbedding.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) : (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 the mixed space ℝ^r₁ × ℂ^r₂, see mixedEmbedding.latticeBasis.

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

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.

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

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

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

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

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

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

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

@[simp]

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

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

@[deprecated NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff]

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

Alias of NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff.

@[simp]

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

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

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

def NumberField.mixedEmbedding.norm {K : Type u_1} [Field K] [NumberField K] : NumberField.mixedEmbedding.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.

Equations

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

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

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

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

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

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

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

theorem NumberField.mixedEmbedding.norm_real {K : Type u_1} [Field K] [NumberField K] (c : ℝ) : NumberField.mixedEmbedding.norm (fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => c, fun (x : { w : NumberField.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) : NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|

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

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

@[reducible, inline]

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

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)

def NumberField.mixedEmbedding.stdBasis (K : Type u_1) [Field K] [NumberField K] : Basis (NumberField.mixedEmbedding.index K) ℝ (NumberField.mixedEmbedding.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.

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 : NumberField.mixedEmbedding.mixedSpace K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : ((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 : NumberField.mixedEmbedding.mixedSpace K) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) : ((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 : NumberField.mixedEmbedding.mixedSpace K) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) : ((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.univ.pi fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => Set.Ico 0 1) ×ˢ Set.univ.pi fun (x : { w : NumberField.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 (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 // w.IsReal }) : (NumberField.mixedEmbedding.indexEquiv K) (Sum.inl w) = (↑w).embedding

@[simp]

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

@[simp]

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

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] : (NumberField.mixedEmbedding.matrixToStdBasis K).det = (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) = (NumberField.mixedEmbedding.matrixToStdBasis K).mulVec (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.

@[reducible, inline]

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

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

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

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

Equations

• NumberField.mixedEmbedding.latticeBasis K = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[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 : NumberField.mixedEmbedding.mixedSpace K} : x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K)) ↔ x ∈ NumberField.mixedEmbedding.integerLattice K

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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)

@[reducible, inline]

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

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

Equations

• NumberField.mixedEmbedding.idealLattice K I = LinearMap.range ((NumberField.mixedEmbedding K).toIntAlgHom.toLinearMap ∘ₗ ↑ℤ (↑↑I).subtype)

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

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) : |(NumberField.mixedEmbedding.latticeBasis K).det (⇑(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 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.

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

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 ⋯)

@[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 : NumberField.mixedEmbedding.mixedSpace K} : x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(NumberField.mixedEmbedding K) '' ↑↑I

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

def NumberField.mixedEmbedding.negAt {K : Type u_1} [Field K] (s : Set { w : NumberField.InfinitePlace K // w.IsReal }) : NumberField.mixedEmbedding.mixedSpace K ≃L[ℝ] NumberField.mixedEmbedding.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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem NumberField.mixedEmbedding.volume_preserving_negAt {K : Type u_1} [Field K] {s : Set { w : NumberField.InfinitePlace K // w.IsReal }} [NumberField K] : MeasureTheory.MeasurePreserving (⇑(NumberField.mixedEmbedding.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 : NumberField.InfinitePlace K // w.IsReal }) (x : NumberField.mixedEmbedding.mixedSpace K) (w : NumberField.InfinitePlace K) : (NumberField.mixedEmbedding.normAtPlace w) ((NumberField.mixedEmbedding.negAt s) x) = (NumberField.mixedEmbedding.normAtPlace w) x

negAt preserves normAtPlace.

@[simp]

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

negAt preserves the norm.

@[simp]

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

negAt is its own inverse.

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

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

Equations

• NumberField.mixedEmbedding.signSet x = {w : { w : NumberField.InfinitePlace K // w.IsReal } | x.1 w ≤ 0}

@[simp]

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

@[simp]

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

theorem NumberField.mixedEmbedding.negAt_preimage {K : Type u_1} [Field K] (s : Set { w : NumberField.InfinitePlace K // w.IsReal }) (A : Set (NumberField.mixedEmbedding.mixedSpace K)) : ⇑(NumberField.mixedEmbedding.negAt s) ⁻¹' A = ⇑(NumberField.mixedEmbedding.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 (NumberField.mixedEmbedding.mixedSpace K)) : Set (NumberField.mixedEmbedding.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.

Equations

• NumberField.mixedEmbedding.plusPart A = A ∩ {x : NumberField.mixedEmbedding.mixedSpace K | ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), 0 < x.1 w}

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

theorem NumberField.mixedEmbedding.pos_of_not_mem_negAt_plusPart {K : Type u_1} [Field K] {s : Set { w : NumberField.InfinitePlace K // w.IsReal }} (A : Set (NumberField.mixedEmbedding.mixedSpace K)) {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A) {w : { w : NumberField.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 (NumberField.mixedEmbedding.mixedSpace K)) : Pairwise (Disjoint on fun (s : Set { w : NumberField.InfinitePlace K // w.IsReal }) => ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.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 : NumberField.InfinitePlace K // w.IsReal }} (A : Set (NumberField.mixedEmbedding.mixedSpace K)) {x : NumberField.mixedEmbedding.mixedSpace K} (hA : ∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun (w : { w : NumberField.InfinitePlace K // w.IsReal }) => |x.1 w|, x.2) ∈ A) (hx₁ : x ∈ A) (hx₂ : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), x.1 w ≠ 0) : x ∈ ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.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 (NumberField.mixedEmbedding.mixedSpace K)) (hA : ∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun (w : { w : NumberField.InfinitePlace K // w.IsReal }) => |x.1 w|, x.2) ∈ A) : (⋃ (s : Set { w : NumberField.InfinitePlace K // w.IsReal }), ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A) ∪ A ∩ ⋃ (w : { w : NumberField.InfinitePlace K // w.IsReal }), {x : NumberField.mixedEmbedding.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 (NumberField.mixedEmbedding.mixedSpace K)) (hA : ∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun (w : { w : NumberField.InfinitePlace K // w.IsReal }) => |x.1 w|, x.2) ∈ A) [NumberField K] : ⋃ (s : Set { w : NumberField.InfinitePlace K // w.IsReal }), ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A =ᵐ[MeasureTheory.volume] A

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

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

theorem NumberField.mixedEmbedding.volume_negAt_plusPart {K : Type u_1} [Field K] {s : Set { w : NumberField.InfinitePlace K // w.IsReal }} (A : Set (NumberField.mixedEmbedding.mixedSpace K)) [NumberField K] (hm : MeasurableSet A) : MeasureTheory.volume (⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A) = MeasureTheory.volume (NumberField.mixedEmbedding.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 (NumberField.mixedEmbedding.mixedSpace K)) (hA : ∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun (w : { w : NumberField.InfinitePlace K // w.IsReal }) => |x.1 w|, x.2) ∈ A) [NumberField K] (hm : MeasurableSet A) : MeasureTheory.volume A = 2 ^ NumberField.InfinitePlace.nrRealPlaces K * MeasureTheory.volume (NumberField.mixedEmbedding.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.