Module

FreeProPH2.lean

Nyll.GaloisCohomology.ProP.FreeProPH2

4 declarations indexed from sourceView source ↗

Module documentation

Degree-two cohomology of a free pro-p group

This file proves that continuous degree-two cohomology with universe-lifted trivial ZMod p coefficients vanishes for the finite-basis free pro-p source used by a presentation. The proof is explicit: a homogeneous cocycle defines a twisted compact pro-p extension, projectivity supplies a continuous section, and the section gives a homogeneous degree-one primitive.

Imports4

Imported by2

theorem

normalizedCocycle_is_continuous_coboundary

L37 ↗

ClassFieldTower.ProP.normalizedCocycle_is_continuous_coboundary

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem normalizedCocycle_is_continuous_coboundary
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d)
    (z : Cohomology.trivialZModPCocyclesLifted p sourceData.carrier 2) :
    ∃ b : C(sourceData.carrier, A p), ∀ g h,
      b (g * h) = b g + b h + normalizedCocycle z g h

theorem

freeProP_continuousCohomologyZModPLifted_degree_two_π_apply_eq_zero

L107 ↗

ClassFieldTower.ProP.freeProP_continuousCohomologyZModPLifted_degree_two_π_apply_eq_zero

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem freeProP_continuousCohomologyZModPLifted_degree_two_π_apply_eq_zero
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d)
    (z : Cohomology.trivialZModPCocyclesLifted p sourceData.carrier 2) :
    ContinuousCohomology.π
        (Cohomology.trivialZModPLifted p sourceData.carrier) 2 z = 0

theorem

freeProP_continuousCohomologyZModPLifted_degree_two_π_eq_zero

L133 ↗

ClassFieldTower.ProP.freeProP_continuousCohomologyZModPLifted_degree_two_π_eq_zero

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem freeProP_continuousCohomologyZModPLifted_degree_two_π_eq_zero
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d) :
    ContinuousCohomology.π
        (Cohomology.trivialZModPLifted p sourceData.carrier) 2 = 0

theorem

freeProP_continuousCohomologyZModPLifted_degree_two_subsingleton

L145 ↗

ClassFieldTower.ProP.freeProP_continuousCohomologyZModPLifted_degree_two_subsingleton

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem freeProP_continuousCohomologyZModPLifted_degree_two_subsingleton
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d) :
    Subsingleton
      (Cohomology.continuousCohomologyZModPLifted p sourceData.carrier 2)

Module documentation

Degree-two cohomology of a free pro-p group

Declarations

normalizedCocycle_is_continuous_coboundary

freeProP_continuousCohomologyZModPLifted_degree_two_π_apply_eq_zero

freeProP_continuousCohomologyZModPLifted_degree_two_π_eq_zero

freeProP_continuousCohomologyZModPLifted_degree_two_subsingleton