Source: ProCGroups.FreeProC.Characterization.EmbeddingProblems
1import ProCGroups.FreeProC.Basic
2import ProCGroups.TopologicalGroups
4/-!
5# Pro C Groups / Free pro-C / Characterization / Embedding Problems
7This module defines topological embedding problems, their weak and proper
8solutions, and the finite split lifting properties used in freeness criteria.
9-/
11namespace ProCGroups.FreeProC.Characterization
13open ProCGroups.FreeProC
15universe u
17section EmbeddingProblems
19/-- A topological embedding problem for a topological group. Finiteness and finite-class
20conditions are expressed by the predicates below instead of parallel wrapper structures. -/
21structure TopologicalEmbeddingProblem
22 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
23 /-- The covering topological group through which a solution must lift. -/
24 A : TopGrp.{u}
25 /-- The common target of the embedding-problem epimorphism and the prescribed map from `G`. -/
26 B : TopGrp.{u}
27 /-- The continuous homomorphism from the covering group `A` onto `B`. -/
28 α : A →ₜ* B
29 /-- The covering homomorphism `α` is surjective. -/
30 surjective_α : Function.Surjective α
31 /-- The prescribed continuous homomorphism from `G` to the target group `B`. -/
32 φ : G →ₜ* B
33 /-- The prescribed map `φ` is surjective, so the embedding problem is epimorphic on both legs. -/
34 surjective_φ : Function.Surjective φ
36namespace TopologicalEmbeddingProblem
38variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
40/-- A proper solution is a surjective weak solution. -/
41def ProperSolution (P : TopologicalEmbeddingProblem G) : Type u :=
42 { φbar : G →ₜ* P.A //
43 Function.Surjective φbar ∧ P.α.comp φbar = P.φ }
45/-- The embedding problem is split: its epimorphism has a continuous section. -/
46def IsSplit (P : TopologicalEmbeddingProblem G) : Prop :=
47 ∃ σ : P.B →ₜ* P.A, P.α.comp σ = ContinuousMonoidHom.id P.B
49/--
50An embedding problem has at least \(\kappa\) different solutions if there is a family of
51pairwise distinct continuous surjective lifts indexed by a set of cardinality \(\kappa\).
52-/
53def HasAtLeastProperSolutions
54 (P : TopologicalEmbeddingProblem G) (κ : Cardinal) : Prop :=
55 ∃ I : Type u, Cardinal.mk I = κ ∧
56 ∃ ψ : I → P.ProperSolution, Function.Injective ψ
58end TopologicalEmbeddingProblem
60/-- A finite embedding problem whose two finite target groups lie in the chosen finite class. -/
61def IsFiniteCEmbeddingProblem
62 (C : ProCGroups.FiniteGroupClass.{u})
63 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
64 (P : TopologicalEmbeddingProblem G) : Prop :=
65 Finite P.A ∧ DiscreteTopology P.A ∧ C P.A ∧
66 Finite P.B ∧ DiscreteTopology P.B ∧ C P.B
68/-- A finite \(C\)-embedding problem with a continuous section. -/
69def IsFiniteSplitCEmbeddingProblem
70 (C : ProCGroups.FiniteGroupClass.{u})
71 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
72 (P : TopologicalEmbeddingProblem G) : Prop :=
73 IsFiniteCEmbeddingProblem C P ∧ P.IsSplit
75end EmbeddingProblems
77end ProCGroups.FreeProC.Characterization