Embeddings of number fields

This file defines the embeddings of a number field and, in particular, the embeddings into the field of complex numbers.

Main Definitions and Results

• NumberField.Embeddings.range_eval_eq_rootSet_minpoly: let x ∈ K with K a number field and let A be an algebraically closed field of char. 0. Then the images of x under the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.
• NumberField.Embeddings.pow_eq_one_of_norm_le_one: A non-zero algebraic integer whose conjugates are all inside the closed unit disk is a root of unity, this is also known as Kronecker's theorem.
• NumberField.Embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.

Tags

number field, embeddings

instance NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [CharZero K] [Algebra.IsAlgebraic ℚ K] [IsAlgClosed A] : Nonempty (K →+* A)

noncomputable instance NumberField.Embeddings.instFintypeRingHom (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [NumberField K] : Fintype (K →+* A)

There are finitely many embeddings of a number field.

theorem NumberField.Embeddings.card (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [NumberField K] [IsAlgClosed A] : Fintype.card (K →+* A) = Module.finrank ℚ K

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

instance NumberField.Embeddings.instNonemptyRingHom (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [NumberField K] [IsAlgClosed A] : Nonempty (K →+* A)

theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly (K : Type u_1) (A : Type u_2) [Field K] [NumberField K] [Field A] [Algebra ℚ A] [IsAlgClosed A] (x : K) : (Set.range fun (φ : K →+* A) => φ x) = (minpoly ℚ x).rootSet 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 ℚ.

theorem NumberField.Embeddings.coeff_bdd_of_norm_le {K : Type u_1} [Field K] [NumberField K] {A : Type u_2} [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {B : ℝ} {x : K} (h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B) (i : ℕ) : ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ Module.finrank ℚ K * ↑((Module.finrank ℚ K).choose (Module.finrank ℚ K / 2))

theorem NumberField.Embeddings.finite_of_norm_le (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] (B : ℝ) : {x : K | IsIntegral ℤ 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.

theorem NumberField.Embeddings.pow_eq_one_of_norm_le_one (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x) (hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1) : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Kronecker's Theorem: A non-zero algebraic integer whose conjugates are all inside the closed unit disk is a root of unity.

theorem NumberField.Embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ (φ : K →+* A), ‖φ x‖ = 1) : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

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

def NumberField.place {K : Type u_1} [Field K] {A : Type u_2} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A) : AbsoluteValue K ℝ

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

@[simp]

theorem NumberField.place_apply {K : Type u_1} [Field K] {A : Type u_2} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A) (x : K) : (place φ) x = ‖φ x‖

noncomputable def NumberField.ComplexEmbedding.lift (K : Type u_1) [Field K] {k : Type u_2} [Field k] [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) : K →+* ℂ

A (random) lift of the complex embedding φ : k →+* ℂ to an extension K of k.

@[simp]

theorem NumberField.ComplexEmbedding.lift_comp_algebraMap (K : Type u_1) [Field K] {k : Type u_2} [Field k] [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) : (lift K φ).comp (algebraMap k K) = φ

@[simp]

theorem NumberField.ComplexEmbedding.lift_algebraMap_apply (K : Type u_1) [Field K] {k : Type u_2} [Field k] [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) (x : k) : (lift K φ) ((algebraMap k K) x) = φ x

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.conjugate {K : Type u_1} [Field K] (φ : K →+* ℂ) : K →+* ℂ

The conjugate of a complex embedding as a complex embedding.

@[simp]

theorem NumberField.ComplexEmbedding.conjugate_comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] (φ : K →+* ℂ) (σ : k →+* K) : (conjugate φ).comp σ = conjugate (φ.comp σ)

theorem NumberField.ComplexEmbedding.involutive_conjugate (K : Type u_1) [Field K] : Function.Involutive conjugate

@[simp]

theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [Field K] (φ : K →+* ℂ) (x : K) : (conjugate φ) x = (starRingEnd ℂ) (φ x)

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

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.IsReal {K : Type u_1} [Field K] (φ : K →+* ℂ) : Prop

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

theorem NumberField.ComplexEmbedding.isReal_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : IsReal φ ↔ conjugate φ = φ

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

def NumberField.ComplexEmbedding.IsReal.embedding {K : Type u_1} [Field K] {φ : K →+* ℂ} (hφ : IsReal φ) : K →+* ℝ

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

@[simp]

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

theorem NumberField.ComplexEmbedding.IsReal.comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] (f : k →+* K) {φ : K →+* ℂ} (hφ : IsReal φ) : IsReal (φ.comp f)

theorem NumberField.ComplexEmbedding.isReal_comp_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] {f : k ≃+* K} {φ : K →+* ℂ} : IsReal (φ.comp ↑f) ↔ IsReal φ

theorem NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsGalois k K] (φ ψ : K →+* ℂ) (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) : ∃ (σ : Gal(K/k)), φ.comp ↑σ.symm = ψ

def NumberField.ComplexEmbedding.IsConj {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] (φ : K →+* ℂ) (σ : Gal(K/k)) : Prop

IsConj φ σ states that σ : Gal(K/k) is the conjugation under the embedding φ : K →+* ℂ.

theorem NumberField.ComplexEmbedding.IsConj.eq {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (h : IsConj φ σ) (x : K) : φ (σ x) = star (φ x)

theorem NumberField.ComplexEmbedding.IsConj.ext {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ₁ σ₂ : Gal(K/k)} (h₁ : IsConj φ σ₁) (h₂ : IsConj φ σ₂) : σ₁ = σ₂

theorem NumberField.ComplexEmbedding.IsConj.ext_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ₁ σ₂ : Gal(K/k)} (h₁ : IsConj φ σ₁) : σ₁ = σ₂ ↔ IsConj φ σ₂

theorem NumberField.ComplexEmbedding.IsConj.isReal_comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (h : IsConj φ σ) : IsReal (φ.comp (algebraMap k K))

theorem NumberField.ComplexEmbedding.isConj_one_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} : IsConj φ 1 ↔ IsReal φ

theorem NumberField.ComplexEmbedding.IsReal.isConjGal_one {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} : IsReal φ → IsConj φ 1

Alias of the reverse direction of NumberField.ComplexEmbedding.isConj_one_iff.

theorem NumberField.ComplexEmbedding.isConj_ne_one_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (hσ : IsConj φ σ) : σ ≠ 1 ↔ ¬IsReal φ

theorem NumberField.ComplexEmbedding.IsConj.symm {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (hσ : IsConj φ σ) : IsConj φ σ.symm

theorem NumberField.ComplexEmbedding.isConj_symm {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} : IsConj φ σ.symm ↔ IsConj φ σ

theorem NumberField.ComplexEmbedding.isConj_apply_apply {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (hσ : IsConj φ σ) (x : K) : σ (σ x) = x

theorem NumberField.ComplexEmbedding.IsConj.comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (hσ : IsConj φ σ) (ν : Gal(K/k)) : IsConj (φ.comp ↑ν) (ν⁻¹ * σ * ν)

theorem NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)} (hσ : IsConj φ σ) (hσ' : σ ≠ 1) : orderOf σ = 2

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.Extension {K : Type u_3} (L : Type u_4) [Field K] [Field L] (ψ : K →+* ℂ) [Algebra K L] : Type u_4

If L/K and ψ : K →+* ℂ, then the type of ComplexEmbedding.Extension L ψ consists of all φ : L →+* ℂ such that φ.comp (algebraMap K L) = ψ.

theorem NumberField.ComplexEmbedding.Extension.comp_eq {K : Type u_3} {L : Type u_4} [Field K] [Field L] {ψ : K →+* ℂ} [Algebra K L] (φ : ComplexEmbedding.Extension L ψ) : (↑φ).comp (algebraMap K L) = ψ

theorem NumberField.ComplexEmbedding.Extension.conjugate_comp_ne {K : Type u_3} {L : Type u_4} [Field K] [Field L] {ψ : K →+* ℂ} [Algebra K L] (φ : ComplexEmbedding.Extension L ψ) (h : ¬IsReal ψ) : (conjugate ↑φ).comp (algebraMap K L) ≠ ψ

theorem NumberField.ComplexEmbedding.Extension.not_isReal_of_not_isReal {K : Type u_3} {L : Type u_4} [Field K] [Field L] {ψ : K →+* ℂ} [Algebra K L] (φ : ComplexEmbedding.Extension L ψ) (h : ¬IsReal ψ) : ¬IsReal ↑φ

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.IsMixed (K : Type u_3) {L : Type u_4} [Field K] [Field L] [Algebra K L] (φ : L →+* ℂ) : Prop

If L/K and φ : L →+* ℂ, then IsMixed K φ if the image of φ is complex while the image of φ restricted to K is real.

This is the complex embedding analogue of InfinitePlace.IsRamified K w, where w : InfinitePlace L. It is not the same concept because conjugation of φ in this case leads to two distinct mixed embeddings but only a single ramified place w, leading to a two-to-one isomorphism between them.

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.IsUnmixed (K : Type u_3) {L : Type u_4} [Field K] [Field L] [Algebra K L] (φ : L →+* ℂ) : Prop

If L/K and φ : L →+* ℂ, then IsMixed K φ if φ is not mixed in K, i.e., φ is real if and only if it's restriction to K is.

This is the complex embedding analogue of InfinitePlace.IsUnramified K w, where w : InfinitePlace L. In this case there is an isomorphism between unmixed embeddings and unramified infinite places.

theorem NumberField.ComplexEmbedding.IsUnmixed.isReal_iff_isReal (K : Type u_3) {L : Type u_4} [Field K] [Field L] [Algebra K L] {φ : L →+* ℂ} (h : IsUnmixed K φ) : IsReal (φ.comp (algebraMap K L)) ↔ IsReal φ