Module

GeneratorRank.lean

Nyll.ProCGroups.ProP.Presentation.GeneratorRank

5 declarations indexed from sourceView source ↗

Module documentation

Generator rank of a minimal pro-p presentation

The displayed free basis gives the upper rank bound. Minimality supplies a surjection from the target to the source Frattini quotient, and the Burnside basis theorem lifts a small generating set back to the free source, giving the reverse bound.

Imports2

Imported by4

instance

(anonymous instance)

L41 ↗

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.FiniteGeneration
open ProCGroups.Generation
open ProCGroups.Presentations
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

instance : (closedPowerCommutator p sourceData.carrier).Normal

theorem

target_topologicallyGeneratedByAtMost

L46 ↗

ClassFieldTower.ProP.FiniteProPPresentation.target_topologicallyGeneratedByAtMost

Documentation

The displayed free basis gives an at-most-d generating family of the target.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.FiniteGeneration
open ProCGroups.Generation
open ProCGroups.Presentations
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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier

Lean source · statement

theorem target_topologicallyGeneratedByAtMost
    (P : FiniteProPPresentation p d r sourceData G) :
    TopologicallyGeneratedByAtMost (G := G) d

theorem

source_topologicalRank_eq_nat

L65 ↗

ClassFieldTower.ProP.FiniteProPPresentation.source_topologicalRank_eq_nat

Documentation

The free source has the displayed generator rank.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.FiniteGeneration
open ProCGroups.Generation
open ProCGroups.Presentations
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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier

Lean source · statement

theorem source_topologicalRank_eq_nat
    (P : FiniteProPPresentation p d r sourceData G) :
    topologicalRank sourceData.carrier = d

theorem

target_topologicalRank_eq_nat

L90 ↗

ClassFieldTower.ProP.FiniteProPPresentation.target_topologicalRank_eq_nat

Documentation

Minimality forces the target generator rank to equal the displayed free rank.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.FiniteGeneration
open ProCGroups.Generation
open ProCGroups.Presentations
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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier

Lean source · statement

theorem target_topologicalRank_eq_nat
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal) :
    topologicalRank G = d

theorem

target_topologicalGeneratorRank_eq

L139 ↗

ClassFieldTower.ProP.FiniteProPPresentation.target_topologicalGeneratorRank_eq

Documentation

Natural-valued generator-rank form of target_topologicalRank_eq_nat.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.FiniteGeneration
open ProCGroups.Generation
open ProCGroups.Presentations
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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier

Lean source · statement

theorem target_topologicalGeneratorRank_eq
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal) :
    topologicalGeneratorRank G = d

Module documentation

Generator rank of a minimal pro-p presentation

Declarations

(anonymous instance)

target_topologicallyGeneratedByAtMost

source_topologicalRank_eq_nat

target_topologicalRank_eq_nat

target_topologicalGeneratorRank_eq