Module

AbsoluteArtin.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteArtin

12 declarations indexed from sourceView source ↗

Module documentation

The absolute local Artin map from compatible finite quotients

Finite local reciprocity supplies a surjective Artin map at every open finite quotient of the absolute topological abelianization. This module assembles those maps into the absolute Artin map and records its finite-stage compatibility.

Imports1

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteFiniteQuotientTransitions

Imported by4

def

absoluteFiniteArtinMap

L33 ↗

LocalClassFieldTheory.absoluteFiniteArtinMap

Documentation

The finite Artin coordinate at an open normal subgroup of the absolute 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 absoluteFiniteArtinMap
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
    Kˣ →ₜ* (localAbsoluteAbelianProfinite K ⧸ N.toSubgroup)

theorem

absoluteFiniteArtinMap_surjective

L41 ↗

LocalClassFieldTheory.absoluteFiniteArtinMap_surjective

Documentation

Every finite coordinate of the absolute Artin map 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 absoluteFiniteArtinMap_surjective
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
    Function.Surjective (absoluteFiniteArtinMap K N)

theorem

absoluteFiniteArtinMap_ker

L50 ↗

LocalClassFieldTheory.absoluteFiniteArtinMap_ker

Documentation

The kernel of a finite absolute Artin coordinate is the ordinary norm subgroup of its corresponding finite abelian fixed field.

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 absoluteFiniteArtinMap_ker
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
    (absoluteFiniteArtinMap K N).toMonoidHom.ker =
      localNormSubgroup K (absoluteFiniteQuotientField K N)

theorem

absoluteFiniteArtinMap_transition

L65 ↗

LocalClassFieldTheory.absoluteFiniteArtinMap_transition

Documentation

Finite absolute Artin coordinates commute with quotient transition.

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 absoluteFiniteArtinMap_transition
    {N M : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)}
    (hNM : N ≤ M) :
    (absoluteFiniteQuotientTransition hNM).comp
        (absoluteFiniteArtinMap K N) =
      absoluteFiniteArtinMap K M

def

absoluteFiniteArtinLimit

L117 ↗

LocalClassFieldTheory.absoluteFiniteArtinLimit

Documentation

The compatible cone of finite Artin coordinates, valued in the inverse limit of all open finite quotients of the absolute abelianized 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 absoluteFiniteArtinLimit : ProfiniteGrp

def

absoluteGaloisAbelianizationLimitEquiv

L124 ↗

LocalClassFieldTheory.absoluteGaloisAbelianizationLimitEquiv

Documentation

The topological abelianization of the absolute Galois group is canonically the inverse limit of all of its finite quotients.

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 absoluteGaloisAbelianizationLimitEquiv :
    localAbsoluteAbelianProfinite K ≃ₜ*
      absoluteFiniteArtinLimit K

def

absoluteFiniteArtinLimitMap

L131 ↗

LocalClassFieldTheory.absoluteFiniteArtinLimitMap

Documentation

Defines absoluteFiniteArtinLimitMap.

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 · full declaration

def absoluteFiniteArtinLimitMap :
    Kˣ →ₜ* (absoluteFiniteArtinLimit K : Type) where
  toFun a :=
    ⟨fun N => absoluteFiniteArtinMap K N a, by
      intro N M i
      change
        absoluteFiniteQuotientTransition (K := K)
            (CategoryTheory.leOfHom i)
            (absoluteFiniteArtinMap K N a) =
          absoluteFiniteArtinMap K M a
      exact DFunLike.congr_fun
        (absoluteFiniteArtinMap_transition K
          (CategoryTheory.leOfHom i)) a⟩
  map_one' := by
    apply Subtype.ext
    funext N
    exact (absoluteFiniteArtinMap K N).map_one
  map_mul' x y := by
    apply Subtype.ext
    funext N
    exact (absoluteFiniteArtinMap K N).map_mul x y
  continuous_toFun := by
    apply continuous_induced_rng.mpr
    apply continuous_pi
    intro N
    let : DiscreteTopology
        (localAbsoluteAbelianProfinite K ⧸ N.toSubgroup) :=
      QuotientGroup.discreteTopology N.isOpen'
    let q :
        (localAbsoluteAbelianProfinite K ⧸ N.toSubgroup) →ₜ*
          (((localAbsoluteAbelianProfinite K).toFiniteQuotientFunctor ⋙
            forget₂ FiniteGrp ProfiniteGrp).obj N : Type) :=
      { toFun := id
        map_one' := rfl
        map_mul' := by intro x y; rfl
        continuous_toFun := continuous_of_discreteTopology }
    exact q.continuous_toFun.comp
      (absoluteFiniteArtinMap K N).continuous_toFun

theorem

absoluteFiniteArtinLimitMap_apply

L172 ↗

LocalClassFieldTheory.absoluteFiniteArtinLimitMap_apply

Documentation

States the theorem absoluteFiniteArtinLimitMap_apply.

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 absoluteFiniteArtinLimitMap_apply
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) (a : Kˣ) :
    (absoluteFiniteArtinLimitMap K a).1 N =
      absoluteFiniteArtinMap K N a

theorem

absoluteFiniteArtinLimitMap_denseRange

L180 ↗

LocalClassFieldTheory.absoluteFiniteArtinLimitMap_denseRange

Documentation

Surjectivity at every finite Artin coordinate makes the assembled cone dense in the inverse limit.

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 absoluteFiniteArtinLimitMap_denseRange :
    DenseRange (absoluteFiniteArtinLimitMap K)

def

separableAbsoluteLocalArtinMap

L214 ↗

LocalClassFieldTheory.separableAbsoluteLocalArtinMap

Documentation

The absolute local Artin map into the topological abelianization of the absolute Galois group of 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 separableAbsoluteLocalArtinMap :
    Kˣ →ₜ* localAbsoluteAbelianProfinite K

theorem

separableAbsoluteLocalArtinMap_finiteProjection

L223 ↗

LocalClassFieldTheory.separableAbsoluteLocalArtinMap_finiteProjection

Documentation

Projection of the absolute local Artin map to an open finite quotient is the corresponding finite local Artin coordinate.

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 separableAbsoluteLocalArtinMap_finiteProjection
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) (a : Kˣ) :
    QuotientGroup.mk' N.toSubgroup
        (separableAbsoluteLocalArtinMap K a) =
      absoluteFiniteArtinMap K N a

theorem

separableAbsoluteLocalArtinMap_denseRange

L237 ↗

LocalClassFieldTheory.separableAbsoluteLocalArtinMap_denseRange

Documentation

The 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 separableAbsoluteLocalArtinMap_denseRange :
    DenseRange (separableAbsoluteLocalArtinMap K)

Module documentation

The absolute local Artin map from compatible finite quotients

Declarations