NYLL
Module

ProfiniteLocalReciprocity.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteLocalReciprocity
33 declarations indexed from sourceView source ↗

Module documentation

Profinite local reciprocity

The absolute Artin map constructed from the compatible finite reciprocity maps is transported from the fixed separable closure to Mathlib's usual algebraic-closure absolute Galois group. Its canonical extension to the topological profinite completion is then automatically onto. Injectivity is supplied by the arithmetic cofinality consequence of the finite local existence theorem.

Imports7
Imported by5

Declarations

def

standardToSeparableAbsoluteGaloisEquiv

L41 ↗
LocalClassFieldTheory.standardToSeparableAbsoluteGaloisEquiv
Documentation

Restriction to the separable closure gives the canonical topological identification between the usual and separable absolute Galois groups.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def standardToSeparableAbsoluteGaloisEquiv :
    _root_.Field.absoluteGaloisGroup K ≃ₜ* intrinsicAbsoluteGalois K
def

separableToStandardAbsoluteAbelianizationEquiv

L47 ↗
LocalClassFieldTheory.separableToStandardAbsoluteAbelianizationEquiv
Documentation

The induced canonical identification from the separable absolute topological abelianization to Mathlib's usual one.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def separableToStandardAbsoluteAbelianizationEquiv :
    TopologicalAbelianization (intrinsicAbsoluteGalois K) ≃ₜ*
      _root_.Field.absoluteGaloisGroupAbelianization K
instance

standardLocalAbsoluteAbelianization_totallyDisconnectedSpace

L54 ↗
LocalClassFieldTheory.standardLocalAbsoluteAbelianization_totallyDisconnectedSpace
Documentation

The separable model makes the standard absolute abelianization totally disconnected.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
instance standardLocalAbsoluteAbelianization_totallyDisconnectedSpace :
    TotallyDisconnectedSpace
      (_root_.Field.absoluteGaloisGroupAbelianization K)
instance

standardLocalAbsoluteAbelianization_compactSpace

L61 ↗
LocalClassFieldTheory.standardLocalAbsoluteAbelianization_compactSpace
Documentation

The standard absolute abelianization is compact via the separable-model equivalence.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
instance standardLocalAbsoluteAbelianization_compactSpace :
    CompactSpace (_root_.Field.absoluteGaloisGroupAbelianization K)
instance

standardLocalAbsoluteAbelianization_t2Space

L67 ↗
LocalClassFieldTheory.standardLocalAbsoluteAbelianization_t2Space
Documentation

The standard absolute abelianization is Hausdorff via the separable-model equivalence.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
instance standardLocalAbsoluteAbelianization_t2Space :
    T2Space (_root_.Field.absoluteGaloisGroupAbelianization K)
def

standardLocalAbsoluteAbelianProfinite

L81 ↗
LocalClassFieldTheory.standardLocalAbsoluteAbelianProfinite
Documentation

The usual absolute Galois topological abelianization, packaged as a stable profinite group.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def standardLocalAbsoluteAbelianProfinite
    (K : Type) [Field K] : ProfiniteGrp
def

separableProfiniteLocalReciprocityHom

L87 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocityHom
Documentation

The canonical extension of the separable absolute Artin map to the open-finite-quotient completion of the local multiplicative group.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def separableProfiniteLocalReciprocityHom :
    TopologicalProfiniteCompletion Kˣ →ₜ*
      localAbsoluteAbelianProfinite K
theorem

separableProfiniteLocalReciprocityHom_map

L96 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocityHom_map
Documentation

The separable reciprocity lift agrees with the Artin map on canonical completion points.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableProfiniteLocalReciprocityHom_map (a : Kˣ) :
    separableProfiniteLocalReciprocityHom K
        (topologicalProfiniteCompletionMap Kˣ a) =
      separableAbsoluteLocalArtinMap K a
theorem

separableProfiniteLocalReciprocityHom_comp_completionMap

L106 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocityHom_comp_completionMap
Documentation

Composing the separable reciprocity lift with the completion map recovers the Artin map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableProfiniteLocalReciprocityHom_comp_completionMap :
    (separableProfiniteLocalReciprocityHom K).comp
        (topologicalProfiniteCompletionMap Kˣ) =
      separableAbsoluteLocalArtinMap K
theorem

separableProfiniteLocalReciprocityHom_surjective

L115 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocityHom_surjective
Documentation

The separable profinite reciprocity homomorphism is onto.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableProfiniteLocalReciprocityHom_surjective :
    Function.Surjective (separableProfiniteLocalReciprocityHom K)
theorem

separableProfiniteLocalReciprocityHom_injective

L124 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocityHom_injective
Documentation

Finite local existence makes the separable profinite reciprocity homomorphism one-to-one.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableProfiniteLocalReciprocityHom_injective :
    Function.Injective (separableProfiniteLocalReciprocityHom K)
def

separableProfiniteLocalReciprocity

L132 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocity
Documentation

Profinite local reciprocity for the fixed separable closure.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def separableProfiniteLocalReciprocity :
    TopologicalProfiniteCompletion Kˣ ≃ₜ*
      localAbsoluteAbelianProfinite K
theorem

separableProfiniteLocalReciprocity_apply

L145 ↗
LocalClassFieldTheory.separableProfiniteLocalReciprocity_apply
Documentation

The separable reciprocity equivalence has the same underlying map as its lifted homomorphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableProfiniteLocalReciprocity_apply
    (x : TopologicalProfiniteCompletion Kˣ) :
    separableProfiniteLocalReciprocity K x =
      separableProfiniteLocalReciprocityHom K x
def

separableToStandardAbsoluteAbelianizationHom

L153 ↗
LocalClassFieldTheory.separableToStandardAbsoluteAbelianizationHom
Documentation

The forward transport from the separable to the usual absolute topological abelianization, as a continuous homomorphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def separableToStandardAbsoluteAbelianizationHom :
    localAbsoluteAbelianProfinite K →ₜ*
      standardLocalAbsoluteAbelianProfinite K
def

absoluteLocalArtinMap

L161 ↗
LocalClassFieldTheory.absoluteLocalArtinMap
Documentation

The absolute local Artin map with Mathlib's usual algebraic-closure absolute Galois group as target.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def absoluteLocalArtinMap :
    Kˣ →ₜ* standardLocalAbsoluteAbelianProfinite K
theorem

separableToStandardAbsoluteAbelianizationEquiv_symm_artinMap

L168 ↗
LocalClassFieldTheory.separableToStandardAbsoluteAbelianizationEquiv_symm_artinMap
Documentation

Transporting the separable Artin map to the standard model gives the absolute Artin map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableToStandardAbsoluteAbelianizationEquiv_symm_artinMap
    (a : Kˣ) :
    (separableToStandardAbsoluteAbelianizationEquiv K).symm
        (absoluteLocalArtinMap K a) =
      separableAbsoluteLocalArtinMap K a
theorem

absoluteLocalArtinMap_denseRange

L181 ↗
LocalClassFieldTheory.absoluteLocalArtinMap_denseRange
Documentation

The usual absolute local Artin map has dense image.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem absoluteLocalArtinMap_denseRange :
    DenseRange (absoluteLocalArtinMap K)
def

profiniteLocalReciprocityHom

L190 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom
Documentation

The canonical homomorphism from the topological profinite completion of K× to the usual absolute Galois topological abelianization.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def profiniteLocalReciprocityHom :
    TopologicalProfiniteCompletion Kˣ →ₜ*
      standardLocalAbsoluteAbelianProfinite K
theorem

profiniteLocalReciprocityHom_map

L199 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_map
Documentation

The standard reciprocity lift agrees with the absolute Artin map on canonical completion points.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_map (a : Kˣ) :
    profiniteLocalReciprocityHom K
        (topologicalProfiniteCompletionMap Kˣ a) =
      absoluteLocalArtinMap K a
theorem

profiniteLocalReciprocityHom_comp_completionMap

L208 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_comp_completionMap
Documentation

The profinite reciprocity homomorphism extends the absolute Artin map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_comp_completionMap :
    (profiniteLocalReciprocityHom K).comp
        (topologicalProfiniteCompletionMap Kˣ) =
      absoluteLocalArtinMap K
theorem

profiniteLocalReciprocityHom_surjective

L217 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_surjective
Documentation

Dense range of the absolute Artin map and compactness of the completion make the profinite reciprocity homomorphism onto.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_surjective :
    Function.Surjective (profiniteLocalReciprocityHom K)
theorem

profiniteLocalReciprocityHom_finiteProjection_map

L226 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_finiteProjection_map
Documentation

Finite target projections agree with projection of the absolute Artin map on the dense copy of K×.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_finiteProjection_map
    (N : OpenNormalSubgroup (standardLocalAbsoluteAbelianProfinite K))
    (a : Kˣ) :
    topologicalProfiniteCompletionFiniteProjection
        (standardLocalAbsoluteAbelianProfinite K) (absoluteLocalArtinMap K) N
        (topologicalProfiniteCompletionMap Kˣ a) =
      QuotientGroup.mk' N.toSubgroup (absoluteLocalArtinMap K a)
theorem

profiniteLocalReciprocityHom_unique

L238 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_unique
Documentation

The profinite reciprocity homomorphism is the unique continuous homomorphism extending the absolute local Artin map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_unique
    (f : TopologicalProfiniteCompletion Kˣ →ₜ*
      standardLocalAbsoluteAbelianProfinite K)
    (hf : f.comp (topologicalProfiniteCompletionMap Kˣ) =
      absoluteLocalArtinMap K) :
    f = profiniteLocalReciprocityHom K
theorem

profiniteLocalReciprocityHom_eq_transport

L249 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_eq_transport
Documentation

The canonical lift to the usual absolute abelianization is transport of the corresponding separable lift.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_eq_transport :
    profiniteLocalReciprocityHom K =
      (separableToStandardAbsoluteAbelianizationHom K).comp
        (separableProfiniteLocalReciprocityHom K)
theorem

profiniteLocalReciprocityHom_injective

L266 ↗
LocalClassFieldTheory.profiniteLocalReciprocityHom_injective
Documentation

The canonical lift to the usual absolute abelianization is one-to-one.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocityHom_injective :
    Function.Injective (profiniteLocalReciprocityHom K)
def

profiniteLocalReciprocity

L275 ↗
LocalClassFieldTheory.profiniteLocalReciprocity
Documentation

Profinite local reciprocity. The topological profinite completion of the local multiplicative group is canonically continuously isomorphic to the topological abelianization of Mathlib's usual absolute Galois group.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def profiniteLocalReciprocity :
    TopologicalProfiniteCompletion Kˣ ≃ₜ*
      standardLocalAbsoluteAbelianProfinite K
theorem

profiniteLocalReciprocity_apply

L288 ↗
LocalClassFieldTheory.profiniteLocalReciprocity_apply
Documentation

The standard reciprocity equivalence has the same underlying map as its lifted homomorphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocity_apply
    (x : TopologicalProfiniteCompletion Kˣ) :
    profiniteLocalReciprocity K x =
      profiniteLocalReciprocityHom K x
theorem

profiniteLocalReciprocity_completionMap

L297 ↗
LocalClassFieldTheory.profiniteLocalReciprocity_completionMap
Documentation

Profinite reciprocity restricts to the absolute local Artin map on the dense copy of the local multiplicative group.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocity_completionMap (a : Kˣ) :
    profiniteLocalReciprocity K
        (topologicalProfiniteCompletionMap Kˣ a) =
      absoluteLocalArtinMap K a
theorem

absoluteLocalArtinMap_injective

L304 ↗
LocalClassFieldTheory.absoluteLocalArtinMap_injective
Documentation

The absolute local Artin map is injective.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem absoluteLocalArtinMap_injective :
    Function.Injective (absoluteLocalArtinMap K)
theorem

profiniteLocalReciprocity_finiteProjection

L315 ↗
LocalClassFieldTheory.profiniteLocalReciprocity_finiteProjection
Documentation

Every finite quotient projection of profinite reciprocity is the finite projection canonically induced by the absolute local Artin map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocity_finiteProjection
    (N : OpenNormalSubgroup (standardLocalAbsoluteAbelianProfinite K))
    (x : TopologicalProfiniteCompletion Kˣ) :
    QuotientGroup.mk' N.toSubgroup (profiniteLocalReciprocity K x) =
      topologicalProfiniteCompletionFiniteProjection
        (standardLocalAbsoluteAbelianProfinite K) (absoluteLocalArtinMap K) N x
theorem

profiniteLocalReciprocity_unique

L368 ↗
LocalClassFieldTheory.profiniteLocalReciprocity_unique
Documentation

Profinite local reciprocity is the unique continuous multiplicative equivalence whose composite with the completion map is the absolute Artin map.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem profiniteLocalReciprocity_unique
    (e : TopologicalProfiniteCompletion Kˣ ≃ₜ*
      standardLocalAbsoluteAbelianProfinite K)
    (he : (ContinuousMonoidHom.toContinuousMonoidHom e).comp
        (topologicalProfiniteCompletionMap Kˣ) =
      absoluteLocalArtinMap K) :
    e = profiniteLocalReciprocity K
def

standardAbsoluteGaloisAbelianizationLimitEquiv

L383 ↗
LocalClassFieldTheory.standardAbsoluteGaloisAbelianizationLimitEquiv
Documentation

Mathlib's absolute Galois abelianization is canonically the inverse limit of its finite quotients, after transport from the fixed separable closure.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def standardAbsoluteGaloisAbelianizationLimitEquiv :
    ContinuousMulEquiv (standardLocalAbsoluteAbelianProfinite K)
      (absoluteFiniteArtinLimit K)
theorem

absoluteLocalArtinMap_finiteProjection

L393 ↗
LocalClassFieldTheory.absoluteLocalArtinMap_finiteProjection
Documentation

Every finite projection of the absolute Artin map is its corresponding finite local Artin coordinate after canonical transport to the separable closure model.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem absoluteLocalArtinMap_finiteProjection
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K))
    (a : Units K) :
    QuotientGroup.mk' N.toSubgroup
        ((separableToStandardAbsoluteAbelianizationEquiv K).symm
          (absoluteLocalArtinMap K a)) =
      absoluteFiniteArtinMap K N a

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