Module

ExtensionBehavior.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.ExtensionBehavior

9 declarations indexed from sourceView source ↗

Module documentation

Scalar-extension behavior of idele norms

Scalar extension raises the finite, archimedean, and absolute idele norms to the degree of the number-field extension. The rational relative-idele base-change realization is included as the endpoint used by cyclotomic reciprocity.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.FiniteNormArithmetic

Imported by2

theorem

infinitePlaceCompletionMap_isometry

L36 ↗

IdeleGroup.infinitePlaceCompletionMap_isometry

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 L] in

Lean source · statement

theorem infinitePlaceCompletionMap_isometry
    (v₀ : InfinitePlace K)
    (W : InfinitePlace L)
    [W.1.LiesOver v₀.1] :
    Isometry
      (NumberField.LiesOver.completionMap
        (v := v₀) (w := W))

theorem

nnnormUnitHom_infinitePlaceCompletionMap

L53 ↗

IdeleGroup.nnnormUnitHom_infinitePlaceCompletionMap

Documentation

Mapping a unit along an infinite-place completion map preserves its positive norm.

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 L] in

Lean source · statement

theorem nnnormUnitHom_infinitePlaceCompletionMap
    (v₀ : InfinitePlace K)
    (W : InfinitePlace L)
    [W.1.LiesOver v₀.1]
    (x : v₀.Completionˣ) :
    nnnormUnitHom W.Completion
        (Units.map
          (NumberField.LiesOver.completionMap
            (v := v₀) (w := W)) x) =
      nnnormUnitHom v₀.Completion x

def

infinitePlaceFiberEquivPlacesOver

L79 ↗

IdeleGroup.infinitePlaceFiberEquivPlacesOver

Documentation

The fiber of restriction of infinite places is the set of places lying over the chosen base place.

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 · full declaration

def infinitePlaceFiberEquivPlacesOver
    (v₀ : InfinitePlace K) :
    {W : InfinitePlace L //
      _root_.infinitePlaceBelow (K := K) W = v₀} ≃
      {W : InfinitePlace L // W ∈ v₀.placesOver L} where
  toFun W :=
    ⟨W.1, ⟨congrArg (fun v : InfinitePlace K => v.1) W.2⟩⟩
  invFun W :=
    ⟨W.1, by
      change W.1.comap (algebraMap K L) = v₀
      let : W.1.1.LiesOver v₀.1 := W.2
      exact InfinitePlace.LiesOver.comap_eq W.1 v₀⟩
  left_inv W := Subtype.ext rfl
  right_inv W := Subtype.ext rfl

theorem

infinitePlace_mult_eq_base_mult_mul_inertiaDeg

L97 ↗

IdeleGroup.infinitePlace_mult_eq_base_mult_mul_inertiaDeg

Documentation

The archimedean multiplicity upstairs is the base multiplicity times the local inertia degree.

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 · statement

theorem infinitePlace_mult_eq_base_mult_mul_inertiaDeg
    (v₀ : InfinitePlace K)
    (W : InfinitePlace L)
    (hW : W ∈ v₀.placesOver L) :
    W.mult = v₀.mult * v₀.inertiaDeg W

theorem

infinitePlaceFiber_inertiaDeg_sum

L142 ↗

IdeleGroup.infinitePlaceFiber_inertiaDeg_sum

Documentation

The inertia degrees in a restriction fiber sum to the global extension degree.

Source context 8 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]
open scoped Classical in
omit [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceFiber_inertiaDeg_sum
    (v₀ : InfinitePlace K) :
    ∑ W : {W : InfinitePlace L //
        _root_.infinitePlaceBelow (K := K) W = v₀},
      v₀.inertiaDeg W.1 =
        Module.finrank K L

theorem

infinitePlaceFiber_mult_sum

L178 ↗

IdeleGroup.infinitePlaceFiber_mult_sum

Documentation

The total archimedean multiplicity in a restriction fiber is the base multiplicity times the extension degree.

Source context 8 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]
open scoped Classical in
omit [FiniteDimensional K L] in

Lean source · statement

theorem infinitePlaceFiber_mult_sum
    (v₀ : InfinitePlace K) :
    ∑ W : {W : InfinitePlace L //
        _root_.infinitePlaceBelow (K := K) W = v₀},
      W.1.mult =
        v₀.mult * Module.finrank K L

theorem

archimedeanNorm_extension

L210 ↗

IdeleGroup.archimedeanNorm_extension

Documentation

Scalar extension raises the archimedean idele norm to the degree of the extension.

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_extension
    (a : IdeleGroup K) :
    InfiniteIdeleGroup.archimedeanNorm
        (extension K L a).1 =
      InfiniteIdeleGroup.archimedeanNorm a.1 ^
        Module.finrank K L

theorem

absoluteNorm_extension

L328 ↗

IdeleGroup.absoluteNorm_extension

Documentation

Scalar extension raises the absolute idele norm to the degree of the number-field extension.

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_extension
    (a : IdeleGroup K) :
    absoluteNorm (extension K L a) =
      absoluteNorm a ^ Module.finrank K L

theorem

absoluteNorm_relativeIdeleBaseChange_inclusion_of_finite_eq_one

L352 ↗

IdeleGroup.absoluteNorm_relativeIdeleBaseChange_inclusion_of_finite_eq_one

Documentation

If the finite part of a rational idele is trivial, then its scalar extension has absolute norm equal to the extension degree power of the original absolute 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_relativeIdeleBaseChange_inclusion_of_finite_eq_one
    (a : IdeleGroup ℚ)
    (ha : a.2 = 1) :
    absoluteNorm
        (_root_.relativeIdeleBaseChangeMulEquiv
          (K := ℚ) (L := L)
          (RelativeIdeleGroup.inclusion ℚ L a)) =
      absoluteNorm a ^ Module.finrank ℚ L

Module documentation

Scalar-extension behavior of idele norms

Declarations