ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet.isFreeProCGroup_of_finite
A finite discrete converging-set basis gives the usual free pro-\(C\) universal property for a concrete finite-group class.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ProCGroups.FreeProC
universe u v w
namespace IsEpimorphicallyFreeProCGroupOnConvergingSetLean source · statement
theorem isFreeProCGroup_of_finite
(C : ProCGroups.FiniteGroupClass.{u})
[hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
[hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
[CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
{ι : X → F}
(hι :
IsEpimorphicallyFreeProCGroupOnConvergingSet
(C := C) X F ι) :
IsFreeProCGroup (C := C) ι