Module

CyclotomicIdeleValueTopology.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicIdeleValueTopology

17 declarations indexed from sourceView source ↗

Module documentation

Topology of the rational cyclotomic idele value

The rational cyclotomic idele value is constructed multiplicatively in CyclotomicIdeleValue. For descent to the additive idele class group and for the valuation package, this file records its genuine continuous additive form. Its finite reductions give the open-kernel finite quotients which form the profinite neighbourhood system used after principal-idèle vanishing has been proved.

Imports3

Imported by2

def

rationalCyclotomicZHatIdeleValueContinuousAdd

L32 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueContinuousAdd

Documentation

The rational cyclotomic idele value in continuous additive notation.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · full declaration

def rationalCyclotomicZHatIdeleValueContinuousAdd :
    Additive (IdeleGroup ℚ) →ₜ+ ZHat where
  __ :=
    rationalCyclotomicZHatIdeleValue.toMonoidHom.toAdditiveLeft
  continuous_toFun :=
    continuous_toAdd.comp
      (rationalCyclotomicZHatIdeleValue.continuous_toFun.comp
        continuous_toMul)

theorem

rationalCyclotomicZHatIdeleValueContinuousAdd_apply

L44 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueContinuousAdd_apply

Documentation

Evaluation of the continuous additive rational cyclotomic value agrees with the original multiplicative value.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

theorem rationalCyclotomicZHatIdeleValueContinuousAdd_apply
    (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleValueContinuousAdd
        (Additive.ofMul a) =
      Multiplicative.toAdd
        (rationalCyclotomicZHatIdeleValue a)

theorem

rationalCyclotomicZHatIdeleValueContinuousAdd_denseRange

L53 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueContinuousAdd_denseRange

Documentation

The continuous additive rational cyclotomic value has dense image.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

theorem rationalCyclotomicZHatIdeleValueContinuousAdd_denseRange :
    DenseRange rationalCyclotomicZHatIdeleValueContinuousAdd

theorem

rationalCyclotomicZHatIdeleValueContinuousAdd_isClosed_ker

L86 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueContinuousAdd_isClosed_ker

Documentation

The kernel of the continuous additive rational cyclotomic value is closed. This is the Hausdorffness input for its eventual quotient descent.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

theorem rationalCyclotomicZHatIdeleValueContinuousAdd_isClosed_ker :
    IsClosed
      (((ContinuousAddMonoidHom.toAddMonoidHom
          rationalCyclotomicZHatIdeleValueContinuousAdd).ker :
        AddSubgroup (Additive (IdeleGroup ℚ))) :
        Set (Additive (IdeleGroup ℚ)))

def

rationalCyclotomicZHatIdeleValueReduction

L107 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueReduction

Documentation

Reduction of the rational cyclotomic idele value modulo a positive integer, as an actual continuous additive homomorphism.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

def rationalCyclotomicZHatIdeleValueReduction
    (n : ℕ) (hn : 0 < n) :
    Additive (IdeleGroup ℚ) →ₜ+ ZMod n

theorem

rationalCyclotomicZHatIdeleValueReduction_apply

L116 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueReduction_apply

Documentation

Evaluation of a finite reduction is reduction of the original cyclotomic value.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

theorem rationalCyclotomicZHatIdeleValueReduction_apply
    (n : ℕ) (hn : 0 < n) (a : IdeleGroup ℚ) :
    rationalCyclotomicZHatIdeleValueReduction n hn
        (Additive.ofMul a) =
      zHatReduction n hn
        (Multiplicative.toAdd
          (rationalCyclotomicZHatIdeleValue a))

theorem

rationalCyclotomicZHatIdeleValueReduction_surjective

L127 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueReduction_surjective

Documentation

Every residue class modulo a positive integer occurs as a finite reduction of the rational cyclotomic idele value.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

theorem rationalCyclotomicZHatIdeleValueReduction_surjective
    (n : ℕ) (hn : 0 < n) :
    Function.Surjective
      (rationalCyclotomicZHatIdeleValueReduction n hn)

theorem

rationalCyclotomicZHatIdeleValueReduction_isOpen_ker

L154 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicZHatIdeleValueReduction_isOpen_ker

Documentation

The finite reduction kernels are open. They are the concrete open congruence subgroups available for the later idele-class quotient map.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation

Lean source · statement

theorem rationalCyclotomicZHatIdeleValueReduction_isOpen_ker
    (n : ℕ) (hn : 0 < n) :
    IsOpen
      (((ContinuousAddMonoidHom.toAddMonoidHom
          (rationalCyclotomicZHatIdeleValueReduction n hn)).ker :
        AddSubgroup (Additive (IdeleGroup ℚ))) :
        Set (Additive (IdeleGroup ℚ)))

def

cyclotomicZHatNormCompositeContinuous

L179 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicZHatNormCompositeContinuous

Documentation

The unnormalized cyclotomic norm composite, bundled with its actual continuity. Continuity here uses the global idele norm rather than a quotient-level substitute.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · full declaration

def cyclotomicZHatNormCompositeContinuous :
    Additive (IdeleGroup K) →ₜ+ ZHat where
  __ := cyclotomicZHatNormComposite K
  continuous_toFun := by
    change
      Continuous
        (fun a : Additive (IdeleGroup K) =>
          Multiplicative.toAdd
            (rationalCyclotomicZHatIdeleValue
              (IdeleGroup.norm ℚ K (Additive.toMul a))))
    exact
      continuous_toAdd.comp
        (rationalCyclotomicZHatIdeleValue.continuous_toFun.comp
          ((IdeleGroup.norm_continuous ℚ K).comp
            continuous_toMul))

theorem

cyclotomicZHatNormCompositeContinuous_apply

L198 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicZHatNormCompositeContinuous_apply

Documentation

The continuous norm composite agrees pointwise with the underlying unnormalized cyclotomic norm composite.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem cyclotomicZHatNormCompositeContinuous_apply
    (a : IdeleGroup K) :
    cyclotomicZHatNormCompositeContinuous K (Additive.ofMul a) =
      Multiplicative.toAdd
        (rationalCyclotomicZHatIdeleValue
          (IdeleGroup.norm ℚ K a))

def

cyclotomicZHatNormCompositeInMulNatRangeContinuous

L208 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicZHatNormCompositeInMulNatRangeContinuous

Documentation

The unnormalized composite, continuously restricted to its actual multiple subgroup f_K ℤ̂.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · full declaration

def cyclotomicZHatNormCompositeInMulNatRangeContinuous :
    Additive (IdeleGroup K) →ₜ+
      (zHatMulNat
        (cyclotomicZHatIntersectionDegree K)).toAddMonoidHom.range where
  __ := cyclotomicZHatNormCompositeInMulNatRange K
  continuous_toFun := by
    apply Continuous.subtype_mk
    exact (cyclotomicZHatNormCompositeContinuous K).continuous_toFun

theorem

cyclotomicZHatNormCompositeInMulNatRangeContinuous_apply

L220 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicZHatNormCompositeInMulNatRangeContinuous_apply

Documentation

Coercing the continuous range-restricted norm composite recovers the underlying cyclotomic norm composite.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem cyclotomicZHatNormCompositeInMulNatRangeContinuous_apply
    (a : Additive (IdeleGroup K)) :
    (cyclotomicZHatNormCompositeInMulNatRangeContinuous K a :
        ZHat) =
      cyclotomicZHatNormComposite K a

def

normalizedCyclotomicZHatIdeleValueContinuous

L229 ↗

GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValueContinuous

Documentation

The normalized cyclotomic value on ideles as a genuine continuous additive homomorphism.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

def normalizedCyclotomicZHatIdeleValueContinuous :
    Additive (IdeleGroup K) →ₜ+ ZHat

theorem

normalizedCyclotomicZHatIdeleValueContinuous_apply

L239 ↗

GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValueContinuous_apply

Documentation

The continuous normalized cyclotomic value agrees pointwise with its underlying additive homomorphism.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem normalizedCyclotomicZHatIdeleValueContinuous_apply
    (a : Additive (IdeleGroup K)) :
    normalizedCyclotomicZHatIdeleValueContinuous K a =
      normalizedCyclotomicZHatIdeleValue K a

def

normalizedCyclotomicZHatIdeleValueContinuousMul

L248 ↗

GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValueContinuousMul

Documentation

The normalized cyclotomic value in continuous multiplicative notation. This is the source homomorphism which descends through the principal-idèle quotient once the rational principal product formula has been established.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · full declaration

def normalizedCyclotomicZHatIdeleValueContinuousMul :
    IdeleGroup K →ₜ* Multiplicative ZHat where
  toMonoidHom :=
    AddMonoidHom.toMultiplicativeRight
      (normalizedCyclotomicZHatIdeleValueContinuous K).toAddMonoidHom
  continuous_toFun :=
    continuous_ofAdd.comp
      ((normalizedCyclotomicZHatIdeleValueContinuous K).continuous_toFun.comp
        continuous_toAdd)

theorem

normalizedCyclotomicZHatIdeleValueContinuousMul_apply

L261 ↗

GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValueContinuousMul_apply

Documentation

The multiplicative continuous normalized value is the multiplicative form of the underlying additive normalized value.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem normalizedCyclotomicZHatIdeleValueContinuousMul_apply
    (a : IdeleGroup K) :
    normalizedCyclotomicZHatIdeleValueContinuousMul K a =
      Multiplicative.ofAdd
        (normalizedCyclotomicZHatIdeleValue K
          (Additive.ofMul a))

theorem

normalizedCyclotomicZHatIdeleValue_normOne_denseRange

L272 ↗

GlobalClassFieldTheory.Reciprocity.normalizedCyclotomicZHatIdeleValue_normOne_denseRange

Documentation

The actual norm-one ideles already have dense normalized cyclotomic value. The source reduction uses the positive archimedean correction, whose cyclotomic value is trivial.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable (K : Type) [Field K] [NumberField K]

Lean source · full declaration

theorem normalizedCyclotomicZHatIdeleValue_normOne_denseRange :
    DenseRange
      (fun b : IdeleGroup.normOneSubgroup (K := K) =>
        normalizedCyclotomicZHatIdeleValue K
          (Additive.ofMul (b : IdeleGroup K))) := by
  apply (normalizedCyclotomicZHatIdeleValue_denseRange K).mono
  rintro z ⟨a, rfl⟩
  obtain ⟨b, hb⟩ :=
    exists_normOneIdele_same_normalizedCyclotomicZHatIdeleValue
      K (Additive.toMul a)
  refine ⟨b, ?_⟩
  simpa using hb

Module documentation

Topology of the rational cyclotomic idele value

Declarations