NYLL
Module

Norm.lean

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

Module documentation

Absolute and relative norms of ideles

This module exposes the absolute norm on the idele group and assembles compatible local determinant-norm preimages into a global relative idele.

Imports5
Imported by8

Declarations

theorem

exists_relativeIdele_norm_eq_of_localTensorPreimages

L39 ↗
Documentation

Assemble compatible local determinant-norm preimages into an actual relative idele. The only restricted-product input is simultaneous basis-integrality of the finite preimage and its inverse at almost every finite place.

Source context 5 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem exists_relativeIdele_norm_eq_of_localTensorPreimages
    (a : IdeleGroup K)
    (zInfinite :
      ∀ w : InfinitePlace K,
        (w.Completion ⊗[K] L)ˣ)
    (zFinite :
      ∀ w : HeightOneSpectrum (𝓞 K),
        (w.adicCompletion K ⊗[K] L)ˣ)
    (hInfinite :
      ∀ w : InfinitePlace K,
        infiniteTensorDetNorm (K := K) (L := L) w
            (zInfinite w) =
          IdeleGroup.infiniteComponent w a)
    (hFinite :
      ∀ w : HeightOneSpectrum (𝓞 K),
        _root_.localTensorNorm
            (K := K) (L := L) w (zFinite w) =
          IdeleGroup.finiteComponent w a)
    (hIntegral :
      ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
        RelativeBasisIntegralUnitAt
          (K := K) (L := L) w (zFinite w)) :
    ∃ z : RelativeIdeleGroup K L,
      RelativeIdeleGroup.norm K L z = a
theorem

idele_mem_relativeNorm_range_of_localNorms_with_integralPreimages

L104 ↗
Documentation

Membership in every local norm image, together with a restricted choice of finite local preimages, implies membership in the image of the global relative-idele norm.

Source context 5 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem idele_mem_relativeNorm_range_of_localNorms_with_integralPreimages
    (a : IdeleGroup K)
    (hInfinite :
      ∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a ∈
          infiniteTensorNormSubgroup
            (K := K) (L := L) w)
    (zFinite :
      ∀ w : HeightOneSpectrum (𝓞 K),
        (w.adicCompletion K ⊗[K] L)ˣ)
    (hFinite :
      ∀ w : HeightOneSpectrum (𝓞 K),
        _root_.localTensorNorm
            (K := K) (L := L) w (zFinite w) =
          IdeleGroup.finiteComponent w a)
    (hIntegral :
      ∀ᶠ w : HeightOneSpectrum (𝓞 K) in Filter.cofinite,
        RelativeBasisIntegralUnitAt
          (K := K) (L := L) w (zFinite w)) :
    a ∈ (RelativeIdeleGroup.norm K L).range
theorem

finiteComponent_mem_localTensorNorm_range_of_mem_relativeNorm_range

L140 ↗
Documentation

Every global relative-idele norm belongs to each finite local determinant-norm image.

Source context 5 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem finiteComponent_mem_localTensorNorm_range_of_mem_relativeNorm_range
    (a : IdeleGroup K)
    (ha : a ∈ (RelativeIdeleGroup.norm K L).range)
    (w : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup.finiteComponent w a ∈
      (_root_.localTensorNorm
        (K := K) (L := L) w).range
theorem

infiniteComponent_mem_infiniteTensorNormSubgroup_of_mem_relativeNorm_range

L157 ↗
Documentation

Every global relative-idele norm belongs to each infinite local determinant-norm image.

Source context 5 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem infiniteComponent_mem_infiniteTensorNormSubgroup_of_mem_relativeNorm_range
    (a : IdeleGroup K)
    (ha : a ∈ (RelativeIdeleGroup.norm K L).range)
    (w : InfinitePlace K) :
    IdeleGroup.infiniteComponent w a ∈
      infiniteTensorNormSubgroup
        (K := K) (L := L) w
theorem

mem_relativeIdeleNorm_range_iff_localTensorNorms

L178 ↗
Documentation

Local-to-global norm criterion for ideles. An idele is an actual global relative-idele norm if and only if all of its finite and infinite components belong to the corresponding determinant-norm images. The restrictedness of the global preimage is automatic: at the cofinitely many places where the given idele is a local integer unit, the finite local preimage is chosen valuation-integral and is therefore basis-integral away from the fixed discriminant support.

Source context 4 commands

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

open scoped NumberField TensorProduct RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem mem_relativeIdeleNorm_range_iff_localTensorNorms
    (a : IdeleGroup K) :
    a ∈ (RelativeIdeleGroup.norm K L).range ↔
      (∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a ∈
          infiniteTensorNormSubgroup
            (K := K) (L := L) w) ∧
      (∀ w : HeightOneSpectrum (𝓞 K),
        IdeleGroup.finiteComponent w a ∈
          (_root_.localTensorNorm
            (K := K) (L := L) w).range)

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