Lifting and finiteness for finite embedding problems

The finite groups in an embedding problem can be moved to the universe of its source. Consequently HasPGroupSolutions lifts open-kernel maps through finite surjections in arbitrary universes. Finiteness of the solution set additionally follows from topological finite generation of the source.

theorem TauCeti.HasPGroupSolutions.exists_isSolution {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : HasPGroupSolutions p G) (P : FiniteEmbeddingProblem G) (hP : IsPGroup p ↥P.α.ker) : ∃ (β : G →* P.E), P.IsSolution β

Solvability with p-group kernel applies to finite target groups in any universe.

theorem TauCeti.HasPGroupSolutions.exists_comp_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : HasPGroupSolutions p G) {E : Type v} [Group E] [Finite E] {F : Type w} [Group F] (φ : E →* F) (hφ : Function.Surjective ⇑φ) (hker : IsPGroup p ↥φ.ker) (β : G →* F) (hβ : IsOpen ↑β.ker) : ∃ (β' : G →* E), IsOpen ↑β'.ker ∧ φ.comp β' = β

An open-kernel map lifts through a finite surjection whose kernel is a p-group.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_isSolution {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsTopologicallyFinitelyGenerated G) (P : FiniteEmbeddingProblem G) : Finite { β : G →* P.E // P.IsSolution β }

A finite embedding problem for a topologically finitely generated group has finitely many solutions.