Module

FiniteAbelianQuotientKernels.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.FiniteAbelianQuotientKernels

9 declarations indexed from sourceView source ↗

Module documentation

Kernels attached to finite abelian subextensions

Every finite abelian subextension of the fixed separable closure determines an open normal subgroup of the absolute topological abelianization. This module identifies its pullback along the absolute Artin map with the ordinary norm subgroup. The finite local existence theorem then shows that these pullbacks are cofinal among the open finite-index subgroups of the local multiplicative group.

Imports4

Imported by2

def

absoluteAbelianRestriction

L38 ↗

LocalClassFieldTheory.absoluteAbelianRestriction

Documentation

Restriction from the absolute topological abelianization to the Galois group of a finite abelian subextension.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · statement

def absoluteAbelianRestriction
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    localAbsoluteAbelianProfinite K →ₜ* Gal(E / K)

theorem

absoluteAbelianRestriction_mk

L68 ↗

LocalClassFieldTheory.absoluteAbelianRestriction_mk

Documentation

States the theorem absoluteAbelianRestriction_mk.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · statement

theorem absoluteAbelianRestriction_mk
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (σ : intrinsicAbsoluteGalois K) :
    absoluteAbelianRestriction K E
        (QuotientGroup.mk σ : localAbsoluteAbelianProfinite K) =
      AlgEquiv.restrictNormalHom E σ

theorem

absoluteAbelianRestriction_surjective

L79 ↗

LocalClassFieldTheory.absoluteAbelianRestriction_surjective

Documentation

Restriction to a finite Galois subextension is onto after passing to the absolute topological abelianization.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · statement

theorem absoluteAbelianRestriction_surjective
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    Function.Surjective (absoluteAbelianRestriction K E)

def

absoluteAbelianRestrictionKernel

L89 ↗

LocalClassFieldTheory.absoluteAbelianRestrictionKernel

Documentation

The open normal kernel attached to a finite abelian subextension.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · full declaration

def absoluteAbelianRestrictionKernel
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    OpenNormalSubgroup (localAbsoluteAbelianProfinite K) where
  toOpenSubgroup :=
    { toSubgroup := (absoluteAbelianRestriction K E).toMonoidHom.ker
      isOpen' := by
        change IsOpen ((absoluteAbelianRestriction K E) ⁻¹' {1})
        exact (isOpen_discrete {1}).preimage
          (absoluteAbelianRestriction K E).continuous_toFun }
  isNormal' := by infer_instance

theorem

mem_absoluteAbelianRestrictionKernel_iff

L103 ↗

LocalClassFieldTheory.mem_absoluteAbelianRestrictionKernel_iff

Documentation

States the theorem mem_absoluteAbelianRestrictionKernel_iff.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · statement

theorem mem_absoluteAbelianRestrictionKernel_iff
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (x : localAbsoluteAbelianProfinite K) :
    x ∈ absoluteAbelianRestrictionKernel K E ↔
      absoluteAbelianRestriction K E x = 1

theorem

absoluteFiniteQuotientPreimage_restrictionKernel

L113 ↗

LocalClassFieldTheory.absoluteFiniteQuotientPreimage_restrictionKernel

Documentation

Pulling the restriction kernel back to the absolute Galois group gives the fixing subgroup of the original finite subextension.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · statement

theorem absoluteFiniteQuotientPreimage_restrictionKernel
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    (absoluteFiniteQuotientPreimage K
      (absoluteAbelianRestrictionKernel K E)).toSubgroup =
        E.fixingSubgroup

theorem

absoluteFiniteQuotientField_restrictionKernel

L129 ↗

LocalClassFieldTheory.absoluteFiniteQuotientField_restrictionKernel

Documentation

The finite field cut out by the restriction kernel is the original finite abelian subextension.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]

Lean source · statement

theorem absoluteFiniteQuotientField_restrictionKernel
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    absoluteFiniteQuotientField K (absoluteAbelianRestrictionKernel K E) = E

theorem

separableAbsoluteLocalArtinMap_preimage_restrictionKernel

L146 ↗

LocalClassFieldTheory.separableAbsoluteLocalArtinMap_preimage_restrictionKernel

Documentation

Pulling a finite restriction kernel back along the absolute local Artin map gives exactly the norm subgroup of that finite abelian extension.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem separableAbsoluteLocalArtinMap_preimage_restrictionKernel
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    (topologicalProfiniteCompletionPreimageIndex
      (localAbsoluteAbelianProfinite K)
      (separableAbsoluteLocalArtinMap K)
      (absoluteAbelianRestrictionKernel K E)).toOpenNormalSubgroup.toSubgroup =
        localNormSubgroup K E

theorem

separableAbsoluteLocalArtinMap_preimage_cofinal

L188 ↗

LocalClassFieldTheory.separableAbsoluteLocalArtinMap_preimage_cofinal

Documentation

The pullbacks of finite abelian restriction kernels are cofinal among the open finite-index normal subgroups of Kˣ. This is the arithmetic input for injectivity of the canonical map from the topological profinite completion.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped IsMulCommutative
open LocalFieldTheory RamificationTheory
open ClassFormation CyclicCohomology
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem separableAbsoluteLocalArtinMap_preimage_cofinal
    (H : OpenFiniteIndexNormalSubgroup Kˣ) :
    ∃ N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K),
      topologicalProfiniteCompletionPreimageIndex
        (localAbsoluteAbelianProfinite K)
        (separableAbsoluteLocalArtinMap K) N ≤ H

Module documentation

Kernels attached to finite abelian subextensions

Declarations