NYLL
Module

InfinitePlaces.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormApproximation.InfinitePlaces
7 declarations indexed from sourceView source ↗

Module documentation

Archimedean norm approximation

This file supplies the archimedean source used in the norm-approximation argument. At a real place the positive units have an n-th root, while at a complex place every unit has one. Consequently the standard positive subgroup is contained in the determinant-norm image of every scalar extension of positive degree.

Imports8
Imported by9

Declarations

theorem

exists_infinitePositiveSubgroup_nthRoot

L46 ↗
Documentation

Every element of the archimedean positive subgroup has an n-th root for n > 0. At complex places the positivity condition is vacuous and algebraic closedness supplies the root.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
section ArchimedeanNorm
variable {K : Type u} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem exists_infinitePositiveSubgroup_nthRoot
    (v : InfinitePlace K)
    (n : ℕ) (hn : 0 < n)
    (x : v.Completionˣ)
    (hx : x ∈ RayClass.infinitePositiveSubgroup v) :
    ∃ y : v.Completionˣ, y ^ n = x
def

infiniteTensorDetNorm

L100 ↗
Documentation

Determinant norm on the actual tensor factor used by the infinite component of the relative adele ring.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
section ArchimedeanNorm
variable {K : Type u} [Field K] [NumberField K]
variable {L : Type v} [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def infiniteTensorDetNorm
    (v : InfinitePlace K) :
    (v.Completion ⊗[K] L)ˣ →* v.Completionˣ
def

infiniteTensorNormSubgroup

L106 ↗
Documentation

Image of the determinant norm on an infinite tensor factor.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
section ArchimedeanNorm
variable {K : Type u} [Field K] [NumberField K]
variable {L : Type v} [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def infiniteTensorNormSubgroup
    (v : InfinitePlace K) :
    Subgroup v.Completionˣ
theorem

infinitePositiveSubgroup_le_infiniteTensorNormSubgroup

L113 ↗
Documentation

The positive subgroup at an infinite place lies in the determinant norm image of the corresponding local tensor algebra.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
section ArchimedeanNorm
variable {K : Type u} [Field K] [NumberField K]
variable {L : Type v} [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem infinitePositiveSubgroup_le_infiniteTensorNormSubgroup
    (v : InfinitePlace K) :
    RayClass.infinitePositiveSubgroup v ≤
      infiniteTensorNormSubgroup (K := K) (L := L) v
theorem

chosenFinitePlaceLocalNormSubgroup_eq_top_of_splitsCompletely

L148 ↗
Documentation

Complete splitting at a finite place makes the chosen local norm subgroup the whole multiplicative group.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
variable {K : Type} [Field K] [NumberField K]
variable {L : Type} [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem chosenFinitePlaceLocalNormSubgroup_eq_top_of_splitsCompletely
    [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v = ⊤
theorem

exists_principal_quotient_mem_localNormSubgroups

L200 ↗
Documentation

Simultaneous weak approximation into the concrete finite local norm subgroups and into the archimedean tensor-norm images.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
variable {K : Type} [Field K] [NumberField K]
variable {L : Type} [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem exists_principal_quotient_mem_localNormSubgroups
    [IsGalois K L]
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : IdeleGroup K) :
    ∃ x : Kˣ,
      (∀ v : ↥S,
        IdeleGroup.finiteComponent v.1 a *
            (IdeleGroup.finiteComponent v.1
              (IdeleGroup.principalIdele K x))⁻¹ ∈
          chosenFinitePlaceLocalNormSubgroup
            (K := K) (L := L) v.1) ∧
      (∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a *
            (IdeleGroup.infiniteComponent w
              (IdeleGroup.principalIdele K x))⁻¹ ∈
          infiniteTensorNormSubgroup
            (K := K) (L := L) w)
theorem

exists_principal_quotient_locallyNormEverywhere_of_splitsOutside

L237 ↗
Documentation

If all finite places outside a finite set split completely, one principal correction makes a given idele a determinant norm locally at every finite and infinite place.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
open LocalClassFieldTheory
universe u v
variable {K : Type} [Field K] [NumberField K]
variable {L : Type} [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem exists_principal_quotient_locallyNormEverywhere_of_splitsOutside
    [IsGalois K L]
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (hsplit :
      ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
        FinitePlaceSplitsCompletely
          (K := K) (L := L) v)
    (a : IdeleGroup K) :
    ∃ x : Kˣ,
      (∀ v : HeightOneSpectrum (𝓞 K),
        IdeleGroup.finiteComponent v a *
            (IdeleGroup.finiteComponent v
              (IdeleGroup.principalIdele K x))⁻¹ ∈
          chosenFinitePlaceLocalNormSubgroup
            (K := K) (L := L) v) ∧
      (∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a *
            (IdeleGroup.infiniteComponent w
              (IdeleGroup.principalIdele K x))⁻¹ ∈
          infiniteTensorNormSubgroup
            (K := K) (L := L) w)

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