ClassFieldTower.ProP.hasFiniteMinimalPresentation_of_finiteDimensional_h2
Finite generation and finite-dimensional H² supply an actual finite minimal pro-p presentation, including the free source, quotient map, and finite relator family.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.FreeProC ProCGroups.Generation ProCGroups.FiniteGeneration
open ProCGroups.Presentations ClassFieldTower.Cohomology
noncomputable section
universe uLean source · statement
theorem hasFiniteMinimalPresentation_of_finiteDimensional_h2
{p : ℕ} [Fact p.Prime]
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hG : ProC.HasPGroupOpenNormalBasis p G)
(hfg : TopologicallyFinitelyGenerated G)
[FiniteDimensional (ZMod p) (continuousCohomologyZModPLifted p G 2)] :
HasFiniteMinimalPresentation p G