Module

NormResidueNaturality.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.NormResidueNaturality

3 declarations indexed from sourceView source ↗

Module documentation

Restriction naturality of the actual abelian local Artin map

The actual algebraic and continuous Artin maps commute with restriction between finite abelian intermediate fields of the fixed separable closure.

Imports2

Imported by13

def

intermediateFieldRestrictContinuous

L32 ↗

LocalClassFieldTheory.intermediateFieldRestrictContinuous

Documentation

Restriction between the actual Galois groups of two finite intermediate fields, bundled as a continuous homomorphism for their finite Krull topologies.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

def intermediateFieldRestrictContinuous
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsGalois K E] [IsGalois K F] :
    Gal(F / K) →ₜ* Gal(E / K)

theorem

abelianLocalArtinMonoidHom_restrict

L42 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_restrict

Documentation

Finite Artin homomorphisms commute with restriction along a tower of finite abelian intermediate fields.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

theorem abelianLocalArtinMonoidHom_restrict
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F] :
    (intermediateFieldRestrictNormalHom E F hEF).comp
        (abelianLocalArtinMonoidHom K F) =
      abelianLocalArtinMonoidHom K E

theorem

abelianLocalArtinMap_restrict

L55 ↗

LocalClassFieldTheory.abelianLocalArtinMap_restrict

Documentation

The continuous actual finite Artin maps commute with restriction along a tower of finite abelian intermediate fields.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

theorem abelianLocalArtinMap_restrict
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F] :
    (intermediateFieldRestrictContinuous K E F hEF).comp
        (abelianLocalArtinMap K F) =
      abelianLocalArtinMap K E

Module documentation

Restriction naturality of the actual abelian local Artin map

Declarations

intermediateFieldRestrictContinuous

abelianLocalArtinMonoidHom_restrict

abelianLocalArtinMap_restrict