number_theory.number_field.embeddings

@[protected, instance]

noncomputable def number_field.embeddings.ring_hom.fintype (K : Type u_1) [field K] [number_field K] (A : Type u_2) [field A] [char_zero A] :

fintype (K →+* A)

There are finitely many embeddings of a number field.

Equations

number_field.embeddings.ring_hom.fintype K A = fintype.of_equiv (K →ₐ[ℚ ] A) ring_hom.equiv_rat_alg_hom.symm

source

theorem number_field.embeddings.card (K : Type u_1) [field K] [number_field K] (A : Type u_2) [field A] [char_zero A] [is_alg_closed A] :

fintype.card (K →+* A) = finite_dimensional.finrank ℚ K

The number of embeddings of a number field is equal to its finrank.

source

@[protected, instance]

def number_field.embeddings.ring_hom.nonempty (K : Type u_1) [field K] [number_field K] (A : Type u_2) [field A] [char_zero A] [is_alg_closed A] :

nonempty (K →+* A)

source

theorem number_field.embeddings.range_eval_eq_root_set_minpoly (K : Type u_1) (A : Type u_2) [field K] [number_field K] [field A] [algebra ℚ A] [is_alg_closed A] (x : K) :

set.range (λ (φ : K →+* A), ⇑φ x) = (minpoly ℚ x).root_set A

Let A be an algebraically closed field and let x ∈ K, with K a number field. The images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.

source

theorem number_field.embeddings.coeff_bdd_of_norm_le {K : Type u_1} [field K] [number_field K] {A : Type u_2} [normed_field A] [is_alg_closed A] [normed_algebra ℚ A] {B : ℝ} {x : K} (h : ∀ (φ : K →+* A), ‖⇑φ x‖ ≤ B) (i : ℕ) :

‖(minpoly ℚ x).coeff i‖ ≤ linear_order.max B 1 ^ finite_dimensional.finrank ℚ K * ↑((finite_dimensional.finrank ℚ K).choose (finite_dimensional.finrank ℚ K / 2))

source

theorem number_field.embeddings.finite_of_norm_le (K : Type u_1) [field K] [number_field K] (A : Type u_2) [normed_field A] [is_alg_closed A] [normed_algebra ℚ A] (B : ℝ) :

{x : K | is_integral ℤ x ∧ ∀ (φ : K →+* A), ‖⇑φ x‖ ≤ B}.finite

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

source

theorem number_field.embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [field K] [number_field K] (A : Type u_2) [normed_field A] [is_alg_closed A] [normed_algebra ℚ A] {x : K} (hxi : is_integral ℤ x) (hx : ∀ (φ : K →+* A), ‖⇑φ x‖ = 1) :

∃ (n : ℕ) (hn : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

source

def number_field.place {K : Type u_1} [field K] {A : Type u_2} [normed_division_ring A] [nontrivial A] (φ : K →+* A) :

absolute_value K ℝ

An embedding into a normed division ring defines a place of K

Equations

number_field.place φ = (is_absolute_value.to_absolute_value has_norm.norm).comp _

source

@[simp]

theorem number_field.place_apply {K : Type u_1} [field K] {A : Type u_2} [normed_division_ring A] [nontrivial A] (φ : K →+* A) (x : K) :

⇑(number_field.place φ) x = ‖⇑φ x‖

source

@[reducible]

def number_field.complex_embedding.conjugate {K : Type u_1} [field K] (φ : K →+* ℂ) :

K →+* ℂ

The conjugate of a complex embedding as a complex embedding.

Equations

number_field.complex_embedding.conjugate φ = has_star.star φ

source

@[simp]

theorem number_field.complex_embedding.conjugate_coe_eq {K : Type u_1} [field K] (φ : K →+* ℂ) (x : K) :

⇑(number_field.complex_embedding.conjugate φ) x = ⇑(star_ring_end ℂ) (⇑φ x)

source

theorem number_field.complex_embedding.place_conjugate {K : Type u_1} [field K] (φ : K →+* ℂ) :

number_field.place (number_field.complex_embedding.conjugate φ) = number_field.place φ

source

@[reducible]

def number_field.complex_embedding.is_real {K : Type u_1} [field K] (φ : K →+* ℂ) :

Prop

A embedding into ℂ is real if it is fixed by complex conjugation.

Equations

number_field.complex_embedding.is_real φ = is_self_adjoint φ

source

theorem number_field.complex_embedding.is_real_iff {K : Type u_1} [field K] {φ : K →+* ℂ} :

number_field.complex_embedding.is_real φ ↔ number_field.complex_embedding.conjugate φ = φ

source

def number_field.complex_embedding.is_real.embedding {K : Type u_1} [field K] {φ : K →+* ℂ} (hφ : number_field.complex_embedding.is_real φ) :

K →+* ℝ

A real embedding as a ring homomorphism from K to ℝ .

Equations

hφ.embedding = {to_fun := λ (x : K), (⇑φ x).re, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem number_field.complex_embedding.is_real.coe_embedding_apply {K : Type u_1} [field K] {φ : K →+* ℂ} (hφ : number_field.complex_embedding.is_real φ) (x : K) :

↑(⇑(hφ.embedding) x) = ⇑φ x

source

theorem number_field.complex_embedding.is_real.place_embedding {K : Type u_1} [field K] {φ : K →+* ℂ} (hφ : number_field.complex_embedding.is_real φ) :

number_field.place hφ.embedding = number_field.place φ

source

theorem number_field.complex_embedding.is_real_conjugate_iff {K : Type u_1} [field K] {φ : K →+* ℂ} :

number_field.complex_embedding.is_real (number_field.complex_embedding.conjugate φ) ↔ number_field.complex_embedding.is_real φ

source

def number_field.infinite_place (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.

Equations

number_field.infinite_place K = {w // ∃ (φ : K →+* ℂ), number_field.place φ = w}

Instances for number_field.infinite_place

source

@[protected, instance]

def number_field.infinite_place.nonempty (K : Type u_1) [field K] [number_field K] :

nonempty (number_field.infinite_place K)

source

noncomputable def number_field.infinite_place.mk {K : Type u_1} [field K] (φ : K →+* ℂ) :

number_field.infinite_place K

Return the infinite place defined by a complex embedding φ.

Equations

number_field.infinite_place.mk φ = ⟨number_field.place φ, _⟩

source

@[protected, instance]

def number_field.infinite_place.has_coe_to_fun {K : Type u_1} [field K] :

has_coe_to_fun (number_field.infinite_place K) (λ (_x : number_field.infinite_place K), K → ℝ)

Equations

number_field.infinite_place.has_coe_to_fun = {coe := λ (w : number_field.infinite_place K), ⇑(w.val)}

source

@[protected, instance]

def number_field.infinite_place.real.monoid_with_zero_hom_class {K : Type u_1} [field K] :

monoid_with_zero_hom_class (number_field.infinite_place K) K ℝ

Equations

number_field.infinite_place.real.monoid_with_zero_hom_class = {coe := λ (w : number_field.infinite_place K) (x : K), ⇑(w.val) x, coe_injective' := _, map_mul := _, map_one := _, map_zero := _}

source

@[protected, instance]

def number_field.infinite_place.real.nonneg_hom_class {K : Type u_1} [field K] :

nonneg_hom_class (number_field.infinite_place K) K ℝ

Equations

number_field.infinite_place.real.nonneg_hom_class = {coe := λ (w : number_field.infinite_place K) (x : K), ⇑w x, coe_injective' := _, map_nonneg := _}

source

theorem number_field.infinite_place.coe_mk {K : Type u_1} [field K] (φ : K →+* ℂ) :

⇑(number_field.infinite_place.mk φ) = ⇑(number_field.place φ)

source

theorem number_field.infinite_place.apply {K : Type u_1} [field K] (φ : K →+* ℂ) (x : K) :

⇑(number_field.infinite_place.mk φ) x = ⇑complex.abs (⇑φ x)

source

noncomputable def number_field.infinite_place.embedding {K : Type u_1} [field K] (w : number_field.infinite_place K) :

K →+* ℂ

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

Equations

w.embedding = Exists.some _

source

@[simp]

theorem number_field.infinite_place.mk_embedding {K : Type u_1} [field K] (w : number_field.infinite_place K) :

number_field.infinite_place.mk w.embedding = w

source

@[simp]

theorem number_field.infinite_place.abs_embedding {K : Type u_1} [field K] (w : number_field.infinite_place K) (x : K) :

⇑complex.abs (⇑(w.embedding) x) = ⇑w x

source

theorem number_field.infinite_place.eq_iff_eq {K : Type u_1} [field K] (x : K) (r : ℝ) :

(∀ (w : number_field.infinite_place K), ⇑w x = r) ↔ ∀ (φ : K →+* ℂ), ‖⇑φ x‖ = r

source

theorem number_field.infinite_place.le_iff_le {K : Type u_1} [field K] (x : K) (r : ℝ) :

(∀ (w : number_field.infinite_place K), ⇑w x ≤ r) ↔ ∀ (φ : K →+* ℂ), ‖⇑φ x‖ ≤ r

source

theorem number_field.infinite_place.pos_iff {K : Type u_1} [field K] {w : number_field.infinite_place K} {x : K} :

0 < ⇑w x ↔ x ≠ 0

source

@[simp]

theorem number_field.infinite_place.mk_conjugate_eq {K : Type u_1} [field K] (φ : K →+* ℂ) :

number_field.infinite_place.mk (number_field.complex_embedding.conjugate φ) = number_field.infinite_place.mk φ

source

@[simp]

theorem number_field.infinite_place.mk_eq_iff {K : Type u_1} [field K] {φ ψ : K →+* ℂ} :

number_field.infinite_place.mk φ = number_field.infinite_place.mk ψ ↔ φ = ψ ∨ number_field.complex_embedding.conjugate φ = ψ

source

def number_field.infinite_place.is_real {K : Type u_1} [field K] (w : number_field.infinite_place K) :

Prop

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

Equations

w.is_real = ∃ (φ : K →+* ℂ), number_field.complex_embedding.is_real φ ∧ number_field.infinite_place.mk φ = w

source

def number_field.infinite_place.is_complex {K : Type u_1} [field K] (w : number_field.infinite_place K) :

Prop

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

Equations

w.is_complex = ∃ (φ : K →+* ℂ), ¬number_field.complex_embedding.is_real φ ∧ number_field.infinite_place.mk φ = w

source

@[simp]

theorem number_field.complex_embeddings.is_real.embedding_mk {K : Type u_1} [field K] {φ : K →+* ℂ} (h : number_field.complex_embedding.is_real φ) :

(number_field.infinite_place.mk φ).embedding = φ

source

theorem number_field.infinite_place.is_real_iff {K : Type u_1} [field K] {w : number_field.infinite_place K} :

w.is_real ↔ number_field.complex_embedding.is_real w.embedding

source

theorem number_field.infinite_place.is_complex_iff {K : Type u_1} [field K] {w : number_field.infinite_place K} :

w.is_complex ↔ ¬number_field.complex_embedding.is_real w.embedding

source

@[simp]

theorem number_field.infinite_place.not_is_real_iff_is_complex {K : Type u_1} [field K] {w : number_field.infinite_place K} :

¬w.is_real ↔ w.is_complex

source

@[simp]

theorem number_field.infinite_place.not_is_complex_iff_is_real {K : Type u_1} [field K] {w : number_field.infinite_place K} :

¬w.is_complex ↔ w.is_real

source

theorem number_field.infinite_place.is_real_or_is_complex {K : Type u_1} [field K] (w : number_field.infinite_place K) :

w.is_real ∨ w.is_complex

source

noncomputable def number_field.infinite_place.is_real.embedding {K : Type u_1} [field K] {w : number_field.infinite_place K} (hw : w.is_real) :

K →+* ℝ

For w a real infinite place, return the corresponding embedding as a morphism K →+* ℝ.

Equations

hw.embedding = _.embedding

source

@[simp]

theorem number_field.infinite_place.is_real.place_embedding_apply {K : Type u_1} [field K] {w : number_field.infinite_place K} (hw : w.is_real) (x : K) :

⇑(number_field.place hw.embedding) x = ⇑w x

source

@[simp]

theorem number_field.infinite_place.is_real.abs_embedding_apply {K : Type u_1} [field K] {w : number_field.infinite_place K} (hw : w.is_real) (x : K) :

|⇑(hw.embedding) x| = ⇑w x

source

noncomputable def number_field.infinite_place.mk_real (K : Type u_1) [field K] :

{φ // number_field.complex_embedding.is_real φ} ≃ {w // w.is_real}

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

Equations

number_field.infinite_place.mk_real K = {to_fun := subtype.map number_field.infinite_place.mk _, inv_fun := λ (w : {w // w.is_real}), ⟨w.val.embedding, _⟩, left_inv := _, right_inv := _}

source

noncomputable def number_field.infinite_place.mk_complex (K : Type u_1) [field K] :

{φ // ¬number_field.complex_embedding.is_real φ} → {w // w.is_complex}

The map from nonreal embeddings to complex infinite places

Equations

number_field.infinite_place.mk_complex K = subtype.map number_field.infinite_place.mk _

source

theorem number_field.infinite_place.mk_complex_embedding (K : Type u_1) [field K] (φ : {φ // ¬number_field.complex_embedding.is_real φ}) :

↑(number_field.infinite_place.mk_complex K φ).embedding = ↑φ ∨ ↑(number_field.infinite_place.mk_complex K φ).embedding = number_field.complex_embedding.conjugate ↑φ

source

@[simp]

theorem number_field.infinite_place.mk_real_coe (K : Type u_1) [field K] (φ : {φ // number_field.complex_embedding.is_real φ}) :

↑(⇑(number_field.infinite_place.mk_real K) φ) = number_field.infinite_place.mk ↑φ

source

@[simp]

theorem number_field.infinite_place.mk_complex_coe (K : Type u_1) [field K] (φ : {φ // ¬number_field.complex_embedding.is_real φ}) :

↑(number_field.infinite_place.mk_complex K φ) = number_field.infinite_place.mk ↑φ

source

@[simp]

theorem number_field.infinite_place.mk_real.apply (K : Type u_1) [field K] (φ : {φ // number_field.complex_embedding.is_real φ}) (x : K) :

⇑(⇑(number_field.infinite_place.mk_real K) φ) x = ⇑complex.abs (⇑φ x)

source

@[simp]

theorem number_field.infinite_place.mk_complex.apply (K : Type u_1) [field K] (φ : {φ // ¬number_field.complex_embedding.is_real φ}) (x : K) :

⇑(number_field.infinite_place.mk_complex K φ) x = ⇑complex.abs (⇑φ x)

source

theorem number_field.infinite_place.mk_complex.filter (K : Type u_1) [field K] [number_field K] (w : {w // w.is_complex}) :

finset.filter (λ (φ : {φ // ¬number_field.complex_embedding.is_real φ}), number_field.infinite_place.mk_complex K φ = w) finset.univ = {⟨w.val.embedding, _⟩, ⟨number_field.complex_embedding.conjugate w.val.embedding, _⟩}

source

theorem number_field.infinite_place.mk_complex.filter_card (K : Type u_1) [field K] [number_field K] (w : {w // w.is_complex}) :

(finset.filter (λ (φ : {φ // ¬number_field.complex_embedding.is_real φ}), number_field.infinite_place.mk_complex K φ = w) finset.univ).card = 2

source

@[protected, instance]

noncomputable def number_field.infinite_place.number_field.infinite_place.fintype (K : Type u_1) [field K] [number_field K] :

fintype (number_field.infinite_place K)

Equations

number_field.infinite_place.number_field.infinite_place.fintype K = set.fintype_range (λ (φ : K →+* ℂ), number_field.place φ)

source

theorem number_field.infinite_place.prod_eq_abs_norm (K : Type u_1) [field K] [number_field K] (x : K) :

finset.univ.prod (λ (w : number_field.infinite_place K), ite w.is_real (⇑w x) (⇑w x ^ 2)) = |↑(⇑(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.

source

theorem number_field.infinite_place.card_real_embeddings (K : Type u_1) [field K] [number_field K] :

fintype.card {φ // number_field.complex_embedding.is_real φ} = fintype.card {w // w.is_real}

source

theorem number_field.infinite_place.card_complex_embeddings (K : Type u_1) [field K] [number_field K] :

fintype.card {φ // ¬number_field.complex_embedding.is_real φ} = 2 * fintype.card {w // w.is_complex}

mathlib3 documentation

Embeddings of number fields #

Main Results #

Tags #