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

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.

Equations
  • =
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_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) :
    @[reducible, inline]

    The conjugate of a complex embedding as a complex embedding.

    Equations
    Instances For
      @[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 →+* } (hφ : NumberField.ComplexEmbedding.IsReal φ) (x : K) :
          (.embedding x) = φ x
          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 →+* ) (ψ : 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 : NumberField.ComplexEmbedding.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} {σ₂ : K ≃ₐ[k] K} (h₁ : NumberField.ComplexEmbedding.IsConj φ σ₁) (h₂ : NumberField.ComplexEmbedding.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} {σ₂ : K ≃ₐ[k] K} (h₁ : NumberField.ComplexEmbedding.IsConj φ σ₁) :
            def NumberField.InfinitePlace (K : Type u_2) [Field K] :
            Type (max 0 u_2)

            An infinite place of a number field K is a place associated to a complex embedding.

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

              Return the infinite place defined by a complex embedding φ.

              Equations
              Instances For
                Equations
                • NumberField.InfinitePlace.instFunLikeReal = { coe := fun (w : NumberField.InfinitePlace K) (x : K) => w x, coe_injective' := }
                @[simp]
                theorem NumberField.InfinitePlace.apply {K : Type u_2} [Field K] (φ : K →+* ) (x : K) :
                (NumberField.InfinitePlace.mk φ) x = Complex.abs (φ x)

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

                Equations
                • w.embedding = .choose
                Instances For
                  theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) (x : K) :
                  w.embedding x = w x
                  theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_2} [Field K] (x : K) (r : ) :
                  (∀ (w : NumberField.InfinitePlace K), w x = r) ∀ (φ : K →+* ), φ x = r
                  theorem NumberField.InfinitePlace.le_iff_le {K : Type u_2} [Field K] (x : K) (r : ) :
                  (∀ (w : NumberField.InfinitePlace K), w x r) ∀ (φ : K →+* ), φ x r
                  theorem NumberField.InfinitePlace.pos_iff {K : Type u_2} [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.

                  Equations
                  Instances For

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

                    Equations
                    Instances For
                      @[simp]
                      @[simp]
                      theorem NumberField.InfinitePlace.ne_of_isReal_isComplex {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} {w' : NumberField.InfinitePlace K} (h : w.IsReal) (h' : w'.IsComplex) :
                      w w'
                      noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) :

                      The real embedding associated to a real infinite place.

                      Equations
                      Instances For
                        @[simp]
                        noncomputable def NumberField.InfinitePlace.mult {K : Type u_2} [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.

                        Equations
                        • w.mult = if w.IsReal then 1 else 2
                        Instances For
                          Equations
                          • NumberField.InfinitePlace.NumberField.InfinitePlace.fintype = Set.fintypeRange NumberField.place
                          noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_2} [Field K] :

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

                          Equations
                          Instances For
                            noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_2} [Field K] :
                            { φ : K →+* // ¬NumberField.ComplexEmbedding.IsReal φ }{ w : NumberField.InfinitePlace K // w.IsComplex }

                            The map from nonreal embeddings to complex infinite places

                            Equations
                            • NumberField.InfinitePlace.mkComplex = Subtype.map NumberField.InfinitePlace.mk
                            Instances For
                              @[simp]
                              theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_2} [Field K] (φ : { φ : K →+* // NumberField.ComplexEmbedding.IsReal φ }) :
                              (NumberField.InfinitePlace.mkReal φ) = NumberField.InfinitePlace.mk φ
                              theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_2} [Field K] [NumberField K] (x : K) :
                              w : NumberField.InfinitePlace K, w x ^ w.mult = |(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.

                              theorem NumberField.InfinitePlace.one_le_of_lt_one {K : Type u_2} [Field K] [NumberField K] {w : NumberField.InfinitePlace K} {a : NumberField.RingOfIntegers K} (ha : a 0) (h : ∀ ⦃z : NumberField.InfinitePlace K⦄, z wz a < 1) :
                              1 w a
                              theorem NumberField.is_primitive_element_of_infinitePlace_lt {K : Type u_2} [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} {w : NumberField.InfinitePlace K} (h₁ : x 0) (h₂ : ∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ww' x < 1) (h₃ : w.IsReal |(w.embedding x).re| < 1) :
                              x =
                              theorem NumberField.adjoin_eq_top_of_infinitePlace_lt {K : Type u_2} [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} {w : NumberField.InfinitePlace K} (h₁ : x 0) (h₂ : ∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ww' x < 1) (h₃ : w.IsReal |(w.embedding x).re| < 1) :
                              @[reducible, inline]
                              noncomputable abbrev NumberField.InfinitePlace.NrRealPlaces (K : Type u_2) [Field K] [NumberField K] :

                              The number of infinite real places of the number field K.

                              Equations
                              Instances For
                                @[reducible, inline]
                                noncomputable abbrev NumberField.InfinitePlace.NrComplexPlaces (K : Type u_2) [Field K] [NumberField K] :

                                The number of infinite complex places of the number field K.

                                Equations
                                Instances For

                                  The restriction of an infinite place along an embedding.

                                  Equations
                                  • w.comap f = (↑w).comp ,
                                  Instances For
                                    @[simp]
                                    theorem NumberField.InfinitePlace.comap_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] (φ : K →+* ) (f : k →+* K) :
                                    theorem NumberField.InfinitePlace.comap_comp {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] (w : NumberField.InfinitePlace K) (f : F →+* K) (g : k →+* F) :
                                    w.comap (f.comp g) = (w.comap f).comap g
                                    theorem NumberField.InfinitePlace.IsReal.comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) {w : NumberField.InfinitePlace K} (hφ : w.IsReal) :
                                    (w.comap f).IsReal
                                    theorem NumberField.InfinitePlace.isReal_comap_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k ≃+* K) {w : NumberField.InfinitePlace K} :
                                    (w.comap f).IsReal w.IsReal
                                    theorem NumberField.InfinitePlace.mult_comap_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) (w : NumberField.InfinitePlace K) :
                                    (w.comap f).mult w.mult
                                    @[simp]
                                    theorem NumberField.InfinitePlace.instMulActionAlgEquiv_smul_coe_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) :
                                    ∀ (a : K), (SMul.smul σ w) a = w (σ.symm a)

                                    The action of the galois group on infinite places.

                                    Equations
                                    • NumberField.InfinitePlace.instMulActionAlgEquiv = MulAction.mk
                                    theorem NumberField.InfinitePlace.smul_eq_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) :
                                    σ w = w.comap σ.symm
                                    @[simp]
                                    theorem NumberField.InfinitePlace.smul_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) (x : K) :
                                    (σ w) x = w (σ.symm x)
                                    @[simp]
                                    theorem NumberField.InfinitePlace.smul_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (φ : K →+* ) :
                                    theorem NumberField.InfinitePlace.comap_smul {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] [Algebra k K] (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) {f : F →+* K} :
                                    (σ w).comap f = w.comap ((↑σ.symm).comp f)
                                    theorem NumberField.InfinitePlace.isReal_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : NumberField.InfinitePlace K} :
                                    (σ w).IsReal w.IsReal
                                    theorem NumberField.InfinitePlace.isComplex_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : NumberField.InfinitePlace K} :
                                    (σ w).IsComplex w.IsComplex
                                    theorem NumberField.InfinitePlace.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 →+* ) (ψ : K →+* ) (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) :
                                    ∃ (σ : K ≃ₐ[k] K), φ.comp σ.symm = ψ
                                    theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : NumberField.InfinitePlace K} {w' : NumberField.InfinitePlace K} (h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) :
                                    ∃ (σ : K ≃ₐ[k] K), σ w = w'
                                    theorem NumberField.InfinitePlace.mem_orbit_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : NumberField.InfinitePlace K} {w' : NumberField.InfinitePlace K} :
                                    w' MulAction.orbit (K ≃ₐ[k] K) w w.comap (algebraMap k K) = w'.comap (algebraMap k K)

                                    The orbits of infinite places under the action of the galois group are indexed by the infinite places of the base field.

                                    Equations
                                    Instances For
                                      theorem NumberField.InfinitePlace.orbitRelEquiv_apply_mk'' {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (w : NumberField.InfinitePlace K) :
                                      NumberField.InfinitePlace.orbitRelEquiv (Quotient.mk'' w) = w.comap (algebraMap k K)

                                      An infinite place is unramified in a field extension if the restriction has the same multiplicity.

                                      Equations
                                      Instances For
                                        theorem NumberField.InfinitePlace.IsUnramified.eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : NumberField.InfinitePlace K} (h : NumberField.InfinitePlace.IsUnramified k w) :
                                        (w.comap (algebraMap k K)).mult = w.mult

                                        A infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.

                                        Equations
                                        Instances For
                                          class IsUnramifiedAtInfinitePlaces (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] :

                                          A field extension is unramified at infinite places if every infinite place is unramified.

                                          Instances