Golod–Shafarevich inequality

DefinitionGenerator rank#✓fully proved

For a topological group \(G\), the generator rank \(d(G)\) is the least natural number \(k\) such that some finite subset of \(G\) with \(k\) elements generates a dense subgroup of \(G\), that is, a subgroup whose closure is all of \(G\). If no finite subset of \(G\) generates a dense subgroup, then \(d(G)\) is defined to be \(0\). For a finite discrete group this is the ordinary minimal number of generators.

noncomputable def generatorRank
    (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ :=
  sInf {k : ℕ | ∃ S : Finset G, S.card = k ∧
    (Subgroup.closure (S : Set G)).topologicalClosure = ⊤}

Used by 1

Used byGolod–Shafarevich inequality

DefinitionTrivial representation on \(\mathbb{Z}/p\mathbb{Z}\)#✓fully proved

For a natural number \(p\) and a topological group \(G\), this is \(\mathbb{Z}/p\mathbb{Z}\), with its discrete topology, regarded as a continuous representation of \(G\) over \(\mathbb{Z}/p\mathbb{Z}\) on which every element of \(G\) acts as the identity.

noncomputable def trivialZModpRep
    (p : ℕ) (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    TopRep (ZMod p) G :=
  TopRep.of (ContRepresentation.trivial (ZMod p) G (ZMod p))

Used by 1

Used byRelation rank

DefinitionRelation rank#✓fully proved

For a prime \(p\) and a topological group \(G\), the relation rank \(r(G)\) is the dimension over \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\) of the continuous cohomology group \(H^2(G, \mathbb{F}_p)\), where \(G\) acts trivially on \(\mathbb{F}_p\). If this space is infinite-dimensional, then \(r(G)\) is defined to be \(0\).

noncomputable def relationRank
    (p : ℕ) [Fact p.Prime] (G : Type)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ :=
  Module.finrank (ZMod p)
    (continuousCohomology 2 (trivialZModpRep p G))

Uses 1 · Used by 1

Statement usesTrivial representation on \(\mathbb{Z}/p\mathbb{Z}\)

Used byGolod–Shafarevich inequality

TheoremGolod–Shafarevich inequality#●ready to prove

Let \(p\) be a prime and let \(Q\) be a nontrivial finite \(p\)-group, viewed as a topological group with the discrete topology. Then the generator rank \(d(Q)\) and the relation rank \(r(Q)\), the dimension over \(\mathbb{F}_p\) of the continuous cohomology group \(H^2(Q, \mathbb{F}_p)\) with trivial coefficients, satisfy \(d(Q)^2 < 4\, r(Q)\).

public theorem_wanted golod_shafarevich_inequality
    (p : ℕ) [Fact p.Prime] (Q : Type)
    [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    [DiscreteTopology Q] [Finite Q] :
    IsPGroup p Q → Nontrivial Q →
      (generatorRank Q : ℝ) ^ 2 < 4 * (relationRank p Q : ℝ)

Sources

• NSW (J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Grundlehren 323, Springer 2008), Theorem 3.9.7; J.-P. Serre, Galois Cohomology, Chapter I, Appendix 2, Theorem 1. Lean hypothesis: https://github.com/logical-intelligence/erdos-unit-distance (Hyp_GolodShafarevichInequality). Problem golod_shafarevich_inequality of the lean-eval benchmark.

Uses 2

Statement usesGenerator rank · Relation rank

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.