NYLL
Module

AbsoluteArtinRestriction.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteArtinRestriction
4 declarations indexed from sourceView source ↗

Module documentation

Actual finite values of the absolute local Artin map

Projecting the absolute Artin map to a finite abelian subextension recovers its canonical finite Artin map, not merely the same norm kernel.

Imports1
Imported by3

Declarations

theorem

absoluteAbelianRestriction_finiteProjection

L26 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteAbelianRestriction_finiteProjection
Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem absoluteAbelianRestriction_finiteProjection
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K))
    (x : localAbsoluteAbelianProfinite K) :
    absoluteAbelianRestriction K (absoluteFiniteQuotientField K N) x =
      absoluteFiniteQuotientEquiv K N (QuotientGroup.mk x)
theorem

separableAbsoluteLocalArtinMap_finiteQuotientRestriction

L34 ↗
ClassFieldTower.Martinet.Shafarevich.separableAbsoluteLocalArtinMap_finiteQuotientRestriction
Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableAbsoluteLocalArtinMap_finiteQuotientRestriction
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) (a : Kˣ) :
    absoluteAbelianRestriction K (absoluteFiniteQuotientField K N)
        (separableAbsoluteLocalArtinMap K a) =
      abelianLocalArtinMap K (absoluteFiniteQuotientField K N) a
theorem

separableAbsoluteLocalArtinMap_restriction

L47 ↗
ClassFieldTower.Martinet.Shafarevich.separableAbsoluteLocalArtinMap_restriction
Documentation

The actual absolute Artin value restricts to the actual finite abelian local Artin value.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem separableAbsoluteLocalArtinMap_restriction
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] (a : Kˣ) :
    absoluteAbelianRestriction K E (separableAbsoluteLocalArtinMap K a) =
      abelianLocalArtinMap K E a
theorem

absoluteLocalArtinMap_restriction

L60 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteLocalArtinMap_restriction
Documentation

The same finite-value comparison for the usual algebraic-closure absolute Artin map.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem absoluteLocalArtinMap_restriction
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] (a : Kˣ) :
    absoluteAbelianRestriction K E
        ((separableToStandardAbsoluteAbelianizationEquiv K).symm
          (absoluteLocalArtinMap K a)) =
      abelianLocalArtinMap K E a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.