NYLL
Module

TopologicalGlobalNormResidue.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.TopologicalGlobalNormResidue
11 declarations indexed from sourceView source ↗

Module documentation

Topological global norm-residue reciprocity

For a finite abelian extension of number fields, the genuine idele-class norm range is open in the ordinary idele-class topology. Hence its native quotient topology is discrete. The finite Krull Galois group is discrete as well, so the algebraic global norm-residue equivalence upgrades to a homeomorphic multiplicative equivalence.

This file also bundles the quotient map and the global norm-residue map as continuous homomorphisms, and proves that forgetting their topology recovers the previously constructed actual global norm-residue symbol.

Imports4
Imported by4

Declarations

def

topologicalNormResidueIdeleClassCommGroup

L38 ↗
GlobalClassFieldTheory.Reciprocity.topologicalNormResidueIdeleClassCommGroup
Documentation

Fix the canonical class-group dictionary before bundling norm-quotient maps.

Source context 5 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
Lean source · statement
def topologicalNormResidueIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)
theorem

topologicalNormResidueIdeleClassIsMulCommutative

L45 ↗
GlobalClassFieldTheory.Reciprocity.topologicalNormResidueIdeleClassIsMulCommutative
Source context 6 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
Lean source · statement
theorem topologicalNormResidueIdeleClassIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

ideleClassNormQuotient_discreteTopology

L60 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassNormQuotient_discreteTopology
Documentation

The native quotient topology on C_K / N_{L/K}(C_L) is discrete because the genuine ordinary idele-class norm range is open.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem ideleClassNormQuotient_discreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
def

globalNormResidueContinuousMulEquiv

L73 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueContinuousMulEquiv
Documentation

Global norm-residue reciprocity as a homeomorphic multiplicative equivalence between the native norm quotient and the finite Krull Galois group. Both directions are continuous in their genuine topologies.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def globalNormResidueContinuousMulEquiv :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃ₜ*
      Gal(L / K)
theorem

globalNormResidueContinuousMulEquiv_apply

L95 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueContinuousMulEquiv_apply
Documentation

Evaluation of the topological norm-residue equivalence is the existing actual norm-residue equivalence on the same quotient class.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem globalNormResidueContinuousMulEquiv_apply
    (c :
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :
    globalNormResidueContinuousMulEquiv K L c =
      Additive.toMul
        (globalNormResidueEquiv K L
          (Additive.ofMul c))
def

globalReciprocityContinuousMulEquiv

L114 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityContinuousMulEquiv
Documentation

Global reciprocity in the direction used by the class-field correspondence,

Gal(L / K) ≃ₜ* C_K / N_{L/K}(C_L).

This is the inverse of the norm-residue equivalence as a ContinuousMulEquiv, so the Krull topology on the finite Galois group and the native quotient topology on the idele-class quotient are part of the public statement.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def globalReciprocityContinuousMulEquiv :
    Gal(L / K) ≃ₜ*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

globalReciprocityContinuousMulEquiv_apply

L124 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityContinuousMulEquiv_apply
Documentation

Evaluation of topological global reciprocity is the inverse of the actual norm-residue equivalence, with no additional choice of an abstract group isomorphism.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem globalReciprocityContinuousMulEquiv_apply
    (σ : Gal(L/K)) :
    globalReciprocityContinuousMulEquiv K L σ =
      Additive.toMul
        ((globalNormResidueEquiv K L).symm
          (Additive.ofMul σ))
def

ideleClassNormQuotientContinuousMonoidHom

L135 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassNormQuotientContinuousMonoidHom
Documentation

The genuine quotient map C_K → C_K / N_{L/K}(C_L), bundled with continuity for the native ordinary quotient topology.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def ideleClassNormQuotientContinuousMonoidHom :
    IdeleClassGroup K →ₜ*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
def

globalNormResidueContinuousMonoidHom

L145 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueContinuousMonoidHom
Documentation

The actual global norm-residue map, bundled as a continuous homomorphism on the ordinary idele-class topology.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def globalNormResidueContinuousMonoidHom :
    IdeleClassGroup K →ₜ* Gal(L / K)
theorem

globalNormResidueContinuousMonoidHom_apply

L154 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueContinuousMonoidHom_apply
Documentation

Evaluation of the continuous global norm-residue map agrees with the existing actual global norm-residue symbol.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem globalNormResidueContinuousMonoidHom_apply
    (c : IdeleClassGroup K) :
    globalNormResidueContinuousMonoidHom K L c =
      globalNormResidueMonoidHom K L c
theorem

globalNormResidueMonoidHom_continuous

L162 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_continuous
Documentation

The existing actual global norm-residue homomorphism is continuous for the ordinary idele-class topology and the finite Krull topology.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] topologicalNormResidueIdeleClassCommGroup
attribute [local instance] topologicalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem globalNormResidueMonoidHom_continuous :
    Continuous (globalNormResidueMonoidHom K L)

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