Module

LocalUnramifiedH2Vanishing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.LocalUnramifiedH2Vanishing

5 declarations indexed from sourceView source ↗

Module documentation

Vanishing of local unramified degree-two cohomology

For a nonarchimedean local field, the continuous residue-degree map is onto the profinite integers. Its kernel is the kernel of the residue action, and the corresponding quotient is therefore continuously equivalent to ZHatMul. Continuous degree-two cohomology of this unramified quotient with trivial ZMod p coefficients vanishes.

Imports3

Imported by3

theorem

localResidueDegree_ker_eq_residueAction_ker

L37 ↗

ClassFieldTower.Martinet.Shafarevich.localResidueDegree_ker_eq_residueAction_ker

Documentation

The kernel of the local residue degree is exactly the kernel of the residue action.

Source context 10 commands

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

open CategoryTheory LocalFieldTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFormation
open LocalClassFieldTheory
open ProCGroups
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem localResidueDegree_ker_eq_residueAction_ker :
    MonoidHom.ker (localResidueDegree K).toMonoidHom =
      MonoidHom.ker (localSeparableResidueAlgAction K).toMonoidHom

abbrev

LocalUnramifiedGaloisQuotient

L75 ↗

ClassFieldTower.Martinet.Shafarevich.LocalUnramifiedGaloisQuotient

Documentation

The Galois quotient detected by the local residue-degree map.

Source context 10 commands

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

open CategoryTheory LocalFieldTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFormation
open LocalClassFieldTheory
open ProCGroups
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

abbrev LocalUnramifiedGaloisQuotient

def

localUnramifiedQuotientContinuousMulEquiv

L80 ↗

ClassFieldTower.Martinet.Shafarevich.localUnramifiedQuotientContinuousMulEquiv

Documentation

The local unramified Galois quotient is continuously equivalent to the profinite integers.

Source context 10 commands

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

open CategoryTheory LocalFieldTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFormation
open LocalClassFieldTheory
open ProCGroups
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

def localUnramifiedQuotientContinuousMulEquiv :
    LocalUnramifiedGaloisQuotient K ≃ₜ* ZHatMul

def

localUnramifiedQuotientH2LinearEquiv

L98 ↗

ClassFieldTower.Martinet.Shafarevich.localUnramifiedQuotientH2LinearEquiv

Documentation

Pullback along the unramified quotient equivalence identifies its degree-two cohomology with degree-two cohomology of the profinite integers.

Source context 11 commands

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

open CategoryTheory LocalFieldTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFormation
open LocalClassFieldTheory
open ProCGroups
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def localUnramifiedQuotientH2LinearEquiv :
    continuousCohomologyZModPLifted p ZHatMul 2 ≃ₗ[ZMod p]
      continuousCohomologyZModPLifted p (LocalUnramifiedGaloisQuotient K) 2

theorem

localUnramifiedQuotientH2_subsingleton

L106 ↗

ClassFieldTower.Martinet.Shafarevich.localUnramifiedQuotientH2_subsingleton

Documentation

Continuous H² of the local unramified quotient with trivial ZMod p coefficients vanishes.

Source context 11 commands

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

open CategoryTheory LocalFieldTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFormation
open LocalClassFieldTheory
open ProCGroups
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem localUnramifiedQuotientH2_subsingleton :
    Subsingleton
      (continuousCohomologyZModPLifted p (LocalUnramifiedGaloisQuotient K) 2)

Module documentation

Vanishing of local unramified degree-two cohomology

Declarations

localResidueDegree_ker_eq_residueAction_ker

LocalUnramifiedGaloisQuotient

localUnramifiedQuotientContinuousMulEquiv

localUnramifiedQuotientH2LinearEquiv

localUnramifiedQuotientH2_subsingleton