Source: ProCGroups.FreeProC.FinitelyGenerated

1import ProCGroups.FreeProC.Basic

3/-!

4# Pro C Groups / Free pro-C / Finitely Generated

6This module turns a finite discrete converging-set basis into the usual

7free pro-C universal property.

8-/

10open scoped Topology

12namespace ProCGroups.FreeProC

14universe u v w

16namespace IsEpimorphicallyFreeProCGroupOnConvergingSet

18/--

19A finite discrete converging-set basis gives the usual free pro-\(C\) universal property for a

20concrete finite-group class.

22theorem isFreeProCGroup_of_finite

23 (C : ProCGroups.FiniteGroupClass.{u})

26 {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X]

27 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

28 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]

29 {ι : X → F}

30 (hι :

31 IsEpimorphicallyFreeProCGroupOnConvergingSet

32 (C := C) X F ι) :

33 IsFreeProCGroup (C := C) ι := by

34 refine

35 { hasOpenNormalBasisInClass := hι.hasOpenNormalBasisInClass

36 continuous_ι := continuous_of_discreteTopology

37 generates_range := hι.generates_range

38 existsUnique_lift := ?_ }

39 intro G _ _ _ _ _ _ hG φ _hφ

40 rcases hι.existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass C

41 hIso.out hVar.out.subgroupClosed hG φ

42 (FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := G) φ) with

43 ⟨f, hf, huniq⟩

44 refine ⟨f.toMonoidHom, ⟨f.continuous, hf⟩, ?_⟩

45 intro g hg

46 let gc : F →ₜ* G := { toMonoidHom := g, continuous_toFun := hg.1 }

47 exact congrArg ContinuousMonoidHom.toMonoidHom (huniq gc hg.2)

49end IsEpimorphicallyFreeProCGroupOnConvergingSet

54end ProCGroups.FreeProC