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

source
๐Ÿ“ coverage
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)
source
๐Ÿ”ธ coverage
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.

Equations
    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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 โ„š.

    source
    ๐Ÿ“ coverage
    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))
    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ”ธ coverage
    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
      Instances For
        source
        ๐Ÿ“ coverage
        @[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โ€–
        source
        ๐Ÿ”ธ coverage
        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.

        Equations
          Instances For
            source
            ๐Ÿ“ coverage
            @[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) = ฯ†
            source
            ๐Ÿ“ coverage
            @[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
            source
            ๐Ÿ”ธ coverage
            @[reducible, inline]
            abbrev NumberField.ComplexEmbedding.conjugate {K : Type u_1} [Field K] (ฯ† : K โ†’+* โ„‚) :
            K โ†’+* โ„‚

            The conjugate of a complex embedding as a complex embedding.

            Equations
              Instances For
                source
                ๐Ÿ“ coverage
                @[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 ฯƒ)
                source
                ๐Ÿ“ coverage
                theorem NumberField.ComplexEmbedding.involutive_conjugate (K : Type u_1) [Field K] :
                Function.Involutive conjugate
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [Field K] (ฯ† : K โ†’+* โ„‚) (x : K) :
                (conjugate ฯ†) x = (starRingEnd โ„‚) (ฯ† x)
                source
                ๐Ÿ“ coverage
                theorem NumberField.ComplexEmbedding.place_conjugate {K : Type u_1} [Field K] (ฯ† : K โ†’+* โ„‚) :
                place (conjugate ฯ†) = place ฯ†
                source
                ๐Ÿ”น coverage
                @[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.

                Equations
                  Instances For
                    source
                    ๐Ÿ“ coverage
                    theorem NumberField.ComplexEmbedding.isReal_iff {K : Type u_1} [Field K] {ฯ† : K โ†’+* โ„‚} :
                    IsReal ฯ† โ†” conjugate ฯ† = ฯ†
                    source
                    ๐Ÿ“ coverage
                    theorem NumberField.ComplexEmbedding.isReal_conjugate_iff {K : Type u_1} [Field K] {ฯ† : K โ†’+* โ„‚} :
                    IsReal (conjugate ฯ†) โ†” IsReal ฯ†
                    source
                    ๐Ÿ”ธ coverage
                    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 โ„ .

                    Equations
                      Instances For
                        source
                        ๐Ÿ“ coverage
                        @[simp]
                        theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply {K : Type u_1} [Field K] {ฯ† : K โ†’+* โ„‚} (hฯ† : IsReal ฯ†) (x : K) :
                        โ†‘(hฯ†.embedding x) = ฯ† x
                        source
                        ๐Ÿ“ coverage
                        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)
                        source
                        ๐Ÿ“ coverage
                        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 ฯ†
                        source
                        ๐Ÿ“ coverage
                        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 = ฯˆ
                        source
                        ๐Ÿ”น coverage
                        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 โ†’+* โ„‚.

                        Equations
                          Instances For
                            source
                            ๐Ÿ“ coverage
                            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)
                            source
                            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 ฯ† ฯƒโ‚‚) :
                            ฯƒโ‚ = ฯƒโ‚‚
                            source
                            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 ฯ† ฯƒโ‚‚
                            source
                            ๐Ÿ“ coverage
                            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))
                            source
                            ๐Ÿ“ coverage
                            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 ฯ†
                            source
                            ๐Ÿ“ coverage
                            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.

                            source
                            ๐Ÿ“ coverage
                            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 ฯ†
                            source
                            ๐Ÿ“ coverage
                            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
                            source
                            ๐Ÿ“ coverage
                            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 ฯ† ฯƒ
                            source
                            ๐Ÿ“ coverage
                            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
                            source
                            ๐Ÿ“ coverage
                            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 โ†‘ฮฝ) (ฮฝโปยน * ฯƒ * ฮฝ)
                            source
                            ๐Ÿ“ coverage
                            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
                            source
                            ๐Ÿ”ธ coverage
                            @[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) = ฯˆ.

                            Equations
                              Instances For
                                source
                                ๐Ÿ“ coverage
                                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) = ฯˆ
                                source
                                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) โ‰  ฯˆ
                                source
                                ๐Ÿ“ coverage
                                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 โ†‘ฯ†
                                source
                                ๐Ÿ”น coverage
                                @[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.

                                Equations
                                  Instances For
                                    source
                                    ๐Ÿ”น coverage
                                    @[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.

                                    Equations
                                      Instances For
                                        source
                                        ๐Ÿ“ coverage
                                        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 ฯ†