ClassFieldTower.ProP.FiniteProPPresentation.source_topologicallyFinitelyGenerated
The free source of any displayed finite presentation is topologically finitely generated by its actual finite free basis.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP.FiniteProPPresentation
open ProCGroups ProCGroups.FiniteGeneration
universe uLean source · statement
theorem source_topologicallyFinitelyGenerated
{p d r : ℕ} [Fact p.Prime]
{sourceData : FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
(FiniteGroupClass.pGroup p)}
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(P : FiniteProPPresentation p d r sourceData G) :
TopologicallyFinitelyGenerated sourceData.carrier