NYLL
Module

ArchimedeanNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.ArchimedeanNorm
5 declarations indexed from sourceView source ↗

Module documentation

Archimedean behavior of idele norms

The positive archimedean norm, and consequently the absolute idele norm, is preserved by the ordinary norm in a finite number-field extension.

Imports1
Imported by3

Declarations

theorem

nnnormUnitHom_map_ringEquiv_of_isometry

L33 ↗
IdeleGroup.nnnormUnitHom_map_ringEquiv_of_isometry
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
Lean source · statement
theorem nnnormUnitHom_map_ringEquiv_of_isometry
    {F E : Type*}
    [NormedField F] [NormedField E]
    (e : F ≃+* E) (he : Isometry e) (x : Fˣ) :
    nnnormUnitHom E
        (Units.mapEquiv e.toMulEquiv x) =
      nnnormUnitHom F x
theorem

nnnormUnitHom_real_normUnits_complex

L46 ↗
IdeleGroup.nnnormUnitHom_real_normUnits_complex
Documentation

The ordinary norm from ℂ to ℝ squares the positive norm.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
Lean source · statement
theorem nnnormUnitHom_real_normUnits_complex
    (x : ℂˣ) :
    nnnormUnitHom ℝ
        (LocalFieldTheory.normUnits ℝ ℂ x) =
      nnnormUnitHom ℂ x ^ 2
theorem

nnnormUnitHom_normUnits_infinitePlace

L63 ↗
IdeleGroup.nnnormUnitHom_normUnits_infinitePlace
Documentation

At an infinite place, the positive norm of a local field norm, with the base multiplicity, is the positive norm upstairs with the upstairs multiplicity.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · full declaration
theorem nnnormUnitHom_normUnits_infinitePlace
    (v₀ : InfinitePlace K)
    (W : InfinitePlace L)
    (hW : W ∈ v₀.placesOver L)
    (x : W.Completionˣ) :
    letI : W.1.LiesOver v₀.1 := hW
    nnnormUnitHom v₀.Completion
        (LocalFieldTheory.normUnits
          v₀.Completion W.Completion x) ^ v₀.mult =
      nnnormUnitHom W.Completion x ^ W.mult := by
  let : W.1.LiesOver v₀.1 := hW
  rcases v₀.isReal_or_isComplex with hvReal | hvComplex
  · rcases W.isReal_or_isComplex with hWReal | hWComplex
    · let eBase :=
        InfinitePlace.Completion.ringEquivRealOfIsReal hvReal
      let eExtension :=
        InfinitePlace.Completion.ringEquivRealOfIsReal hWReal
      let :
          NumberField.ComplexEmbedding.LiesOver
            (InfinitePlace.Completion.extensionEmbedding W)
            (InfinitePlace.Completion.extensionEmbedding v₀) :=
        InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal
          W hvReal
      have hCompatible :
          RingHom.comp (algebraMap ℝ ℝ) eBase.toRingHom =
            RingHom.comp eExtension.toRingHom
              (algebraMap v₀.Completion W.Completion) := by
        ext z
        change
          InfinitePlace.Completion.extensionEmbeddingOfIsReal
              hvReal z =
            InfinitePlace.Completion.extensionEmbeddingOfIsReal
              hWReal ((algebraMap v₀.Completion W.Completion) z)
        apply Complex.ofReal_injective
        simpa only [
          InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply] using
          (InfinitePlace.Completion.liesOver_extensionEmbedding_apply
            W (v := v₀)).symm
      have hNorm :=
        LocalClassFieldTheory.normUnits_map_ringEquiv
          eBase eExtension
          hCompatible x
      rw [InfinitePlace.mult_isReal ⟨v₀, hvReal⟩,
        InfinitePlace.mult_isReal ⟨W, hWReal⟩,
        pow_one, pow_one]
      calc
        nnnormUnitHom v₀.Completion
            (LocalFieldTheory.normUnits
              v₀.Completion W.Completion x) =
            nnnormUnitHom ℝ
              (Units.mapEquiv eBase.toMulEquiv
                (LocalFieldTheory.normUnits
                  v₀.Completion W.Completion x)) := by
          symm
          exact
            nnnormUnitHom_map_ringEquiv_of_isometry
              eBase
              (InfinitePlace.Completion.isometryEquivRealOfIsReal
                hvReal).isometry _
        _ =
            nnnormUnitHom ℝ
              (LocalFieldTheory.normUnits ℝ ℝ
                (Units.mapEquiv eExtension.toMulEquiv x)) := by
          rw [hNorm]
        _ =
            nnnormUnitHom ℝ
              (Units.mapEquiv eExtension.toMulEquiv x) := by
          simp [LocalFieldTheory.normUnits]
        _ = nnnormUnitHom W.Completion x :=
          nnnormUnitHom_map_ringEquiv_of_isometry
            eExtension
            (InfinitePlace.Completion.isometryEquivRealOfIsReal
              hWReal).isometry x
    · let eBase :=
        InfinitePlace.Completion.ringEquivRealOfIsReal hvReal
      let eExtension :=
        InfinitePlace.Completion.ringEquivComplexOfIsComplex hWComplex
      let :
          NumberField.ComplexEmbedding.LiesOver
            (InfinitePlace.Completion.extensionEmbedding W)
            (InfinitePlace.Completion.extensionEmbedding v₀) :=
        InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal
          W hvReal
      have hCompatible :
          RingHom.comp (algebraMap ℝ ℂ) eBase.toRingHom =
            RingHom.comp eExtension.toRingHom
              (algebraMap v₀.Completion W.Completion) := by
        ext z
        simp [eBase, eExtension]
      have hNorm :=
        LocalClassFieldTheory.normUnits_map_ringEquiv
          eBase eExtension
          hCompatible x
      rw [InfinitePlace.mult_isReal ⟨v₀, hvReal⟩,
        InfinitePlace.mult_isComplex ⟨W, hWComplex⟩,
        pow_one]
      calc
        nnnormUnitHom v₀.Completion
            (LocalFieldTheory.normUnits
              v₀.Completion W.Completion x) =
            nnnormUnitHom ℝ
              (Units.mapEquiv eBase.toMulEquiv
                (LocalFieldTheory.normUnits
                  v₀.Completion W.Completion x)) := by
          symm
          exact
            nnnormUnitHom_map_ringEquiv_of_isometry
              eBase
              (InfinitePlace.Completion.isometryEquivRealOfIsReal
                hvReal).isometry _
        _ =
            nnnormUnitHom ℝ
              (LocalFieldTheory.normUnits ℝ ℂ
                (Units.mapEquiv eExtension.toMulEquiv x)) := by
          rw [hNorm]
        _ =
            nnnormUnitHom ℂ
                (Units.mapEquiv eExtension.toMulEquiv x) ^ 2 :=
          nnnormUnitHom_real_normUnits_complex
            (Units.mapEquiv eExtension.toMulEquiv x)
        _ = nnnormUnitHom W.Completion x ^ 2 := by
          rw [nnnormUnitHom_map_ringEquiv_of_isometry
            eExtension
            (InfinitePlace.Completion.isometryEquivComplexOfIsComplex
              hWComplex).isometry]
  · have hWComplex :
        W.IsComplex :=
      InfinitePlace.LiesOver.isComplex_of_isComplex_under
        W hvComplex
    let eBase :=
      InfinitePlace.Completion.ringEquivComplexOfIsComplex hvComplex
    have hCore
        (eExtension : W.Completion ≃+* ℂ)
        (hCompatible :
          RingHom.comp (algebraMap ℂ ℂ) eBase.toRingHom =
            RingHom.comp eExtension.toRingHom
              (algebraMap v₀.Completion W.Completion))
        (hExtensionIsometry : Isometry eExtension) :
        nnnormUnitHom v₀.Completion
            (LocalFieldTheory.normUnits
              v₀.Completion W.Completion x) =
          nnnormUnitHom W.Completion x := by
      have hNorm :=
        LocalClassFieldTheory.normUnits_map_ringEquiv
          eBase eExtension
          hCompatible x
      calc
        nnnormUnitHom v₀.Completion
            (LocalFieldTheory.normUnits
              v₀.Completion W.Completion x) =
            nnnormUnitHom ℂ
              (Units.mapEquiv eBase.toMulEquiv
                (LocalFieldTheory.normUnits
                  v₀.Completion W.Completion x)) := by
          symm
          exact
            nnnormUnitHom_map_ringEquiv_of_isometry
              eBase
              (InfinitePlace.Completion.isometryEquivComplexOfIsComplex
                hvComplex).isometry _
        _ =
            nnnormUnitHom ℂ
              (LocalFieldTheory.normUnits ℂ ℂ
                (Units.mapEquiv eExtension.toMulEquiv x)) := by
          rw [hNorm]
        _ =
            nnnormUnitHom ℂ
              (Units.mapEquiv eExtension.toMulEquiv x) := by
          simp [LocalFieldTheory.normUnits]
        _ = nnnormUnitHom W.Completion x :=
          nnnormUnitHom_map_ringEquiv_of_isometry
            eExtension hExtensionIsometry x
    rw [InfinitePlace.mult_isComplex ⟨v₀, hvComplex⟩,
      InfinitePlace.mult_isComplex ⟨W, hWComplex⟩]
    congr 1
    rcases
        InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq
          W v₀ with hEmbedding | hConjugate
    · let eExtension :=
        InfinitePlace.Completion.ringEquivComplexOfIsComplex hWComplex
      let :
          NumberField.ComplexEmbedding.LiesOver W.embedding v₀.embedding :=
        ⟨hEmbedding⟩
      let :
          NumberField.ComplexEmbedding.LiesOver
            (InfinitePlace.Completion.extensionEmbedding W)
            (InfinitePlace.Completion.extensionEmbedding v₀) :=
        InfinitePlace.Completion.liesOver_extensionEmbedding W v₀
      have hCompatible :
          RingHom.comp (algebraMap ℂ ℂ) eBase.toRingHom =
            RingHom.comp eExtension.toRingHom
              (algebraMap v₀.Completion W.Completion) := by
        ext z
        change
          InfinitePlace.Completion.extensionEmbedding v₀ z =
            InfinitePlace.Completion.extensionEmbedding W
              ((algebraMap v₀.Completion W.Completion) z)
        exact
          (InfinitePlace.Completion.liesOver_extensionEmbedding_apply
            W (v := v₀)).symm
      exact
        hCore eExtension hCompatible
          (InfinitePlace.Completion.isometryEquivComplexOfIsComplex
            hWComplex).isometry
    · let eExtension :=
        (InfinitePlace.Completion.ringEquivComplexOfIsComplex hWComplex).trans
          (starRingAut (R := ℂ))
      let :
          NumberField.ComplexEmbedding.LiesOver
            (ComplexEmbedding.conjugate W.embedding) v₀.embedding :=
        ⟨hConjugate⟩
      let :
          NumberField.ComplexEmbedding.LiesOver
            (ComplexEmbedding.conjugate
              (InfinitePlace.Completion.extensionEmbedding W))
            (InfinitePlace.Completion.extensionEmbedding v₀) :=
        InfinitePlace.Completion.liesOver_conjugate_extensionEmbedding W v₀
      have hCompatible :
          RingHom.comp (algebraMap ℂ ℂ) eBase.toRingHom =
            RingHom.comp eExtension.toRingHom
              (algebraMap v₀.Completion W.Completion) := by
        ext z
        simp [eBase, eExtension, ← ComplexEmbedding.conjugate_coe_eq]
      have hExtensionIsometry : Isometry eExtension := by
        intro y z
        change
          edist (star (InfinitePlace.Completion.extensionEmbedding W y))
              (star (InfinitePlace.Completion.extensionEmbedding W z)) =
            edist y z
        calc
          edist (star (InfinitePlace.Completion.extensionEmbedding W y))
              (star (InfinitePlace.Completion.extensionEmbedding W z)) =
              edist (InfinitePlace.Completion.extensionEmbedding W y)
                (InfinitePlace.Completion.extensionEmbedding W z) :=
            star_isometry.edist_eq _ _
          _ = edist y z :=
            (InfinitePlace.Completion.isometry_extensionEmbedding W).edist_eq _ _
      exact hCore eExtension hCompatible hExtensionIsometry
theorem

archimedeanNorm_norm

L303 ↗
IdeleGroup.archimedeanNorm_norm
Documentation

The archimedean positive norm is preserved by the ordinary idele norm.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
Lean source · statement
theorem archimedeanNorm_norm
    (a : IdeleGroup L) :
    InfiniteIdeleGroup.archimedeanNorm
        (norm K L a).1 =
      InfiniteIdeleGroup.archimedeanNorm a.1
theorem

absoluteNorm_norm

L395 ↗
IdeleGroup.absoluteNorm_norm
Documentation

The absolute idele norm is preserved by the ordinary idele norm.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
universe u v
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
Lean source · statement
theorem absoluteNorm_norm
    (a : IdeleGroup L) :
    absoluteNorm (norm K L a) =
      absoluteNorm a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.