Yamaguchi Lean 4 Library
ProCGroups/FreeProC/Characterization/EmbeddingProblems.lean
ProCGroups/FreeProC/Characterization/EmbeddingProblems/Source

ProCGroups/FreeProC/Characterization/EmbeddingProblems.lean

1import ProCGroups.FreeProC.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeProC/Characterization/EmbeddingProblems.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-/
17namespace ProCGroups.FreeProC.Characterization
19open ProCGroups.FreeProC
21universe u
23section EmbeddingProblems
25/-- A subgroup is minimal normal if it is nontrivial, normal, and has no proper nontrivial
26normal subgroup below it. -/
28 {A : Type u} [Group A] (N : Subgroup A) : Prop :=
29 N.Normal ∧ N ≠ ⊥ ∧
30 ∀ M : Subgroup A, M.Normal → M ≤ N → M = ⊥ ∨ M = N
32/-- A topological embedding problem for a topological group.
34No finiteness or pro-`C` condition is built into this structure; those are supplied by
37 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
38 A : Type u
39 instGroupA : Group A
40 instTopologicalSpaceA : TopologicalSpace A
41 instIsTopologicalGroupA : IsTopologicalGroup A
42 B : Type u
43 instGroupB : Group B
44 instTopologicalSpaceB : TopologicalSpace B
45 instIsTopologicalGroupB : IsTopologicalGroup B
46 α : A →* B
47 continuous_α : Continuous α
48 surjective_α : Function.Surjective α
49 φ : G →* B
50 continuous_φ : Continuous φ
51 surjective_φ : Function.Surjective φ
53attribute [instance] TopologicalEmbeddingProblem.instGroupA
54attribute [instance] TopologicalEmbeddingProblem.instTopologicalSpaceA
55attribute [instance] TopologicalEmbeddingProblem.instIsTopologicalGroupA
56attribute [instance] TopologicalEmbeddingProblem.instGroupB
57attribute [instance] TopologicalEmbeddingProblem.instTopologicalSpaceB
58attribute [instance] TopologicalEmbeddingProblem.instIsTopologicalGroupB
60/-- A topological embedding problem whose two finite target groups are finite. -/
62 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
64 finiteA : Finite A
65 finiteB : Finite B
67/-- A topological embedding problem whose two finite target groups lie in the chosen pro-`C`
68predicate. -/
70 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
71 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
73 isProCA : @ProCGroups.ProC.ProCGroupPredicate.holds ProC A _ _ _
74 isProCB : @ProCGroups.ProC.ProCGroupPredicate.holds ProC B _ _ _
78variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
80/-- The kernel of an embedding problem. -/
81def kernel (P : TopologicalEmbeddingProblem G) : Subgroup P.A :=
82 P.α.ker
84/-- A weak solution is a continuous lift commuting with the embedding-problem square. -/
86 { φbar : G →* P.A // Continuous φbar ∧ P.α.comp φbar = P.φ }
88/-- A proper solution is a surjective weak solution. -/
90 { φbar : WeakSolution P // Function.Surjective φbar.1 }
92/-- Weak solvability of an embedding problem. -/
94 ∃ φbar : G →* P.A, Continuous φbar ∧ P.α.comp φbar = P.φ
96/-- Solvability of an embedding problem. -/
98 ∃ φbar : G →* P.A,
99 Continuous φbar ∧ Function.Surjective φbar ∧ P.α.comp φbar = P.φ
101/-- The finite minimal normal kernel condition. -/
103 Finite P.kernel ∧ IsMinimalNormalSubgroup P.kernel
105/-- The embedding problem is split: its epimorphism has a continuous section. -/
107 ∃ σ : P.B →* P.A, Continuous σ ∧ P.α.comp σ = MonoidHom.id P.B
109/-- An embedding problem has at least `κ` different solutions if there is a family of pairwise
110distinct continuous surjective lifts indexed by a set of cardinality `κ`. -/
112 (P : TopologicalEmbeddingProblem G) (κ : Cardinal) : Prop :=
113 ∃ I : Type u, Cardinal.mk I = κ ∧
114 ∃ ψ : I → P.ProperSolution, Function.Injective ψ
118/-- A global class of embedding problems, varying with the ambient source group. -/
120 {G : Type u} → [Group G] → [TopologicalSpace G] → [IsTopologicalGroup G] →
123/-- An embedding problem whose source and target both lie in the chosen pro-`C` class. -/
125 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
126 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
128 @ProCGroups.ProC.ProCGroupPredicate.holds ProC P.A _ _ _ ∧
129 @ProCGroups.ProC.ProCGroupPredicate.holds ProC P.B _ _ _
131/-- A finite embedding problem whose two finite target groups lie in the chosen finite class. -/
133 (C : ProCGroups.FiniteGroupClass.{u})
134 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
136 Finite P.A ∧ Finite P.B ∧
137 ProCGroups.ProC.IsProCGroup C P.A ∧ ProCGroups.ProC.IsProCGroup C P.B
139/-- A finite `C`-embedding problem with a continuous section. -/
141 (C : ProCGroups.FiniteGroupClass.{u})
142 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
144 IsFiniteCEmbeddingProblem C P ∧ P.IsSplit
146/-- Weak lifting property over a class of embedding problems. -/
148 (E : EmbeddingProblemPredicate.{u})
149 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
150 ∀ P : TopologicalEmbeddingProblem G, E P → P.HasWeakSolution
152/-- Strong lifting property over a class of embedding problems, with the ambient cardinal bound
153exposed explicitly. -/
155 (E : EmbeddingProblemPredicate.{u})
156 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
157 (κ : Cardinal) : Prop :=
158 ∀ P : TopologicalEmbeddingProblem G, E P →
159 Generation.topologicalRank P.B < κ →
160 Generation.topologicalRank P.A ≤ κ →
161 P.HasSolution
163end EmbeddingProblems
165end ProCGroups.FreeProC.Characterization