Documentation

Mathlib.NumberTheory.NumberField.Embeddings

Embeddings of number fields #

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

Main Definitions and Results #

Tags #

number field, embeddings, places, infinite places

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 φ => φ 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 .

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.

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.

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

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) :
    ↑(NumberField.place φ) x = φ x
    @[reducible]

    The conjugate of a complex embedding as a complex embedding.

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

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

      Instances For

        A real embedding as a ring homomorphism from K to .

        Instances For
          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.

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

            Return the infinite place defined by a complex embedding φ.

            Instances For
              @[simp]
              theorem NumberField.InfinitePlace.apply {K : Type u_1} [Field K] (φ : K →+* ) (x : K) :

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

              Instances For
                theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_1} [Field K] (x : K) (r : ) :
                (∀ (w : NumberField.InfinitePlace K), w x = r) ∀ (φ : K →+* ), φ x = r
                theorem NumberField.InfinitePlace.le_iff_le {K : Type u_1} [Field K] (x : K) (r : ) :
                (∀ (w : NumberField.InfinitePlace K), w x r) ∀ (φ : K →+* ), φ x r
                theorem NumberField.InfinitePlace.pos_iff {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} {x : K} :
                0 < w x x 0

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

                Instances For

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

                  Instances For

                    The real embedding associated to a real infinite place.

                    Instances For
                      noncomputable def NumberField.InfinitePlace.mult {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) :

                      The multiplicity of an infinite place, that is the number of distinct complex embeddings that define it, see card_filter_mk_eq.

                      Instances For

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

                        Instances For

                          The map from nonreal embeddings to complex infinite places

                          Instances For
                            @[simp]
                            theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_1} [Field K] (φ : { φ // NumberField.ComplexEmbedding.IsReal φ }) :
                            ↑(NumberField.InfinitePlace.mkReal φ) = NumberField.InfinitePlace.mk φ
                            theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_1} [Field K] [NumberField K] (x : K) :
                            (Finset.prod Finset.univ fun w => w x ^ NumberField.InfinitePlace.mult w) = |↑(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.