Module

AbsoluteUnramifiedH2Localization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteUnramifiedH2Localization

5 declarations indexed from sourceView source ↗

Module documentation

Localization of degree-two classes inflated from the unramified quotient

This file defines inflation from the maximal everywhere-unramified pro-p Galois group to the absolute Galois group and records its finite-place localization as pullback along the composite local decomposition map. Proving that this composite vanishes in degree two requires the missing local unramified-quotient cohomology comparison, so the file stops at the naturality endpoint.

Imports2

Imported by2

def

absoluteUnramifiedH2Inflation

L34 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2Inflation

Documentation

Inflation in degree two along absolute restriction to the maximal everywhere-unramified pro-p extension.

Source context 8 commands

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

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

Lean source · statement

def absoluteUnramifiedH2Inflation :
    continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2 →ₗ[ZMod p]
      continuousCohomologyZModPLifted p (Field.absoluteGaloisGroup F) 2

theorem

absoluteUnramifiedH2Inflation_apply

L42 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2Inflation_apply

Source context 8 commands

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

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

Lean source · statement

theorem absoluteUnramifiedH2Inflation_apply
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) :
    absoluteUnramifiedH2Inflation F p x =
      (continuousCohomologyZModPMapLifted p
        (absoluteToMaxEverywhereUnramifiedProP F p) 2).hom x

def

absoluteUnramifiedH2LocalizationFamily

L52 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2LocalizationFamily

Documentation

Simultaneous finite-place localization after inflation from the everywhere-unramified quotient.

Source context 8 commands

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

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

Lean source · statement

def absoluteUnramifiedH2LocalizationFamily :
    continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2 →ₗ[ZMod p]
      FinitePlaceH2LocalizationTarget F p

theorem

absoluteUnramifiedH2LocalizationFamily_apply

L60 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2LocalizationFamily_apply

Source context 8 commands

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

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

Lean source · statement

theorem absoluteUnramifiedH2LocalizationFamily_apply
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteUnramifiedH2LocalizationFamily F p x v =
      finitePlaceH2Localization F p v (absoluteUnramifiedH2Inflation F p x)

theorem

absoluteUnramifiedH2LocalizationFamily_component

L70 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2LocalizationFamily_component

Documentation

Each localized inflated class is pullback along the composite from the local decomposition group to the maximal everywhere-unramified pro-p Galois group.

Source context 8 commands

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

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

Lean source · statement

theorem absoluteUnramifiedH2LocalizationFamily_component
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteUnramifiedH2LocalizationFamily F p x v =
      (continuousCohomologyZModPMapLifted p
        ((absoluteToMaxEverywhereUnramifiedProP F p).comp
          (finitePlaceAbsoluteDecompositionInclusion F v)) 2).hom x

Module documentation

Localization of degree-two classes inflated from the unramified quotient

Declarations

absoluteUnramifiedH2Inflation

absoluteUnramifiedH2Inflation_apply

absoluteUnramifiedH2LocalizationFamily

absoluteUnramifiedH2LocalizationFamily_apply

absoluteUnramifiedH2LocalizationFamily_component