ProCGroups/FreeProC/Characterization/FreenessAndLifting.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/FreenessAndLifting.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
19universe u
21section CoreTheorems
23variable {E : EmbeddingProblemPredicate.{u}}
25/-- Weak solvability reduces to the finite minimal normal kernel case when the reduction step is
26supplied explicitly. -/
28 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29 (hfinite :
30 ∀ P : TopologicalEmbeddingProblem G, E P →
31 P.HasFiniteMinimalNormalKernel → P.HasWeakSolution)
32 (hreduce :
33 ∀ P : TopologicalEmbeddingProblem G, E P →
34 ∃ P₀ : TopologicalEmbeddingProblem G, E P₀ ∧
35 P₀.HasFiniteMinimalNormalKernel ∧
36 (P₀.HasWeakSolution → P.HasWeakSolution)) :
37 ∀ P : TopologicalEmbeddingProblem G, E P → P.HasWeakSolution := by
38 intro P hP
39 rcases hreduce P hP with ⟨P₀, hP₀, hker, hback⟩
40 exact hback (hfinite P₀ hP₀ hker)
42end CoreTheorems
45/-- Weak lifting can be tested on finite-target embedding problems, with explicit reduction data
48 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
49 {E : EmbeddingProblemPredicate.{u}}
50 (hreduce :
51 ∀ P : TopologicalEmbeddingProblem G, E P →
52 ∃ P₀ : TopologicalEmbeddingProblem G, E P₀ ∧
53 P₀.HasFiniteMinimalNormalKernel ∧
54 (P₀.HasWeakSolution → P.HasWeakSolution))
55 (hfiniteTargetOfFiniteMinimalKernel :
56 ∀ P : TopologicalEmbeddingProblem G, E P →
57 P.HasFiniteMinimalNormalKernel → Finite P.A) :
58 HasWeakLiftingPropertyOver E G ↔
59 ∀ P : TopologicalEmbeddingProblem G, E P → Finite P.A → P.HasWeakSolution := by
60 constructor
61 · intro h P hP _hfinite
62 exact h P hP
63 · intro h P hP
64 rcases hreduce P hP with ⟨P₀, hP₀, hmin, hback⟩
65 exact hback (h P₀ hP₀ (hfiniteTargetOfFiniteMinimalKernel P₀ hP₀ hmin))
68end ProCGroups.FreeProC.Characterization