Infinite places of a number field

This file defines the infinite places of a number field.

Main Definitions and Results

• NumberField.InfinitePlace: the type of infinite places of a number field K.
• NumberField.InfinitePlace.mk_eq_iff: two complex embeddings define the same infinite place iff they are equal or complex conjugates.
• NumberField.InfinitePlace.IsReal: The predicate on infinite places saying that a place is real, i.e., defined by a real embedding.
• NumberField.InfinitePlace.IsComplex: The predicate on infinite places saying that a place is complex, i.e., defined by a complex embedding that is not real.
• NumberField.InfinitePlace.mult: the multiplicity of an infinite place, that is the number of distinct complex embeddings that define it. So it is equal to 1 if the place is real and 2 if the place is complex.
• NumberField.InfinitePlace.prod_eq_abs_norm: the infinite part of the product formula, that is for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where the product is over the infinite place w and ‖·‖_w is the normalized absolute value for w.
• NumberField.InfinitePlace.card_add_two_mul_card_eq_rank: the degree of K is equal to the number of real places plus twice the number of complex places.
• NumberField.InfinitePlace.denseRange_algebraMap_pi: the image of K by the diagonal embedding into the product of its infinite completions is dense.

Tags

number field, infinite places

def NumberField.InfinitePlace (K : Type u_1) [Field K] : Type u_1

An infinite place of a number field K is a place associated to a complex embedding.

instance NumberField.instNonemptyInfinitePlaceOfRingHomComplex (K : Type u_1) [Field K] [Nonempty (K →+* ℂ)] : Nonempty (InfinitePlace K)

noncomputable def NumberField.InfinitePlace.mk {K : Type u_1} [Field K] (φ : K →+* ℂ) : InfinitePlace K

Return the infinite place defined by a complex embedding φ.

def NumberField.IsInfinitePlace {K : Type u_1} [Field K] (w : AbsoluteValue K ℝ) : Prop

A predicate singling out infinite places among the absolute values on a number field K.

theorem NumberField.InfinitePlace.isInfinitePlace {K : Type u_1} [Field K] (v : InfinitePlace K) : IsInfinitePlace ↑v

theorem NumberField.isInfinitePlace_iff {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : IsInfinitePlace v ↔ ∃ (w : InfinitePlace K), ↑w = v

instance NumberField.InfinitePlace.instFunLikeReal {K : Type u_1} [Field K] : FunLike (InfinitePlace K) K ℝ

theorem NumberField.InfinitePlace.coe_apply {K : Type u_1} [Field K] (v : InfinitePlace K) (x : K) : v x = ↑v x

theorem NumberField.InfinitePlace.ext {K : Type u_1} [Field K] (v₁ v₂ : InfinitePlace K) (h : ∀ (k : K), v₁ k = v₂ k) : v₁ = v₂

theorem NumberField.InfinitePlace.ext_iff {K : Type u_1} [Field K] {v₁ v₂ : InfinitePlace K} : v₁ = v₂ ↔ ∀ (k : K), v₁ k = v₂ k

instance NumberField.InfinitePlace.instMonoidWithZeroHomClassReal {K : Type u_1} [Field K] : MonoidWithZeroHomClass (InfinitePlace K) K ℝ

instance NumberField.InfinitePlace.instNonnegHomClassReal {K : Type u_1} [Field K] : NonnegHomClass (InfinitePlace K) K ℝ

@[simp]

theorem NumberField.InfinitePlace.apply {K : Type u_1} [Field K] (φ : K →+* ℂ) (x : K) : (mk φ) x = ‖φ x‖

noncomputable def NumberField.InfinitePlace.embedding {K : Type u_1} [Field K] (w : InfinitePlace K) : K →+* ℂ

For an infinite place w, return an embedding φ such that w = infinite_place φ .

@[simp]

theorem NumberField.InfinitePlace.mk_embedding {K : Type u_1} [Field K] (w : InfinitePlace K) : mk w.embedding = w

@[simp]

theorem NumberField.InfinitePlace.mk_conjugate_eq {K : Type u_1} [Field K] (φ : K →+* ℂ) : mk (ComplexEmbedding.conjugate φ) = mk φ

theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_1} [Field K] (w : InfinitePlace K) (x : K) : ‖w.embedding x‖ = w x

theorem NumberField.InfinitePlace.embedding_injective (K : Type u_1) [Field K] : Function.Injective embedding

@[simp]

theorem NumberField.InfinitePlace.embedding_inj {K : Type u_1} [Field K] {v₁ v₂ : InfinitePlace K} : v₁.embedding = v₂.embedding ↔ v₁ = v₂

theorem NumberField.InfinitePlace.conjugate_embedding_injective (K : Type u_1) [Field K] : Function.Injective fun (v : InfinitePlace K) => ComplexEmbedding.conjugate v.embedding

theorem NumberField.InfinitePlace.eq_of_embedding_eq_conjugate (K : Type u_1) [Field K] {v₁ v₂ : InfinitePlace K} (h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding) : v₁ = v₂

theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_1} [Field K] (x : K) (r : ℝ) : (∀ (w : InfinitePlace K), w x = r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ = r

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

theorem NumberField.InfinitePlace.pos_iff {K : Type u_1} [Field K] {w : InfinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0

@[simp]

theorem NumberField.InfinitePlace.mk_eq_iff {K : Type u_1} [Field K] {φ ψ : K →+* ℂ} : mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

def NumberField.InfinitePlace.IsReal {K : Type u_1} [Field K] (w : InfinitePlace K) : Prop

An infinite place is real if it is defined by a real embedding.

def NumberField.InfinitePlace.IsComplex {K : Type u_1} [Field K] (w : InfinitePlace K) : Prop

An infinite place is complex if it is defined by a complex (i.e. not real) embedding.

theorem NumberField.InfinitePlace.embedding_mk_eq {K : Type u_1} [Field K] (φ : K →+* ℂ) : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ

@[simp]

theorem NumberField.InfinitePlace.embedding_mk_eq_of_isReal {K : Type u_1} [Field K] {φ : K →+* ℂ} (h : ComplexEmbedding.IsReal φ) : (mk φ).embedding = φ

theorem NumberField.InfinitePlace.isReal_iff {K : Type u_1} [Field K] {w : InfinitePlace K} : w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

theorem NumberField.InfinitePlace.isComplex_iff {K : Type u_1} [Field K] {w : InfinitePlace K} : w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

@[simp]

theorem NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal {K : Type u_1} [Field K] {w : InfinitePlace K} (h : w.IsReal) : ComplexEmbedding.conjugate w.embedding = w.embedding

@[simp]

theorem NumberField.InfinitePlace.not_isReal_iff_isComplex {K : Type u_1} [Field K] {w : InfinitePlace K} : ¬w.IsReal ↔ w.IsComplex

@[simp]

theorem NumberField.InfinitePlace.not_isComplex_iff_isReal {K : Type u_1} [Field K] {w : InfinitePlace K} : ¬w.IsComplex ↔ w.IsReal

theorem NumberField.InfinitePlace.isReal_or_isComplex {K : Type u_1} [Field K] (w : InfinitePlace K) : w.IsReal ∨ w.IsComplex

theorem NumberField.InfinitePlace.ne_of_isReal_isComplex {K : Type u_1} [Field K] {w w' : InfinitePlace K} (h : w.IsReal) (h' : w'.IsComplex) : w ≠ w'

theorem NumberField.InfinitePlace.disjoint_isReal_isComplex (K : Type u_1) [Field K] : Disjoint {w : InfinitePlace K | w.IsReal} {w : InfinitePlace K | w.IsComplex}

noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) : K →+* ℝ

The real embedding associated to a real infinite place.

@[simp]

theorem NumberField.InfinitePlace.embedding_of_isReal_apply {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : K) : ↑((embedding_of_isReal hw) x) = w.embedding x

theorem NumberField.InfinitePlace.norm_embedding_of_isReal {K : Type u_1} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : K) : ‖(embedding_of_isReal hw) x‖ = w x

@[simp]

theorem NumberField.InfinitePlace.isReal_of_mk_isReal {K : Type u_1} [Field K] {φ : K →+* ℂ} (h : (mk φ).IsReal) : ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isReal_mk_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : (mk φ).IsReal ↔ ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isComplex_mk_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : (mk φ).IsComplex ↔ ¬ComplexEmbedding.IsReal φ

@[simp]

theorem NumberField.InfinitePlace.not_isReal_of_mk_isComplex {K : Type u_1} [Field K] {φ : K →+* ℂ} (h : (mk φ).IsComplex) : ¬ComplexEmbedding.IsReal φ

noncomputable def NumberField.InfinitePlace.mult {K : Type u_1} [Field K] (w : InfinitePlace K) : ℕ

The multiplicity of an infinite place, that is the number of distinct complex embeddings that define it, see card_filter_mk_eq.

@[simp]

theorem NumberField.InfinitePlace.mult_isReal {K : Type u_1} [Field K] (w : { w : InfinitePlace K // w.IsReal }) : (↑w).mult = 1

@[simp]

theorem NumberField.InfinitePlace.mult_isComplex {K : Type u_1} [Field K] (w : { w : InfinitePlace K // w.IsComplex }) : (↑w).mult = 2

theorem NumberField.InfinitePlace.mult_pos {K : Type u_1} [Field K] {w : InfinitePlace K} : 0 < w.mult

@[simp]

theorem NumberField.InfinitePlace.mult_ne_zero {K : Type u_1} [Field K] {w : InfinitePlace K} : w.mult ≠ 0

theorem NumberField.InfinitePlace.mult_coe_ne_zero {K : Type u_1} [Field K] {w : InfinitePlace K} : ↑w.mult ≠ 0

theorem NumberField.InfinitePlace.one_le_mult {K : Type u_1} [Field K] {w : InfinitePlace K} : 1 ≤ ↑w.mult

theorem NumberField.InfinitePlace.card_filter_mk_eq {K : Type u_1} [Field K] [NumberField K] (w : InfinitePlace K) : {φ : K →+* ℂ | mk φ = w}.card = w.mult

noncomputable instance NumberField.InfinitePlace.NumberField.InfinitePlace.fintype {K : Type u_1} [Field K] [NumberField K] : Fintype (InfinitePlace K)

theorem NumberField.InfinitePlace.prod_eq_prod_mul_prod {K : Type u_1} [Field K] {α : Type u_2} [CommMonoid α] [NumberField K] (f : InfinitePlace K → α) : ∏ w : InfinitePlace K, f w = (∏ w : { w : InfinitePlace K // w.IsReal }, f ↑w) * ∏ w : { w : InfinitePlace K // w.IsComplex }, f ↑w

theorem NumberField.InfinitePlace.sum_eq_sum_add_sum {K : Type u_1} [Field K] {α : Type u_2} [AddCommMonoid α] [NumberField K] (f : InfinitePlace K → α) : ∑ w : InfinitePlace K, f w = ∑ w : { w : InfinitePlace K // w.IsReal }, f ↑w + ∑ w : { w : InfinitePlace K // w.IsComplex }, f ↑w

theorem NumberField.InfinitePlace.sum_mult_eq {K : Type u_1} [Field K] [NumberField K] : ∑ w : InfinitePlace K, w.mult = Module.finrank ℚ K

noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_1} [Field K] : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }

The map from real embeddings to real infinite places as an equiv

noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_1} [Field K] : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } → { w : InfinitePlace K // w.IsComplex }

The map from nonreal embeddings to complex infinite places

@[simp]

theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_1} [Field K] (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) : ↑(mkReal φ) = mk ↑φ

@[simp]

theorem NumberField.InfinitePlace.mkComplex_coe {K : Type u_1} [Field K] (φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) : ↑(mkComplex φ) = mk ↑φ

theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_1} [Field K] [NumberField K] (x : K) : ∏ w : InfinitePlace K, w x ^ w.mult = ↑|(Algebra.norm ℚ) x|

The infinite part of the product formula : for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where ‖·‖_w is the normalized absolute value for w.

theorem NumberField.InfinitePlace.one_le_of_lt_one {K : Type u_1} [Field K] [NumberField K] {w : InfinitePlace K} {a : RingOfIntegers K} (ha : a ≠ 0) (h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1) : 1 ≤ w ↑a

theorem NumberField.is_primitive_element_of_infinitePlace_lt {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) (h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1) : ℚ⟮↑x⟯ = ⊤

theorem NumberField.adjoin_eq_top_of_infinitePlace_lt {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) (h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1) : Algebra.adjoin ℚ {↑x} = ⊤

@[reducible, inline]

noncomputable abbrev NumberField.InfinitePlace.nrRealPlaces (K : Type u_1) [Field K] [NumberField K] : ℕ

The number of infinite real places of the number field K.

@[reducible, inline]

noncomputable abbrev NumberField.InfinitePlace.nrComplexPlaces (K : Type u_1) [Field K] [NumberField K] : ℕ

The number of infinite complex places of the number field K.

theorem NumberField.InfinitePlace.card_real_embeddings (K : Type u_1) [Field K] [NumberField K] : Fintype.card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = nrRealPlaces K

theorem NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces (K : Type u_1) [Field K] [NumberField K] : Fintype.card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

theorem NumberField.InfinitePlace.card_complex_embeddings (K : Type u_1) [Field K] [NumberField K] : Fintype.card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

theorem NumberField.InfinitePlace.card_add_two_mul_card_eq_rank (K : Type u_1) [Field K] [NumberField K] : nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K

theorem NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign (K : Type u_1) [Field K] [NumberField K] : Equiv.Perm.sign (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) = (-1) ^ nrComplexPlaces K

The signature of the permutation on the complex embeddings of K defined by sending an embedding to its conjugate has signature (-1) ^ nrComplexPlaces K.

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one {K : Type u_1} [Field K] [NumberField K] (h : Module.finrank ℚ K = 1) : nrComplexPlaces K = 0

theorem NumberField.InfinitePlace.nrRealPlaces_eq_one_of_finrank_eq_one {K : Type u_1} [Field K] [NumberField K] (h : Module.finrank ℚ K = 1) : nrRealPlaces K = 1

theorem NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank {K : Type u_1} [Field K] [NumberField K] (h : Odd (Module.finrank ℚ K)) : 0 < nrRealPlaces K

theorem NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt {K : Type u_1} [Field K] [NumberField K] {ζ : K} {k : ℕ} (hk : 2 < k) (hζ : IsPrimitiveRoot ζ k) : nrRealPlaces K = 0

The infinite place of the rationals.

noncomputable def Rat.infinitePlace : NumberField.InfinitePlace ℚ

The infinite place of ℚ, coming from the canonical map ℚ → ℂ.

@[simp]

theorem Rat.infinitePlace_apply (v : NumberField.InfinitePlace ℚ) (x : ℚ) : v x = ↑|x|

instance Rat.instSubsingletonInfinitePlace : Subsingleton (NumberField.InfinitePlace ℚ)

theorem Rat.isReal_infinitePlace : infinitePlace.IsReal

@[simp]

theorem NumberField.InfinitePlace.map_ratCast {K : Type u_1} [Field K] (v : InfinitePlace K) (x : ℚ) : v ↑x = ‖x‖

@[simp]

theorem NumberField.InfinitePlace.map_natCast {K : Type u_1} [Field K] (v : InfinitePlace K) (n : ℕ) : v ↑n = ↑n

@[simp]

theorem NumberField.InfinitePlace.map_intCast {K : Type u_1} [Field K] (v : InfinitePlace K) (z : ℤ) : v ↑z = ‖z‖

theorem NumberField.InfinitePlace.eq_one_of_rpow_eq {K : Type u_1} [Field K] {v w : InfinitePlace K} {t : ℝ} (h : (fun (x : K) => w x) ^ t = ⇑v) : t = 1

If v and w are infinite places of K and v = w ^ t for some t then t = 1.

theorem NumberField.InfinitePlace.eq_iff_isEquiv {K : Type u_1} [Field K] {v w : InfinitePlace K} : w = v ↔ (↑w).IsEquiv ↑v

Two infinite places v and w are equal if and only if their underlying absolute values are equivalent.

theorem NumberField.InfinitePlace.isNontrivial {K : Type u_1} [Field K] (v : InfinitePlace K) : (↑v).IsNontrivial

Infinite places are represented by non-trivial absolute values.

theorem NumberField.InfinitePlace.denseRange_algebraMap_pi (K : Type u_1) [Field K] [NumberField K] : DenseRange ⇑(algebraMap K ((v : InfinitePlace K) → WithAbs ↑v))

Weak approximation for infinite places The number field K is dense when embedded diagonally in the product (v : InfinitePlace K) → WithAbs v.1, in which WithAbs v.1 represents K equipped with the topology coming from the infinite place v.