Documentation

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Canonical embedding of a number field #

The canonical embedding of a number field K of degree n is the ring homomorphism K →+* ℂ^n that sends x ∈ K to (φ_₁(x),...,φ_n(x)) where the φ_i's are the complex embeddings of K. Note that we do not choose an ordering of the embeddings, but instead map K into the type (K →+* ℂ) → ℂ of -vectors indexed by the complex embeddings.

Main definitions and results #

Tags #

number field, infinite places

The canonical embedding of a number field K of degree n into ℂ^n.

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

    The image of canonicalEmbedding lives in the -submodule of the x ∈ ((K →+* ℂ) → ℂ) such that conj x_φ = x_(conj φ) for all ∀ φ : K →+* ℂ.

    theorem NumberField.canonicalEmbedding.nnnorm_eq {K : Type u_1} [Field K] [NumberField K] (x : K) :
    (NumberField.canonicalEmbedding K) x‖₊ = Finset.univ.sup fun (φ : K →+* ) => φ x‖₊

    A -basis of ℂ^n that is also a -basis of the integerLattice.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def NumberField.mixedEmbedding (K : Type u_1) [Field K] :
      K →+* ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })

      The mixed embedding of a number field K of signature (r₁, r₂) into ℝ^r₁ × ℂ^r₂.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def NumberField.mixedEmbedding.commMap (K : Type u_1) [Field K] :
        ((K →+* )) →ₗ[] ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })

        The linear map that makes canonicalEmbedding and mixedEmbedding commute, see commMap_canonical_eq_mixed.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem NumberField.mixedEmbedding.commMap_apply_of_isReal (K : Type u_1) [Field K] (x : (K →+* )) {w : NumberField.InfinitePlace K} (hw : w.IsReal) :
          ((NumberField.mixedEmbedding.commMap K) x).1 w, hw = (x w.embedding).re
          theorem NumberField.mixedEmbedding.commMap_apply_of_isComplex (K : Type u_1) [Field K] (x : (K →+* )) {w : NumberField.InfinitePlace K} (hw : w.IsComplex) :
          ((NumberField.mixedEmbedding.commMap K) x).2 w, hw = x w.embedding

          This is a technical result to ensure that the image of the -basis of ℂ^n defined in canonicalEmbedding.latticeBasis is a -basis of ℝ^r₁ × ℂ^r₂, see mixedEmbedding.latticeBasis.

          def NumberField.mixedEmbedding.normAtPlace {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) :
          ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex }) →*₀

          The norm at the infinite place w of an element of ({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem NumberField.mixedEmbedding.normAtPlace_real {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (c : ) :
            (NumberField.mixedEmbedding.normAtPlace w) (fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => c, fun (x : { w : NumberField.InfinitePlace K // w.IsComplex }) => c) = |c|
            theorem NumberField.mixedEmbedding.normAtPlace_apply_isReal {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
            theorem NumberField.mixedEmbedding.normAtPlace_apply_isComplex {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
            theorem NumberField.mixedEmbedding.normAtPlace_eq_zero {K : Type u_1} [Field K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })} :
            theorem NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
            x‖₊ = Finset.univ.sup fun (w : NumberField.InfinitePlace K) => (NumberField.mixedEmbedding.normAtPlace w) x,
            theorem NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
            def NumberField.mixedEmbedding.norm {K : Type u_1} [Field K] [NumberField K] :
            ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex }) →*₀

            The norm of x is ∏ w, (normAtPlace x) ^ mult w. It is defined such that the norm of mixedEmbedding K a for a : K is equal to the absolute value of the norm of a over , see norm_eq_norm.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem NumberField.mixedEmbedding.norm_apply {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
              NumberField.mixedEmbedding.norm x = w : NumberField.InfinitePlace K, (NumberField.mixedEmbedding.normAtPlace w) x ^ w.mult
              theorem NumberField.mixedEmbedding.norm_nonneg {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
              0 NumberField.mixedEmbedding.norm x
              theorem NumberField.mixedEmbedding.norm_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })} :
              NumberField.mixedEmbedding.norm x = 0 ∃ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x = 0
              theorem NumberField.mixedEmbedding.norm_ne_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })} :
              NumberField.mixedEmbedding.norm x 0 ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x 0
              theorem NumberField.mixedEmbedding.norm_smul {K : Type u_1} [Field K] [NumberField K] (c : ) (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) :
              NumberField.mixedEmbedding.norm (c x) = |c| ^ FiniteDimensional.finrank K * NumberField.mixedEmbedding.norm x
              theorem NumberField.mixedEmbedding.norm_real {K : Type u_1} [Field K] [NumberField K] (c : ) :
              NumberField.mixedEmbedding.norm (fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => c, fun (x : { w : NumberField.InfinitePlace K // w.IsComplex }) => c) = |c| ^ FiniteDimensional.finrank K
              @[simp]
              theorem NumberField.mixedEmbedding.norm_eq_norm {K : Type u_1} [Field K] [NumberField K] (x : K) :
              NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding K) x) = |(Algebra.norm ) x|
              theorem NumberField.mixedEmbedding.norm_eq_zero_iff' {K : Type u_1} [Field K] [NumberField K] {x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })} (hx : x Set.range (NumberField.mixedEmbedding K)) :
              NumberField.mixedEmbedding.norm x = 0 x = 0
              @[reducible, inline]

              The type indexing the basis stdBasis.

              Equations
              Instances For

                The -basis of ({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ) formed by the vector equal to 1 at w and 0 elsewhere for IsReal w and by the couple of vectors equal to 1 (resp. I) at w and 0 elsewhere for IsComplex w.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem NumberField.mixedEmbedding.stdBasis_apply_ofIsReal {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :
                  @[simp]
                  theorem NumberField.mixedEmbedding.stdBasis_apply_ofIsComplex_fst {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) :
                  ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 0)) = (x.2 w).re
                  @[simp]
                  theorem NumberField.mixedEmbedding.stdBasis_apply_ofIsComplex_snd {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal }) × ({ w : NumberField.InfinitePlace K // w.IsComplex })) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) :
                  ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 1)) = (x.2 w).im
                  theorem NumberField.mixedEmbedding.fundamentalDomain_stdBasis (K : Type u_1) [Field K] [NumberField K] :
                  Zspan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K) = (Set.univ.pi fun (x : { w : NumberField.InfinitePlace K // w.IsReal }) => Set.Ico 0 1) ×ˢ Set.univ.pi fun (x : { w : NumberField.InfinitePlace K // w.IsComplex }) => Complex.measurableEquivPi ⁻¹' Set.univ.pi fun (x : Fin 2) => Set.Ico 0 1

                  The Equiv between index K and K →+* ℂ defined by sending a real infinite place w to the unique corresponding embedding w.embedding, and the pair ⟨w, 0⟩ (resp. ⟨w, 1⟩) for a complex infinite place w to w.embedding (resp. conjugate w.embedding).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The matrix that gives the representation on stdBasis of the image by commMap of an element x of (K →+* ℂ) → ℂ fixed by the map x_φ ↦ conj x_(conjugate φ), see stdBasis_repr_eq_matrixToStdBasis_mul.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Let x : (K →+* ℂ) → ℂ such that x_φ = conj x_(conj φ) for all φ : K →+* ℂ, then the representation of commMap K x on stdBasis is given (up to reindexing) by the product of matrixToStdBasis by x.

                      A -basis of ℝ^r₁ × ℂ^r₂ that is also a -basis of the image of 𝓞 K.

                      Equations
                      Instances For

                        The generalized index of the lattice generated by I in the lattice generated by 𝓞 K is equal to the norm of the ideal I. The result is stated in terms of base change determinant and is the translation of NumberField.det_basisOfFractionalIdeal_eq_absNorm in ℝ^r₁ × ℂ^r₂. This is useful, in particular, to prove that the family obtained from the -basis of I is actually an -basis of ℝ^r₁ × ℂ^r₂, see fractionalIdealLatticeBasis.

                        A -basis of ℝ^r₁ × ℂ^r₂ that is also a -basis of the image of the fractional ideal I.

                        Equations
                        Instances For