ProCGroups/FreeProC/Characterization/Quasifree.lean
1import ProCGroups.FreeProC.Characterization.EmbeddingProblems
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeProC/Characterization/Quasifree.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C groups
14Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
15-/
17noncomputable section
19open scoped Cardinal
21namespace ProCGroups.FreeProC.Characterization
23universe u
25/-- An abstract group has a generating set of cardinality `κ`. This is not the right rank
26condition for quasifree profinite groups; use
27`HasTopologicalGeneratingSetOfCardinality` there. -/
28def HasGeneratingSetOfCardinality (G : Type u) [Group G] (κ : Cardinal) : Prop :=
29 ∃ S : Set G, Subgroup.closure S = ⊤ ∧ Cardinal.mk S = κ
31/-- A topological group has a topological generating set of cardinality `κ`. -/
33 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34 (κ : Cardinal) : Prop :=
35 ∃ S : Set G, Generation.TopologicallyGenerates (G := G) S ∧ Cardinal.mk S = κ
37/-- A pro-`C` group is projective for finite `C`-embedding problems, stated as the concrete
39def IsProjectiveProCGroup (C : ProCGroups.FiniteGroupClass.{u})
40 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
41 ProCGroups.ProC.IsProCGroup C G ∧
42 ∀ {A B : Type u} [Group A] [Group B]
43 [TopologicalSpace A] [TopologicalSpace B]
44 [IsTopologicalGroup A] [IsTopologicalGroup B],
45 ProCGroups.ProC.IsProCGroup C A → ProCGroups.ProC.IsProCGroup C B →
47 ∃ lift : G →ₜ* A, π.comp lift = φ
49/-- A group has the quasifree proper-solution property at rank `κ` for finite split
50`C`-embedding problems. -/
52 (C : ProCGroups.FiniteGroupClass.{u})
53 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
54 (κ : Cardinal) : Prop :=
55 ∀ P : TopologicalEmbeddingProblem G,
56 IsFiniteSplitCEmbeddingProblem C P → P.HasAtLeastProperSolutions κ
58/-- Quasifreeness at infinite rank `κ`.
60The rank field is deliberately topological: in profinite contexts an abstract generating set is
61too weak and does not control the closed subgroup generated by the chosen family. The lifting
63def IsQuasifreeOfRank (C : ProCGroups.FiniteGroupClass.{u})
64 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
65 (κ : Cardinal) : Prop :=
66 ProCGroups.ProC.IsProCGroup C G ∧
68 Cardinal.aleph0 ≤ κ ∧
71end ProCGroups.FreeProC.Characterization