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.

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

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

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

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 // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ))

Equations

• ⋯ = ⋯

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

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 ℝ^r₁ × ℂ^r₂, see mixedEmbedding.latticeBasis.

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

The norm at the infinite place w of an element of ({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ).

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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : 0 ≤ (NumberField.mixedEmbedding.normAtPlace w) x

theorem NumberField.mixedEmbedding.normAtPlace_neg {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (y : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : (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.normAtPlace_eq_zero {K : Type u_1} [Field K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)} : (∀ (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : ‖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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : ‖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] : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ) →*₀ ℝ

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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : 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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : 0 ≤ NumberField.mixedEmbedding.norm x

theorem NumberField.mixedEmbedding.norm_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)} : 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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)} : NumberField.mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x ≠ 0

theorem NumberField.mixedEmbedding.norm_smul {K : Type u_1} [Field K] [NumberField K] (c : ℝ) (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : NumberField.mixedEmbedding.norm (c • x) = |c| ^ FiniteDimensional.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| ^ FiniteDimensional.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_eq_zero_iff' {K : Type u_1} [Field K] [NumberField K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)} (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) ℝ (({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ))

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 // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (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 : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (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.

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

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 // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K)) ↔ x ∈ ((NumberField.mixedEmbedding K).comp (algebraMap (NumberField.RingOfIntegers K) K)).range

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) : |(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 ℝ^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 // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ))

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 ⋯; (let_fun this := ⋯; Basis.mk ⋯ ⋯).reindex 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 // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(NumberField.mixedEmbedding K) '' ↑↑I