Module

NormResidue.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.NormResidue

8 declarations indexed from sourceView source ↗

Module documentation

The actual abelian local Artin map

For a finite abelian Galois extension, finite local reciprocity takes values in the actual Galois group, not merely its abelianization. This module provides both the algebraic homomorphism and its continuous refinement for the native topologies.

Imports3

Mathlib.GroupTheory.Abelianization.Defs
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.TopologicalReciprocity
Mathlib.FieldTheory.Galois.Abelian

Imported by10

def

abelianLocalArtinMonoidHom

L35 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom

Documentation

The finite local Artin homomorphism with values in the actual Galois group of an abelian extension.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def abelianLocalArtinMonoidHom :
    Kˣ →* Gal(L / K)

theorem

abelianLocalArtinMonoidHom_surjective

L41 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_surjective

Documentation

The actual abelian local Artin homomorphism is surjective.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem abelianLocalArtinMonoidHom_surjective :
    Function.Surjective (abelianLocalArtinMonoidHom K L)

theorem

abelianLocalArtinMonoidHom_ker

L48 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_ker

Documentation

The kernel of the actual abelian local Artin homomorphism is the norm subgroup.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem abelianLocalArtinMonoidHom_ker :
    MonoidHom.ker (abelianLocalArtinMonoidHom K L) =
      localNormSubgroup K L

def

topologicalAbelianizationEquivSelf

L64 ↗

LocalClassFieldTheory.topologicalAbelianizationEquivSelf

Documentation

For a finite abelian Galois extension, topological abelianization is canonically homeomorphic to the actual Galois group.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def topologicalAbelianizationEquivSelf :
    TopologicalAbelianization Gal(L / K) ≃ₜ* Gal(L / K)

def

abelianLocalArtinMap

L78 ↗

LocalClassFieldTheory.abelianLocalArtinMap

Documentation

The continuous local Artin map with values in the actual Galois group of a finite abelian extension.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def abelianLocalArtinMap :
    Kˣ →ₜ* Gal(L / K)

theorem

abelianLocalArtinMap_toMonoidHom

L86 ↗

LocalClassFieldTheory.abelianLocalArtinMap_toMonoidHom

Documentation

Forgetting topology from the continuous actual Artin map recovers the algebraic actual Artin homomorphism.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem abelianLocalArtinMap_toMonoidHom :
    (abelianLocalArtinMap K L).toMonoidHom =
      abelianLocalArtinMonoidHom K L

theorem

abelianLocalArtinMap_surjective

L98 ↗

LocalClassFieldTheory.abelianLocalArtinMap_surjective

Documentation

The continuous actual abelian local Artin map is surjective.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem abelianLocalArtinMap_surjective :
    Function.Surjective (abelianLocalArtinMap K L)

theorem

abelianLocalArtinMap_ker

L105 ↗

LocalClassFieldTheory.abelianLocalArtinMap_ker

Documentation

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

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped IsMulCommutative
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem abelianLocalArtinMap_ker :
    (abelianLocalArtinMap K L).toMonoidHom.ker =
      localNormSubgroup K L

Module documentation

The actual abelian local Artin map

Declarations