Embeddings of number fields #

This file defines the embeddings of a number field into an algebraic closed field.

Main Definitions and Results #

NumberField.Embeddings.range_eval_eq_rootSet_minpoly: let x ∈ K with K number field and let A be an algebraic closed field of char. 0, then the images of x by 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_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.
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.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.

Tags #

number field, embeddings, places, infinite places

noncomputable instance NumberField.Embeddings.instFintypeRingHomToNonAssocSemiringToSemiringToDivisionSemiringToSemifieldToNonAssocSemiringToSemiringToDivisionSemiringToSemifield (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] :

Fintype (K →+* A)

There are finitely many embeddings of a number field.

Equations

One or more equations did not get rendered due to their size.

source

theorem NumberField.Embeddings.card (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] [IsAlgClosed A] :

Fintype.card (K →+* A) = FiniteDimensional.finrank ℚ K

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

source

instance NumberField.Embeddings.instNonemptyRingHomToNonAssocSemiringToSemiringToDivisionSemiringToSemifieldToNonAssocSemiringToSemiringToDivisionSemiringToSemifield (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] [IsAlgClosed A] :

Nonempty (K →+* A)

Equations

One or more equations did not get rendered due to their size.

source

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 φ => ↑φ x) = Polynomial.rootSet (minpoly ℚ x) 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 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 : ℕ) :

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

source

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 : ℝ) :

Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}

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 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 x, x ^ n = 1

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

source

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

Equations

NumberField.place φ = AbsoluteValue.comp (IsAbsoluteValue.toAbsoluteValue norm) (_ : Function.Injective ↑φ)

Instances For

source

@[simp]

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

↑(NumberField.place φ) x = ‖↑φ x‖

source

@[reducible]

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

K →+* ℂ

The conjugate of a complex embedding as a complex embedding.

Equations

NumberField.ComplexEmbedding.conjugate φ = star φ

Instances For

source

@[simp]

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

↑(NumberField.ComplexEmbedding.conjugate φ) x = ↑(starRingEnd ((fun x => ℂ) x)) (↑φ x)

source

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

NumberField.place (NumberField.ComplexEmbedding.conjugate φ) = NumberField.place φ

source

@[reducible]

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

Prop

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

Equations

NumberField.ComplexEmbedding.IsReal φ = IsSelfAdjoint φ

Instances For

source

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

NumberField.ComplexEmbedding.IsReal φ ↔ NumberField.ComplexEmbedding.conjugate φ = φ

source

theorem NumberField.ComplexEmbedding.isReal_conjugate_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} :

NumberField.ComplexEmbedding.IsReal (NumberField.ComplexEmbedding.conjugate φ) ↔ NumberField.ComplexEmbedding.IsReal φ

source

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

K →+* ℝ

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

↑(↑(NumberField.ComplexEmbedding.IsReal.embedding hφ) x) = ↑φ x

source

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.

Equations

NumberField.InfinitePlace K = { w // ∃ φ, NumberField.place φ = w }

Instances For

source

instance instNonemptyInfinitePlace (K : Type u_1) [Field K] [NumberField K] :

Nonempty (NumberField.InfinitePlace K)

Equations

instNonemptyInfinitePlace = instNonemptyInfinitePlace.proof_1

source

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

NumberField.InfinitePlace K

Return the infinite place defined by a complex embedding φ.

Equations

NumberField.InfinitePlace.mk φ = { val := NumberField.place φ, property := (_ : ∃ φ, NumberField.place φ = NumberField.place φ) }

Instances For

source

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

FunLike (NumberField.InfinitePlace K) K fun x => ℝ

Equations

One or more equations did not get rendered due to their size.

source

instance NumberField.InfinitePlace.instMonoidWithZeroHomClassInfinitePlaceRealToMulZeroOneClassToNonAssocSemiringToSemiringToDivisionSemiringToSemifieldToMulZeroOneClassToNonAssocSemiringSemiring {K : Type u_1} [Field K] :

MonoidWithZeroHomClass (NumberField.InfinitePlace K) K ℝ

Equations

One or more equations did not get rendered due to their size.

source

instance NumberField.InfinitePlace.instNonnegHomClassInfinitePlaceRealInstZeroRealInstLEReal {K : Type u_1} [Field K] :

NonnegHomClass (NumberField.InfinitePlace K) K ℝ

Equations

NumberField.InfinitePlace.instNonnegHomClassInfinitePlaceRealInstZeroRealInstLEReal = NonnegHomClass.mk (_ : ∀ (w : NumberField.InfinitePlace K) (x : K), 0 ≤ ↑↑w x)