Module

AbsoluteUnramifiedFiniteStageTransgression.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteUnramifiedFiniteStageTransgression

5 declarations indexed from sourceView source ↗

Module documentation

Finite-stage transgression for the absolute unramified quotient

For an open normal finite p-quotient of the absolute Galois group, finite transgression first lands in the degree-two cohomology of the absolute group modulo its unramified kernel. The topological quotient equivalence then transports that class back to the degree-two cohomology of the maximal everywhere-unramified pro-p Galois group.

Imports2

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

instance

absoluteFiniteStageCompactSpace

L35 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteFiniteStageCompactSpace

Source context 10 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
open ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

instance absoluteFiniteStageCompactSpace :
    CompactSpace (Field.absoluteGaloisGroup F)

def

absoluteUnramifiedFiniteStageTransgressionLinearMap

L42 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedFiniteStageTransgressionLinearMap

Documentation

Finite-stage transgression for the absolute unramified kernel, transported from the quotient of the absolute Galois group to the maximal everywhere-unramified pro-p Galois group.

Source context 10 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
open ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def absoluteUnramifiedFiniteStageTransgressionLinearMap
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p)
      (Field.absoluteGaloisGroup F)) :
    InvariantFiniteCharacter (p := p)
        (finiteStageImage (absoluteUnramifiedKernel F p) U) →ₗ[ZMod p]
      continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2

theorem

absoluteUnramifiedFiniteStageTransgressionLinearMap_apply

L56 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedFiniteStageTransgressionLinearMap_apply

Documentation

The absolute finite-stage map is inflated transgression followed by inverse transport across the quotient cohomology equivalence.

Source context 10 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
open ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedFiniteStageTransgressionLinearMap_apply
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p)
      (Field.absoluteGaloisGroup F))
    (χ : InvariantFiniteCharacter (p := p)
      (finiteStageImage (absoluteUnramifiedKernel F p) U)) :
    absoluteUnramifiedFiniteStageTransgressionLinearMap F p U χ =
      (absoluteUnramifiedQuotientH2LinearEquiv F p).symm
        (inflatedFiniteTransgressionLinearMap
          (absoluteUnramifiedKernel F p) U χ)

theorem

absoluteUnramifiedFiniteStageTransgressionLinearMap_zero

L69 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedFiniteStageTransgressionLinearMap_zero

Documentation

The zero invariant character has zero absolute unramified transgression.

Source context 10 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
open ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedFiniteStageTransgressionLinearMap_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p)
      (Field.absoluteGaloisGroup F)) :
    absoluteUnramifiedFiniteStageTransgressionLinearMap F p U
        (0 : InvariantFiniteCharacter (p := p)
          (finiteStageImage (absoluteUnramifiedKernel F p) U)) = 0

theorem

absoluteUnramifiedFiniteStageTransgressionLinearMap_ker

L79 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedFiniteStageTransgressionLinearMap_ker

Documentation

Transport across the quotient cohomology equivalence does not change the kernel of finite- stage inflated transgression.

Source context 10 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
open ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedFiniteStageTransgressionLinearMap_ker
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p)
      (Field.absoluteGaloisGroup F)) :
    LinearMap.ker (absoluteUnramifiedFiniteStageTransgressionLinearMap F p U) =
      LinearMap.ker (inflatedFiniteTransgressionLinearMap
        (absoluteUnramifiedKernel F p) U)

Module documentation

Finite-stage transgression for the absolute unramified quotient

Declarations

absoluteFiniteStageCompactSpace

absoluteUnramifiedFiniteStageTransgressionLinearMap

absoluteUnramifiedFiniteStageTransgressionLinearMap_apply

absoluteUnramifiedFiniteStageTransgressionLinearMap_zero

absoluteUnramifiedFiniteStageTransgressionLinearMap_ker