Module

FiniteCriterion.lean

Nyll.ProCGroups.GolodShafarevich.FiniteCriterion

4 declarations indexed from sourceView source ↗

Module documentation

Finite Golod--Shafarevich bound

The truncated Fox inequality and its numerical criterion imply the classical strict bound d² < 4r for a finite nontrivial pro-p group. The result is first stated for a concrete minimal presentation and then for the canonical minimal relation rank. Its contrapositive is the reusable infinitude criterion.

Imports5

Imported by3

theorem

displayedGeneratorCard_pos

L45 ↗

ClassFieldTower.ProP.FiniteProPPresentation.displayedGeneratorCard_pos

Documentation

A minimal presentation of a nontrivial target has a positive displayed generator count.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Generation
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem displayedGeneratorCard_pos
    [Nontrivial G]
    (P : FiniteProPPresentation p d r sourceData G)
    (hP : P.IsMinimal) :
    0 < d

theorem

finite_sq_generatorCard_lt_four_mul_relationCard

L58 ↗

ClassFieldTower.ProP.FiniteProPPresentation.finite_sq_generatorCard_lt_four_mul_relationCard

Documentation

The strict Golod--Shafarevich bound for one concrete finite minimal presentation.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Generation
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem finite_sq_generatorCard_lt_four_mul_relationCard
    [Finite G] [Nontrivial G]
    (P : FiniteProPPresentation p d r sourceData G)
    (hP : P.IsMinimal) :
    d ^ 2 < 4 * r

theorem

finite_sq_generatorRank_lt_four_mul_relationRank

L89 ↗

ClassFieldTower.ProP.finite_sq_generatorRank_lt_four_mul_relationRank

Documentation

A finite nontrivial pro-p group with a finite minimal presentation satisfies the strict generator/relation-rank bound.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Generation
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 finite_sq_generatorRank_lt_four_mul_relationRank
    [Finite G] [Nontrivial G]
    (hG : HasFiniteMinimalPresentation p G) :
    topologicalGeneratorRank G ^ 2 < 4 * minimalRelationRank p G hG

theorem

infinite_of_four_mul_relationRank_le_generatorRank_sq

L100 ↗

ClassFieldTower.ProP.infinite_of_four_mul_relationRank_le_generatorRank_sq

Documentation

If the generator square reaches four times the minimal relation rank, the pro-p group is infinite.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Generation
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 infinite_of_four_mul_relationRank_le_generatorRank_sq
    [Nontrivial G]
    (hG : HasFiniteMinimalPresentation p G)
    (hineq : 4 * minimalRelationRank p G hG ≤
      topologicalGeneratorRank G ^ 2) :
    Infinite G

Module documentation

Finite Golod--Shafarevich bound

Declarations

displayedGeneratorCard_pos

finite_sq_generatorCard_lt_four_mul_relationCard

finite_sq_generatorRank_lt_four_mul_relationRank

infinite_of_four_mul_relationRank_le_generatorRank_sq