Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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 #

Tags #

number field, embeddings

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

There are finitely many embeddings of a number field.

Equations

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

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

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

Equations
Instances For
    @[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 →+* ) :

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

    Equations
    Instances For
      @[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]

      The conjugate of a complex embedding as a complex embedding.

      Equations
      Instances For
        @[simp]
        theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [Field K] (φ : K →+* ) (x : K) :
        (conjugate φ) x = (starRingEnd ) (φ x)
        @[reducible, inline]

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

        Equations
        Instances For

          A real embedding as a ring homomorphism from K to .

          Equations
          • .embedding = { toFun := fun (x : K) => (φ x).re, map_one' := , map_mul' := , map_zero' := , map_add' := }
          Instances For
            @[simp]
            theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply {K : Type u_1} [Field K] {φ : K →+* } ( : IsReal φ) (x : K) :
            (.embedding x) = φ x
            theorem NumberField.ComplexEmbedding.IsReal.comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] (f : k →+* K) {φ : K →+* } ( : 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)) :
            ∃ (σ : K ≃ₐ[k] K), φ.comp σ.symm = ψ
            def NumberField.ComplexEmbedding.IsConj {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] (φ : K →+* ) (σ : K ≃ₐ[k] K) :

            IsConj φ σ states that σ : K ≃ₐ[k] K is the conjugation under the embedding φ : K →+* ℂ.

            Equations
            Instances For
              theorem NumberField.ComplexEmbedding.IsConj.eq {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[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 →+* } {σ₁ σ₂ : K ≃ₐ[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 →+* } {σ₁ σ₂ : K ≃ₐ[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 →+* } {σ : K ≃ₐ[k] K} (h : IsConj φ σ) :
              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.symm {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[k] K} ( : IsConj φ σ) :
              IsConj φ σ.symm
              theorem NumberField.ComplexEmbedding.isConj_symm {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[k] K} :
              IsConj φ σ.symm IsConj φ σ