Continuous lifts from compatible finite-level solutions

A compatible family of LevelSolutions determines a continuous lift into the profinite group A, with precisely the supplied quotient maps. This assembly requires no finite generation or finite embedding-problem solvability assumption; HasPGroupSolutions supplies such a family in TauCeti.HasPGroupSolutions.exists_compatible_levelSolutions.

theorem TauCeti.exists_continuous_lift_of_compatible_levelSolutions {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) (β : (U : OpenNormalSubgroup A) → LevelSolution α hα f U) (hβ : ∀ ⦃V U : OpenNormalSubgroup A⦄ (hVU : V ≤ U), levelSolutionMap α hα f hVU (β V) = β U) : ∃ (φ : G →ₜ* A), α.comp φ = f ∧ ∀ (U : OpenNormalSubgroup A), (QuotientGroup.mk' ↑U.toOpenSubgroup).comp φ.toMonoidHom = (↑(β U)).toMonoidHom

Assemble a compatible family of finite-level solutions into a continuous lift, retaining its prescribed value in every open-normal quotient.