Source: ProCGroups.FreeProC.Characterization.Quasifree
1import ProCGroups.FreeProC.Characterization.EmbeddingProblems
3/-!
4# Pro C Groups / Free pro-C / Characterization / Quasifree
6This module formulates quasifree proper-solution growth and its cardinal
7monotonicity consequences.
8-/
10noncomputable section
12open scoped Cardinal
14namespace ProCGroups.FreeProC.Characterization
16universe u
18/-- A topological group has a topological generating set of cardinality \(\kappa\). -/
19def HasTopologicalGeneratingSetOfCardinality
20 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
21 (κ : Cardinal) : Prop :=
22 ∃ S : Set G, Generation.TopologicallyGenerates (G := G) S ∧ Cardinal.mk S = κ
24/--
25A group has the quasifree proper-solution property at rank \(\kappa\) for finite split
26\(C\)-embedding problems.
27-/
28def HasQuasifreeProperSolutionProperty
29 (C : ProCGroups.FiniteGroupClass.{u})
30 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31 (κ : Cardinal) : Prop :=
32 ∀ P : TopologicalEmbeddingProblem G,
33 IsFiniteSplitCEmbeddingProblem C P → P.HasAtLeastProperSolutions κ
35/--
36Quasifreeness at infinite rank \(\kappa\). The rank field is deliberately topological: in
37profinite contexts an abstract generating set is too weak and does not control the closed
38subgroup generated by the chosen family. The lifting field records the standard proper-solution
39condition for finite split embedding problems.
40-/
41def IsQuasifreeOfRank (C : ProCGroups.FiniteGroupClass.{u})
42 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
43 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
44 (κ : Cardinal) : Prop :=
46 HasTopologicalGeneratingSetOfCardinality G κ ∧
47 Cardinal.aleph0 ≤ κ ∧
48 HasQuasifreeProperSolutionProperty C G κ
50end ProCGroups.FreeProC.Characterization