Module

FiniteGolodShafarevichH2.lean

Nyll.GaloisCohomology.ProP.FiniteGolodShafarevichH2

1 declaration indexed from sourceView source ↗

Module documentation

Finite Golod--Shafarevich bound in terms of H²

For a finite nontrivial pro-p group, finite cochains supply finite-dimensional H² and the constructed finite minimal presentation identifies its relation rank with that dimension. Thus no presentation or finite-presentation hypothesis is required in the numerical bound.

Imports16

Nyll.GaloisCohomology.ProP.FinitePresentationExistence
Nyll.GaloisCohomology.ProP.H2FiniteStageFamily
Nyll.GaloisCohomology.ProP.RelationRankH2
Nyll.GaloisCohomology.ProP.TrivialZModP
Nyll.ProCGroups.FiniteGeneration.Basic
Nyll.ProCGroups.GolodShafarevich.FiniteCriterion
Nyll.ProCGroups.ProC.InverseLimits.Predicates
Nyll.ProCGroups.ProP.GeneratorRank
Nyll.ProCGroups.ProP.Presentation.RelationCardinal
Mathlib.Algebra.Field.ZMod
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.Topology.Algebra.Group.Basic
Mathlib.Topology.Compactness.Compact
Mathlib.Topology.Connected.TotallyDisconnected
Mathlib.Topology.Separation.Basic
Mathlib.Topology.Separation.Hausdorff

Imported by1

Nyll.GaloisCohomology.ProP.All

theorem

finite_sq_generatorRank_lt_four_mul_finrank_h2

L40 ↗

ClassFieldTower.ProP.finite_sq_generatorRank_lt_four_mul_finrank_h2

Documentation

A finite nontrivial pro-p group satisfies the strict Golod--Shafarevich inequality with its actual degree-two continuous cohomology dimension.

Source context 3 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.FiniteGeneration ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem finite_sq_generatorRank_lt_four_mul_finrank_h2
    (p : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [T2Space G] [Finite G] [Nontrivial G]
    (hG : ProC.HasPGroupOpenNormalBasis p G) :
    topologicalGeneratorRank G ^ 2 < 4 * Module.finrank (ZMod p)
      (continuousCohomologyZModPLifted p G 2)

Module documentation

Finite Golod--Shafarevich bound in terms of H²

Declarations

finite_sq_generatorRank_lt_four_mul_finrank_h2