Transition maps between finite solutions

Solutions at a finer quotient restrict to solutions at a coarser quotient. If G solves finite embedding problems with p-group kernel, every coarse solution has a fine lift. This statement does not require finite generation of G; finiteness of the solution sets is a separate hypothesis for a subsequent compactness argument.

theorem TauCeti.levelImage_mono {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (α : A →ₜ* B) (hα : Function.Surjective ⇑α) : Monotone (levelImage α hα)

The image of an open normal subgroup under α is monotone in the subgroup.

def TauCeti.levelSolutionMap {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) {V U : OpenNormalSubgroup A} (hVU : V ≤ U) (β : LevelSolution α hα f V) : LevelSolution α hα f U

Restrict a solution at V to the coarser quotient at U.

Equations

• TauCeti.levelSolutionMap α hα f hVU β = ⟨{ toMonoidHom := TauCeti.QuotientGroup.mapOfLE hVU, continuous_toFun := ⋯ }.comp ↑β, ⋯⟩

@[simp]

theorem TauCeti.levelSolutionMap_apply {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) {V U : OpenNormalSubgroup A} (hVU : V ≤ U) (β : LevelSolution α hα f V) (g : G) : ↑(levelSolutionMap α hα f hVU β) g = (QuotientGroup.mapOfLE hVU) (↑β g)

@[simp]

theorem TauCeti.levelSolutionMap_refl {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace 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) : levelSolutionMap α hα f ⋯ β = β

@[simp]

theorem TauCeti.levelSolutionMap_comp {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) {W V U : OpenNormalSubgroup A} (hWV : W ≤ V) (hVU : V ≤ U) (β : LevelSolution α hα f W) : levelSolutionMap α hα f hVU (levelSolutionMap α hα f hWV β) = levelSolutionMap α hα f ⋯ β

instance TauCeti.instDirectedSystemOpenNormalSubgroupLevelSolutionLevelSolutionMap {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) : DirectedSystem (LevelSolution α hα f) fun (x x_1 : OpenNormalSubgroup A) (h : x ≤ x_1) => levelSolutionMap α hα f h

theorem TauCeti.levelSolutionMap_surjective {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] [IsTopologicalGroup G] {p : ℕ} (hG : HasPGroupSolutions p G) (hA : IsProP p A) (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) {V U : OpenNormalSubgroup A} (hVU : V ≤ U) : Function.Surjective (levelSolutionMap α hα f hVU)

Every solution at a coarse level extends to a solution at any finer level.