Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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.

Tags #

number field, infinite places

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

Type u_2

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

Equations

NumberField.InfinitePlace K = { w : AbsoluteValue K ℝ // ∃ (φ : K →+* ℂ), NumberField.place φ = w }

Instances For

instance instNonemptyInfinitePlaceOfNumberField (K : Type u_2) [Field K] [NumberField K] :

Nonempty (NumberField.InfinitePlace K)

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

InfinitePlace K

Return the infinite place defined by a complex embedding φ.

Equations

NumberField.InfinitePlace.mk φ = ⟨NumberField.place φ, ⋯⟩

Instances For

instance NumberField.InfinitePlace.instFunLikeReal {K : Type u_4} [Field K] :

FunLike (InfinitePlace K) K ℝ

Equations

NumberField.InfinitePlace.instFunLikeReal = { coe := fun (w : NumberField.InfinitePlace K) (x : K) => ↑w x, coe_injective' := ⋯ }

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

v x = ↑v x

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

v₁ = v₂

theorem NumberField.InfinitePlace.ext_iff {K : Type u_4} [Field K] {v₁ v₂ : InfinitePlace K} :

v₁ = v₂ ↔ ∀ (k : K), v₁ k = v₂ k

instance NumberField.InfinitePlace.instMonoidWithZeroHomClassReal {K : Type u_2} [Field K] :

MonoidWithZeroHomClass (InfinitePlace K) K ℝ

instance NumberField.InfinitePlace.instNonnegHomClassReal {K : Type u_2} [Field K] :

NonnegHomClass (InfinitePlace K) K ℝ

@[simp]

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

(mk φ) x = ‖φ x‖

noncomputable def NumberField.InfinitePlace.embedding {K : Type u_2} [Field K] (w : InfinitePlace K) :

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

Equations

w.embedding = ⋯.choose

Instances For

@[simp]

theorem NumberField.InfinitePlace.mk_embedding {K : Type u_2} [Field K] (w : InfinitePlace K) :

mk w.embedding = w

@[simp]

theorem NumberField.InfinitePlace.mk_conjugate_eq {K : Type u_2} [Field K] (φ : K →+* ℂ) :

mk (ComplexEmbedding.conjugate φ) = mk φ

theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_2} [Field K] (w : InfinitePlace K) (x : K) :

‖w.embedding x‖ = w x

theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_2} [Field K] (x : K) (r : ℝ) :

(∀ (w : InfinitePlace K), w x = r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ = r

theorem NumberField.InfinitePlace.le_iff_le {K : Type u_2} [Field K] (x : K) (r : ℝ) :

(∀ (w : InfinitePlace K), w x ≤ r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

theorem NumberField.InfinitePlace.pos_iff {K : Type u_2} [Field K] {w : InfinitePlace K} {x : K} :

0 < w x ↔ x ≠ 0

@[simp]

theorem NumberField.InfinitePlace.mk_eq_iff {K : Type u_2} [Field K] {φ ψ : K →+* ℂ} :

mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

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

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

Equations

w.IsReal = ∃ (φ : K →+* ℂ), NumberField.ComplexEmbedding.IsReal φ ∧ NumberField.InfinitePlace.mk φ = w

Instances For

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

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

Equations

w.IsComplex = ∃ (φ : K →+* ℂ), ¬NumberField.ComplexEmbedding.IsReal φ ∧ NumberField.InfinitePlace.mk φ = w

Instances For

theorem NumberField.InfinitePlace.embedding_mk_eq {K : Type u_2} [Field K] (φ : K →+* ℂ) :

(mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ

@[simp]

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

(mk φ).embedding = φ

theorem NumberField.InfinitePlace.isReal_iff {K : Type u_2} [Field K] {w : InfinitePlace K} :

w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

theorem NumberField.InfinitePlace.isComplex_iff {K : Type u_2} [Field K] {w : InfinitePlace K} :

w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

@[simp]

theorem NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal {K : Type u_2} [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_2} [Field K] {w : InfinitePlace K} :

¬w.IsReal ↔ w.IsComplex

@[simp]

theorem NumberField.InfinitePlace.not_isComplex_iff_isReal {K : Type u_2} [Field K] {w : InfinitePlace K} :

¬w.IsComplex ↔ w.IsReal

theorem NumberField.InfinitePlace.isReal_or_isComplex {K : Type u_2} [Field K] (w : InfinitePlace K) :

w.IsReal ∨ w.IsComplex

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

w ≠ w'

theorem NumberField.InfinitePlace.disjoint_isReal_isComplex (K : Type u_2) [Field K] :

Disjoint {w : InfinitePlace K | w.IsReal} {w : InfinitePlace K | w.IsComplex}

noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_2} [Field K] {w : InfinitePlace K} (hw : w.IsReal) :

The real embedding associated to a real infinite place.

Equations

NumberField.InfinitePlace.embedding_of_isReal hw = ⋯.embedding

Instances For

@[simp]

theorem NumberField.InfinitePlace.embedding_of_isReal_apply {K : Type u_2} [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_2} [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_2} [Field K] {φ : K →+* ℂ} (h : (mk φ).IsReal) :

ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isReal_mk_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} :

(mk φ).IsReal ↔ ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isComplex_mk_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} :

(mk φ).IsComplex ↔ ¬ComplexEmbedding.IsReal φ

@[simp]

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

¬ComplexEmbedding.IsReal φ

noncomputable def NumberField.InfinitePlace.mult {K : Type u_2} [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.

Equations

w.mult = if w.IsReal then 1 else 2

Instances For

@[simp]

theorem NumberField.InfinitePlace.mult_isReal {K : Type u_2} [Field K] (w : { w : InfinitePlace K // w.IsReal }) :

(↑w).mult = 1

@[simp]

theorem NumberField.InfinitePlace.mult_isComplex {K : Type u_2} [Field K] (w : { w : InfinitePlace K // w.IsComplex }) :

(↑w).mult = 2

theorem NumberField.InfinitePlace.mult_pos {K : Type u_2} [Field K] {w : InfinitePlace K} :

0 < w.mult

@[simp]

theorem NumberField.InfinitePlace.mult_ne_zero {K : Type u_2} [Field K] {w : InfinitePlace K} :

theorem NumberField.InfinitePlace.mult_coe_ne_zero {K : Type u_2} [Field K] {w : InfinitePlace K} :

↑w.mult ≠ 0

theorem NumberField.InfinitePlace.one_le_mult {K : Type u_2} [Field K] {w : InfinitePlace K} :

1 ≤ ↑w.mult

theorem NumberField.InfinitePlace.card_filter_mk_eq {K : Type u_2} [Field K] [NumberField K] (w : InfinitePlace K) :

{φ : K →+* ℂ | mk φ = w}.card = w.mult

noncomputable instance NumberField.InfinitePlace.NumberField.InfinitePlace.fintype {K : Type u_2} [Field K] [NumberField K] :

Fintype (InfinitePlace K)

Equations

NumberField.InfinitePlace.NumberField.InfinitePlace.fintype = Set.fintypeRange NumberField.place

theorem NumberField.InfinitePlace.prod_eq_prod_mul_prod {K : Type u_2} [Field K] {α : Type u_4} [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_2} [Field K] {α : Type u_4} [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_2} [Field K] [NumberField K] :

∑ w : InfinitePlace K, w.mult = Module.finrank ℚ K

noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_2} [Field K] :

{ φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }

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

Equations

NumberField.InfinitePlace.mkReal = Equiv.ofBijective (fun (φ : { φ : K →+* ℂ // NumberField.ComplexEmbedding.IsReal φ }) => ⟨NumberField.InfinitePlace.mk ↑φ, ⋯⟩) ⋯

Instances For

noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_2} [Field K] :

{ φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } → { w : InfinitePlace K // w.IsComplex }

The map from nonreal embeddings to complex infinite places

Equations

NumberField.InfinitePlace.mkComplex = Subtype.map NumberField.InfinitePlace.mk ⋯

Instances For

@[simp]

theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_2} [Field K] (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) :

↑(mkReal φ) = mk ↑φ

@[simp]

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

↑(mkComplex φ) = mk ↑φ

theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_2} [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_2} [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_2} [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_2} [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_2) [Field K] [NumberField K] :

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

Equations

NumberField.InfinitePlace.nrRealPlaces K = Fintype.card { w : NumberField.InfinitePlace K // w.IsReal }

Instances For

@[deprecated NumberField.InfinitePlace.nrRealPlaces (since := "2024-10-24")]

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

Alias of NumberField.InfinitePlace.nrRealPlaces.

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

Equations

NumberField.InfinitePlace.NrRealPlaces = NumberField.InfinitePlace.nrRealPlaces

Instances For

@[reducible, inline]

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

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

Equations

NumberField.InfinitePlace.nrComplexPlaces K = Fintype.card { w : NumberField.InfinitePlace K // w.IsComplex }

Instances For

@[deprecated NumberField.InfinitePlace.nrComplexPlaces (since := "2024-10-24")]

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

Alias of NumberField.InfinitePlace.nrComplexPlaces.

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

Equations

NumberField.InfinitePlace.NrComplexPlaces = NumberField.InfinitePlace.nrComplexPlaces

Instances For

theorem NumberField.InfinitePlace.card_real_embeddings (K : Type u_2) [Field K] [NumberField K] :

Fintype.card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = nrRealPlaces K

theorem NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces (K : Type u_2) [Field K] [NumberField K] :

Fintype.card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

theorem NumberField.InfinitePlace.card_complex_embeddings (K : Type u_2) [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_2) [Field K] [NumberField K] :

nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one {K : Type u_2} [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_2} [Field K] [NumberField K] (h : Module.finrank ℚ K = 1) :

nrRealPlaces K = 1

theorem NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank {K : Type u_2} [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_2} [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 ℚ → ℂ.

Equations

Rat.infinitePlace = NumberField.InfinitePlace.mk (Rat.castHom ℂ)

Instances For

@[simp]

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

v x = ↑|x|

instance Rat.instSubsingletonInfinitePlace :

Subsingleton (NumberField.InfinitePlace ℚ)

theorem Rat.isReal_infinitePlace :

infinitePlace.IsReal