ProCGroups/Generation/GeneratingFamilies.lean
1import ProCGroups.FreeProC.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Generation/GeneratingFamilies.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Topological generation
14Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.
15-/
17open scoped Cardinal
19namespace ProCGroups.Generation
21universe u
23/-- An indexed topological generating family converging to `1`.
25This is deliberately weaker than a free pro-`C` basis: it records only generation and convergence
26of the image. -/
27structure TopologicalGeneratingFamily
28 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
29 index : Type u
30 toFun : index → G
31 convergesToOne : _root_.ProCGroups.FreeProC.FamilyConvergesToOne (G := G) toFun
32 generates : TopologicallyGenerates (G := G) (Set.range toFun)
34namespace TopologicalGeneratingFamily
36variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38instance instCoeFunTopologicalGeneratingFamily :
39 CoeFun (TopologicalGeneratingFamily G) (fun family => family.index → G) where
40 coe family := family.toFun
42@[simp] theorem toFun_eq_coe (family : TopologicalGeneratingFamily G) :
43 family.toFun = (family : family.index → G) := rfl
45/-- The cardinality of the indexing type. -/
46def cardinal (family : TopologicalGeneratingFamily G) : Cardinal :=
47 Cardinal.mk family.index
51end ProCGroups.Generation