Module

RelationRankH2.lean

Nyll.GaloisCohomology.ProP.RelationRankH2

3 declarations indexed from sourceView source ↗

Module documentation

Minimal relation rank and degree-two continuous cohomology

The upper and lower presentation bounds identify the least relation count of a finitely minimally presented pro-p group with the dimension of its continuous degree-two cohomology with trivial ZMod p coefficients.

Imports2

Imported by3

def

h2Rank

L27 ↗

ClassFieldTower.ProP.h2Rank

Documentation

The dimension of continuous degree-two cohomology with trivial ZMod p coefficients.

Source context 4 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
noncomputable section
universe u

Lean source · statement

def h2Rank (p : ℕ)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ

theorem

h2Rank_eq_finrank

L32 ↗

ClassFieldTower.ProP.h2Rank_eq_finrank

Source context 4 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
noncomputable section
universe u

Lean source · statement

theorem h2Rank_eq_finrank
    {p : ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    h2Rank p G = Module.finrank (ZMod p)
      (Cohomology.continuousCohomologyZModPLifted p G 2)

theorem

minimalRelationRank_eq_h2Rank

L44 ↗

ClassFieldTower.ProP.minimalRelationRank_eq_h2Rank

Documentation

For a finitely minimally presented pro-p group, relation rank equals H² rank.

Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem minimalRelationRank_eq_h2Rank
    (hG : HasFiniteMinimalPresentation p G) :
    minimalRelationRank p G hG = h2Rank p G

Module documentation

Minimal relation rank and degree-two continuous cohomology

Declarations

h2Rank

h2Rank_eq_finrank

minimalRelationRank_eq_h2Rank