NYLL
Module

TopologicalReciprocity.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.TopologicalReciprocity
20 declarations indexed from sourceView source ↗

Module documentation

Topological finite local reciprocity

This module upgrades the algebraic finite local reciprocity isomorphism to a homeomorphic group isomorphism. The key input is that the norm subgroup of a finite Galois extension is open. Consequently its quotient is discrete, as is the topological abelianization of the finite Krull Galois group.

Imports9
Imported by12

Declarations

instance

normQuotientTopologicalSpace

L36 ↗
LocalClassFieldTheory.normQuotientTopologicalSpace
Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L)
def

integerUnitNormMap

L48 ↗
LocalClassFieldTheory.integerUnitNormMap
Documentation

The norm map restricted to valuation-ring units upstairs.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
Lean source · statement
def integerUnitNormMap
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    [ValuativeRel L] : 𝒪[L]ˣ →* Kˣ
def

integerUnitNormSubgroup

L54 ↗
LocalClassFieldTheory.integerUnitNormSubgroup
Documentation

The image of valuation-ring units under the field norm.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
Lean source · statement
def integerUnitNormSubgroup
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    [ValuativeRel L] : Subgroup Kˣ
theorem

integerUnitNormSubgroup_isCompact

L59 ↗
LocalClassFieldTheory.integerUnitNormSubgroup_isCompact
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
Lean source · statement
theorem integerUnitNormSubgroup_isCompact
    (K L : Type u) [NontriviallyNormedField K] [NormedField L]
    [NormedAlgebra K L] [FiniteDimensional K L] [CompleteSpace K]
    [ValuativeRel L] [CompactSpace 𝒪[L]] :
    IsCompact (integerUnitNormSubgroup K L : Set Kˣ)
theorem

integerUnitNormSubgroup_eq_localNormSubgroup_inf_baseUnits

L72 ↗
LocalClassFieldTheory.integerUnitNormSubgroup_eq_localNormSubgroup_inf_baseUnits
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
Lean source · statement
theorem integerUnitNormSubgroup_eq_localNormSubgroup_inf_baseUnits
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    integerUnitNormSubgroup K L =
      localNormSubgroup K L ⊓ localBaseUnitSubgroup K
theorem

localNormSubgroup_isOpen_of_compatibleLocalField

L125 ↗
LocalClassFieldTheory.localNormSubgroup_isOpen_of_compatibleLocalField
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
Lean source · statement
theorem localNormSubgroup_isOpen_of_compatibleLocalField
    (K L : Type)
    [NontriviallyNormedField K] [NormedField L] [NormedAlgebra K L]
    [CompleteSpace K]
    [ValuativeRel K] [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [IsNonarchimedeanLocalField L]
    [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    IsOpen (localNormSubgroup K L : Set Kˣ)
theorem

localNormSubgroup_isOpen

L220 ↗
LocalClassFieldTheory.localNormSubgroup_isOpen
Documentation

The norm subgroup of a finite Galois extension of a nonarchimedean local field is open in the native topology of the base-field unit group.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
open _root_.ValuationTheory.DiscreteValuationField.Valuation (
  valuationSubring_isIntegralClosure_of_isIntegral
) in
Lean source · statement
theorem localNormSubgroup_isOpen
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    IsOpen (localNormSubgroup K L : Set Kˣ)
theorem

normQuotient_discrete

L334 ↗
LocalClassFieldTheory.normQuotient_discrete
Documentation

The native quotient topology on the finite norm quotient is discrete.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section NormSubgroupTopology
universe u
Lean source · statement
theorem normQuotient_discrete
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    DiscreteTopology (NormQuotient K L)
theorem

commutator_topologicalClosure_eq

L353 ↗
LocalClassFieldTheory.commutator_topologicalClosure_eq
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem commutator_topologicalClosure_eq
    (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [DiscreteTopology G] :
    Subgroup.topologicalClosure (commutator G) = commutator G
def

topologicalAbelianization_finite_equiv

L363 ↗
LocalClassFieldTheory.topologicalAbelianization_finite_equiv
Documentation

For a finite-dimensional Galois extension, algebraic and topological abelianization agree as multiplicative groups.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def topologicalAbelianization_finite_equiv :
    Abelianization (Gal(L / K)) ≃* TopologicalAbelianization (Gal(L / K))
def

localReciprocityEquiv

L372 ↗
LocalClassFieldTheory.localReciprocityEquiv
Documentation

Finite local reciprocity as a homeomorphic group isomorphism from the norm quotient to the topological abelianization of the Krull Galois group.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def localReciprocityEquiv :
    NormQuotient K L ≃ₜ* TopologicalAbelianization (Gal(L / K))
theorem

localReciprocityEquiv_toMulEquiv

L387 ↗
LocalClassFieldTheory.localReciprocityEquiv_toMulEquiv
Documentation

The underlying multiplicative equivalence is the algebraic reciprocity isomorphism followed by the finite abelianization comparison.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localReciprocityEquiv_toMulEquiv :
    (localReciprocityEquiv K L).toMulEquiv =
      (abelianizationEquivNormQuotient K L).symm.trans
        (topologicalAbelianization_finite_equiv K L)
def

normClassContinuous

L395 ↗
LocalClassFieldTheory.normClassContinuous
Documentation

The quotient map to the norm quotient, bundled as a continuous homomorphism for the native quotient topology.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def normClassContinuous :
    Kˣ →ₜ* NormQuotient K L
def

localArtinMap

L401 ↗
LocalClassFieldTheory.localArtinMap
Documentation

The continuous finite local Artin map.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def localArtinMap :
    Kˣ →ₜ* TopologicalAbelianization (Gal(L / K))
theorem

localArtinMap_toMonoidHom

L408 ↗
LocalClassFieldTheory.localArtinMap_toMonoidHom
Documentation

Forgetting the topology and comparing finite abelianizations recovers the algebraic local Artin homomorphism.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localArtinMap_toMonoidHom :
    (topologicalAbelianization_finite_equiv K L).symm.toMonoidHom.comp
        (localArtinMap K L).toMonoidHom =
      localArtinMonoidHom K L
theorem

localArtinMap_embedding_independent

L431 ↗
LocalClassFieldTheory.localArtinMap_embedding_independent
Documentation

The continuous local Artin map is canonical: after forgetting topology, it agrees with the reciprocity symbol computed from any realization of the extension in the fixed separable closure.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localArtinMap_embedding_independent
    (i : L →ₐ[K] SeparableClosure K) :
    (topologicalAbelianization_finite_equiv K L).symm.toMonoidHom.comp
        (localArtinMap K L).toMonoidHom =
      concreteNormResidueSymbolOfEmbedding K L i
        (localResidueDatum K)
        (localHenselianValuation K)
        (separableClosureUnits_isClassFormation K)
theorem

localArtinMap_surjective

L443 ↗
LocalClassFieldTheory.localArtinMap_surjective
Documentation

The continuous finite local Artin map is surjective.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localArtinMap_surjective :
    Function.Surjective (localArtinMap K L)
theorem

localArtinMap_ker

L450 ↗
LocalClassFieldTheory.localArtinMap_ker
Documentation

The kernel of the continuous finite local Artin map is the norm subgroup.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localArtinMap_ker :
    (localArtinMap K L).toMonoidHom.ker = localNormSubgroup K L
def

localArtinMap_quotientKerEquiv

L463 ↗
LocalClassFieldTheory.localArtinMap_quotientKerEquiv
Documentation

The canonical first-isomorphism equivalence induced by the continuous local Artin map.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def localArtinMap_quotientKerEquiv :
    Kˣ ⧸ (localArtinMap K L).toMonoidHom.ker ≃*
      TopologicalAbelianization (Gal(L / K))
theorem

localArtinMap_quotientKerEquiv_mk

L472 ↗
LocalClassFieldTheory.localArtinMap_quotientKerEquiv_mk
Documentation

The first-isomorphism equivalence sends the class of a field unit to its image under the local Artin map.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable local instance normQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
section TopologicalReciprocity
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localArtinMap_quotientKerEquiv_mk (x : Kˣ) :
    localArtinMap_quotientKerEquiv K L (QuotientGroup.mk x) =
      localArtinMap K L x

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