Module

Main.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.Main

6 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: the local reciprocity law

The residue Frobenius datum, the normalized henselian valuation, and the class-field axiom constructed over the fixed separable closure are inserted into the abstract reciprocity theorem. The resulting isomorphism is independent of the embedding used to realize the finite Galois extension in that closure.

Imports4

Imported by9

def

abelianizationEquivNormQuotient

L40 ↗

LocalClassFieldTheory.abelianizationEquivNormQuotient

Documentation

Finite local reciprocity (Local Reciprocity Law). For every finite Galois extension of nonarchimedean local fields, reciprocity gives the canonical isomorphism G(L/K)ᵃᵇ ≃ Kˣ / N_{L/K}(Lˣ).

The coefficient module used in the construction is (SeparableClosure K)ˣ, in the fixed-separable-closure model.

Source context 4 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
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 abelianizationEquivNormQuotient :
    Abelianization (Gal(L / K)) ≃* NormQuotient K L

theorem

abelianizationEquivNormQuotient_eq_of_embedding

L50 ↗

LocalClassFieldTheory.abelianizationEquivNormQuotient_eq_of_embedding

Documentation

The isomorphism in the finite local reciprocity construction is independent of the embedding used to realize L/K inside the fixed separable closure.

Source context 4 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
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 abelianizationEquivNormQuotient_eq_of_embedding
    (i : L →ₐ[K] SeparableClosure K) :
    abelianizationEquivNormQuotient K L =
      concreteReciprocityEquivOfEmbedding K L i
        (localResidueDatum K)
        (localHenselianValuation K)
        (separableClosureUnits_isClassFormation K)

def

localArtinMonoidHom

L66 ↗

LocalClassFieldTheory.localArtinMonoidHom

Documentation

The local norm-residue symbol is the inverse of reciprocity, preceded by the quotient map from Kˣ.

Source context 4 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
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 localArtinMonoidHom :
    Kˣ →* Abelianization (Gal(L / K))

theorem

localArtinMonoidHom_eq_of_embedding

L75 ↗

LocalClassFieldTheory.localArtinMonoidHom_eq_of_embedding

Documentation

The canonical local norm-residue symbol can be computed using any explicit realization of the finite Galois extension in the fixed separable closure. This is the symbol-level form of the embedding independence in the finite local reciprocity construction.

Source context 4 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
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 localArtinMonoidHom_eq_of_embedding
    (i : L →ₐ[K] SeparableClosure K) :
    localArtinMonoidHom K L =
      concreteNormResidueSymbolOfEmbedding K L i
        (localResidueDatum K)
        (localHenselianValuation K)
        (separableClosureUnits_isClassFormation K)

theorem

localArtinMonoidHom_surjective

L94 ↗

LocalClassFieldTheory.localArtinMonoidHom_surjective

Documentation

The local norm-residue symbol of the finite local reciprocity construction is surjective.

Source context 4 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
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 localArtinMonoidHom_surjective :
    Function.Surjective (localArtinMonoidHom K L)

theorem

localArtinMonoidHom_ker

L101 ↗

LocalClassFieldTheory.localArtinMonoidHom_ker

Documentation

The kernel of the local norm-residue symbol is exactly the norm subgroup N_{L/K}(Lˣ).

Source context 4 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
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 localArtinMonoidHom_ker :
    (localArtinMonoidHom K L).ker = localNormSubgroup K L

Module documentation

Finite local reciprocity: the local reciprocity law

Declarations

abelianizationEquivNormQuotient

abelianizationEquivNormQuotient_eq_of_embedding

localArtinMonoidHom

localArtinMonoidHom_eq_of_embedding

localArtinMonoidHom_surjective

localArtinMonoidHom_ker