NYLL
Module

PositiveArchimedeanSection.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PositiveArchimedeanSection
19 declarations indexed from sourceView source ↗

Module documentation

Positive archimedean section of the idele norm

This module constructs an idele supported at one infinite place whose absolute norm is a prescribed inverse. Its finite components are trivial and all of its infinite components lie in the standard positive subgroups.

Imports4
Imported by3

Declarations

def

positiveArchimedeanLocalComponent

L36 ↗
IdeleGroup.positiveArchimedeanLocalComponent
Documentation

A positive real unit placed in an archimedean completion. At a complex place it is first regarded as a complex unit.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def positiveArchimedeanLocalComponent
    (v : InfinitePlace K) :
    ℝ≥0ˣ →* v.Completionˣ
def

positiveArchimedeanLocalComponentContinuous

L55 ↗
IdeleGroup.positiveArchimedeanLocalComponentContinuous
Documentation

The positive local archimedean component, with its natural continuity.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · full declaration
def positiveArchimedeanLocalComponentContinuous
    (v : InfinitePlace K) :
    ℝ≥0ˣ →ₜ* v.Completionˣ where
  __ := positiveArchimedeanLocalComponent v
  continuous_toFun := by
    by_cases hv : v.IsReal
    · have hcompletion :
          Continuous
            (Units.mapEquiv
              (InfinitePlace.Completion.ringEquivRealOfIsReal
                hv).symm.toMulEquiv) := by
        exact
          (RayClass.realCompletionContinuousMulEquiv v hv).symm.continuous.units_map
            (InfinitePlace.Completion.ringEquivRealOfIsReal
              hv).symm.toMonoidHom
      apply
        (hcompletion.comp
          (NNReal.continuous_coe.units_map
            NNReal.toRealHom.toMonoidHom)).congr
      intro r
      simp only [positiveArchimedeanLocalComponent,
        dite_eq_left hv]
      congr 2
    · have hvc : v.IsComplex :=
        InfinitePlace.not_isReal_iff_isComplex.mp hv
      have hcompletion :
          Continuous
            (Units.mapEquiv
              (InfinitePlace.Completion.ringEquivComplexOfIsComplex
                hvc).symm.toMulEquiv) := by
        exact
          (RayClass.complexCompletionContinuousMulEquiv v hvc).symm.continuous.units_map
            (InfinitePlace.Completion.ringEquivComplexOfIsComplex
              hvc).symm.toMonoidHom
      apply
        (hcompletion.comp
          ((Complex.continuous_ofReal.units_map
              Complex.ofRealHom.toMonoidHom).comp
            (NNReal.continuous_coe.units_map
              NNReal.toRealHom.toMonoidHom))).congr
      intro r
      simp only [positiveArchimedeanLocalComponent,
        dite_eq_right hv]
      congr 2
theorem

positiveArchimedeanLocalComponentContinuous_apply

L102 ↗
IdeleGroup.positiveArchimedeanLocalComponentContinuous_apply
Source context 8 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem positiveArchimedeanLocalComponentContinuous_apply
    (v : InfinitePlace K) (r : ℝ≥0ˣ) :
    positiveArchimedeanLocalComponentContinuous v r =
      positiveArchimedeanLocalComponent v r
theorem

positiveArchimedeanLocalComponent_nnnorm

L109 ↗
IdeleGroup.positiveArchimedeanLocalComponent_nnnorm
Source context 8 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem positiveArchimedeanLocalComponent_nnnorm
    (v : InfinitePlace K) (r : ℝ≥0ˣ) :
    ‖((positiveArchimedeanLocalComponent v r :
        v.Completionˣ) : v.Completion)‖₊ =
      (r : ℝ≥0)
theorem

positiveArchimedeanLocalComponent_mem_positive

L196 ↗
IdeleGroup.positiveArchimedeanLocalComponent_mem_positive
Source context 8 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem positiveArchimedeanLocalComponent_mem_positive
    (v : InfinitePlace K) (r : ℝ≥0ˣ) :
    positiveArchimedeanLocalComponent v r ∈
      RayClass.infinitePositiveSubgroup v
def

positiveArchimedeanRoot

L234 ↗
IdeleGroup.positiveArchimedeanRoot
Documentation

The positive root needed to compensate for the multiplicity of the chosen infinite place.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def positiveArchimedeanRoot :
    ℝ≥0ˣ →* ℝ≥0ˣ
def

positiveArchimedeanRootContinuous

L241 ↗
IdeleGroup.positiveArchimedeanRootContinuous
Documentation

The positive root map used in the archimedean section is continuous.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · full declaration
def positiveArchimedeanRootContinuous :
    ℝ≥0ˣ →ₜ* ℝ≥0ˣ where
  __ := positiveArchimedeanRoot (K := K)
  continuous_toFun :=
    (NNReal.continuous_rpow_const
      (inv_nonneg.mpr (Nat.cast_nonneg _))).units_map
        (NNReal.rpowMonoidHom
          (((w₀ (K := K)).mult : ℝ)⁻¹))
def

positiveArchimedeanSection

L253 ↗
IdeleGroup.positiveArchimedeanSection
Documentation

The positive archimedean idele over a number field. Its finite part is one, and its sole nontrivial infinite component has been normalized so that the total archimedean norm is the input.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def positiveArchimedeanSection
    (K : Type u) [Field K] [NumberField K] :
    ℝ≥0ˣ →* IdeleGroup K
def

positiveArchimedeanSectionContinuous

L263 ↗
IdeleGroup.positiveArchimedeanSectionContinuous
Documentation

The positive archimedean section as a continuous homomorphism.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def positiveArchimedeanSectionContinuous
    (K : Type u) [Field K] [NumberField K] :
    ℝ≥0ˣ →ₜ* IdeleGroup K
theorem

positiveArchimedeanSectionContinuous_apply

L273 ↗
IdeleGroup.positiveArchimedeanSectionContinuous_apply
Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanSectionContinuous_apply
    (r : ℝ≥0ˣ) :
    positiveArchimedeanSectionContinuous K r =
      positiveArchimedeanSection K r
theorem

continuous_positiveArchimedeanSection

L280 ↗
IdeleGroup.continuous_positiveArchimedeanSection
Documentation

The positive archimedean section is continuous.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem continuous_positiveArchimedeanSection :
    Continuous (positiveArchimedeanSection K)
theorem

positiveArchimedeanSection_infiniteComponent_same

L285 ↗
IdeleGroup.positiveArchimedeanSection_infiniteComponent_same
Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanSection_infiniteComponent_same
    (r : ℝ≥0ˣ) :
    IdeleGroup.infiniteComponent (w₀ (K := K))
        (positiveArchimedeanSection K r) =
      positiveArchimedeanLocalComponent
        (w₀ (K := K))
        (positiveArchimedeanRoot (K := K) r)
theorem

positiveArchimedeanSection_infiniteComponent_of_ne

L302 ↗
IdeleGroup.positiveArchimedeanSection_infiniteComponent_of_ne
Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanSection_infiniteComponent_of_ne
    (r : ℝ≥0ˣ) (v : InfinitePlace K)
    (hv : v ≠ w₀ (K := K)) :
    IdeleGroup.infiniteComponent v
        (positiveArchimedeanSection K r) =
      1
theorem

positiveArchimedeanSection_finiteComponent

L321 ↗
IdeleGroup.positiveArchimedeanSection_finiteComponent
Documentation

Every finite component of the positive archimedean idele is one.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanSection_finiteComponent
    (r : ℝ≥0ˣ)
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup.finiteComponent v
        (positiveArchimedeanSection K r) =
      1
theorem

positiveArchimedeanSection_infiniteComponent_mem_positive

L338 ↗
IdeleGroup.positiveArchimedeanSection_infiniteComponent_mem_positive
Documentation

Every infinite component of the positive archimedean idele lies in the standard positive subgroup.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanSection_infiniteComponent_mem_positive
    (r : ℝ≥0ˣ) (v : InfinitePlace K) :
    IdeleGroup.infiniteComponent v
        (positiveArchimedeanSection K r) ∈
      RayClass.infinitePositiveSubgroup v
theorem

positiveArchimedeanSection_absoluteNorm

L356 ↗
IdeleGroup.positiveArchimedeanSection_absoluteNorm
Documentation

The positive archimedean idele has absolute idele norm r⁻¹.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanSection_absoluteNorm
    (r : ℝ≥0ˣ) :
    IdeleGroup.absoluteNorm
        (positiveArchimedeanSection K r) =
      r⁻¹
def

positiveArchimedeanNormOneCorrection

L418 ↗
IdeleGroup.positiveArchimedeanNormOneCorrection
Documentation

Multiplying an idele by its positive archimedean correction produces an idele of absolute norm one.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def positiveArchimedeanNormOneCorrection
    (K : Type u) [Field K] [NumberField K]
    (a : IdeleGroup K) :
    IdeleGroup.normOneSubgroup (K := K)
theorem

positiveArchimedeanNormOneCorrection_coe

L433 ↗
IdeleGroup.positiveArchimedeanNormOneCorrection_coe
Documentation

The underlying idele of the norm-one correction is its defining product.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem positiveArchimedeanNormOneCorrection_coe
    (a : IdeleGroup K) :
    (positiveArchimedeanNormOneCorrection K a : IdeleGroup K) =
      a * positiveArchimedeanSection K (IdeleGroup.absoluteNorm a)
theorem

eq_positiveArchimedeanNormOneCorrection_mul_section_inv

L441 ↗
IdeleGroup.eq_positiveArchimedeanNormOneCorrection_mul_section_inv
Documentation

Every idele is its norm-one correction multiplied by the inverse of the positive archimedean section.

Source context 7 commands

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

open scoped IsMulCommutative NNReal NumberField Topology
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
universe u
namespace IdeleGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem eq_positiveArchimedeanNormOneCorrection_mul_section_inv
    (a : IdeleGroup K) :
    a =
      (positiveArchimedeanNormOneCorrection K a : IdeleGroup K) *
        (positiveArchimedeanSection K
          (IdeleGroup.absoluteNorm a))⁻¹

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