Module

AbsoluteUnramifiedH2Quotient.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteUnramifiedH2Quotient

4 declarations indexed from sourceView source ↗

Module documentation

Degree-two cohomology of the absolute unramified quotient

The topological first-isomorphism equivalence for absolute restriction identifies degree-two continuous cohomology of the maximal everywhere-unramified pro-p Galois group with that of the corresponding quotient of the absolute Galois group.

Imports2

Imported by2

def

absoluteUnramifiedQuotientH2LinearEquiv

L34 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedQuotientH2LinearEquiv

Documentation

Pullback along the absolute unramified quotient equivalence identifies the two degree-two continuous cohomology spaces with trivial lifted ZMod p coefficients.

Source context 8 commands

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

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

Lean source · statement

def absoluteUnramifiedQuotientH2LinearEquiv :
    continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2 ≃ₗ[ZMod p]
      continuousCohomologyZModPLifted p
        (Field.absoluteGaloisGroup F ⧸
          (absoluteUnramifiedKernel F p).toSubgroup) 2

theorem

absoluteUnramifiedQuotientH2LinearEquiv_apply

L45 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedQuotientH2LinearEquiv_apply

Documentation

The forward equivalence is the cohomological pullback along the quotient equivalence.

Source context 8 commands

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

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

Lean source · statement

theorem absoluteUnramifiedQuotientH2LinearEquiv_apply
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) :
    absoluteUnramifiedQuotientH2LinearEquiv F p x =
      (continuousCohomologyZModPMapLifted p
        (absoluteUnramifiedQuotientContinuousMulEquiv F p) 2).hom x

theorem

absoluteUnramifiedQuotientH2LinearEquiv_eq_zero_iff

L55 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedQuotientH2LinearEquiv_eq_zero_iff

Documentation

Pullback to the absolute unramified quotient detects the zero class.

Source context 8 commands

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

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

Lean source · statement

theorem absoluteUnramifiedQuotientH2LinearEquiv_eq_zero_iff
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) :
    absoluteUnramifiedQuotientH2LinearEquiv F p x = 0 ↔ x = 0

theorem

absoluteUnramifiedQuotientH2LinearEquiv_injective

L62 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedQuotientH2LinearEquiv_injective

Documentation

Pullback to the absolute unramified quotient is injective.

Source context 8 commands

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

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

Lean source · statement

theorem absoluteUnramifiedQuotientH2LinearEquiv_injective :
    Function.Injective (absoluteUnramifiedQuotientH2LinearEquiv F p)

Module documentation

Degree-two cohomology of the absolute unramified quotient

Declarations

absoluteUnramifiedQuotientH2LinearEquiv

absoluteUnramifiedQuotientH2LinearEquiv_apply

absoluteUnramifiedQuotientH2LinearEquiv_eq_zero_iff

absoluteUnramifiedQuotientH2LinearEquiv_injective