Module

FinitePlaceUnramifiedH2LocalizationVanishing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FinitePlaceUnramifiedH2LocalizationVanishing

5 declarations indexed from sourceView source ↗

Module documentation

Vanishing of localized unramified degree-two classes

At a finite place, absolute restriction to the maximal everywhere-unramified pro-p extension kills inertia. It therefore factors through the unramified quotient of the selected decomposition group. The chosen local comparison identifies that quotient with the standard local unramified quotient, whose continuous degree-two cohomology with trivial ZMod p coefficients vanishes.

Imports4

Imported by4

def

finitePlaceUnramifiedToMaxEverywhereUnramifiedProP

L40 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedToMaxEverywhereUnramifiedProP

Documentation

Absolute restriction from a finite-place decomposition group factors through its unramified quotient.

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
open LocalClassFieldTheory
open LocalFieldTheory
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def finitePlaceUnramifiedToMaxEverywhereUnramifiedProP
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v ⧸
        finitePlaceAbsoluteInertiaSubgroup F v →ₜ*
      MaxEverywhereUnramifiedProPGaloisGroup F p

theorem

finitePlaceUnramifiedToMaxEverywhereUnramifiedProP_mk

L68 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedToMaxEverywhereUnramifiedProP_mk

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
open LocalClassFieldTheory
open LocalFieldTheory
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finitePlaceUnramifiedToMaxEverywhereUnramifiedProP_mk
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    finitePlaceUnramifiedToMaxEverywhereUnramifiedProP F p v
        (QuotientGroup.mk' (finitePlaceAbsoluteInertiaSubgroup F v) sigma) =
      absoluteToMaxEverywhereUnramifiedProP F p sigma.1

theorem

finitePlaceUnramifiedQuotientH2_subsingleton

L78 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedQuotientH2_subsingleton

Documentation

The degree-two cohomology of the unramified quotient selected at a finite place is trivial.

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
open LocalClassFieldTheory
open LocalFieldTheory
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finitePlaceUnramifiedQuotientH2_subsingleton
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Subsingleton
      (continuousCohomologyZModPLifted p
        (finitePlaceAbsoluteDecompositionGroup F v ⧸
          finitePlaceAbsoluteInertiaSubgroup F v) 2)

theorem

absoluteUnramifiedH2LocalizationFamily_component_eq_zero

L105 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2LocalizationFamily_component_eq_zero

Documentation

Each finite-place localization of a degree-two class inflated from the maximal everywhere-unramified pro-p quotient vanishes.

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
open LocalClassFieldTheory
open LocalFieldTheory
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedH2LocalizationFamily_component_eq_zero
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteUnramifiedH2LocalizationFamily F p x v = 0

theorem

absoluteUnramifiedH2LocalizationFamily_eq_zero

L134 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2LocalizationFamily_eq_zero

Documentation

Localization after inflation from the maximal everywhere-unramified pro-p quotient is the zero linear map.

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
open LocalClassFieldTheory
open LocalFieldTheory
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedH2LocalizationFamily_eq_zero :
    absoluteUnramifiedH2LocalizationFamily F p = 0

Module documentation

Vanishing of localized unramified degree-two classes

Declarations

finitePlaceUnramifiedToMaxEverywhereUnramifiedProP

finitePlaceUnramifiedToMaxEverywhereUnramifiedProP_mk

finitePlaceUnramifiedQuotientH2_subsingleton

absoluteUnramifiedH2LocalizationFamily_component_eq_zero

absoluteUnramifiedH2LocalizationFamily_eq_zero