Finite levels of a lifting problem

For a continuous surjection α : A → B, an open normal subgroup U of A gives the quotient map A/U → B/α(U). The map induced by f : G → B need not be surjective. Accordingly levelProblem restricts the quotient map to the preimage of that map's range.

LevelSolution records the equivalent lift into A/U. Solvability follows from HasPGroupSolutions, and topological finite generation of G makes each level's solution set finite.

def TauCeti.levelImage {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 ⇑α) (U : OpenNormalSubgroup A) : OpenNormalSubgroup B

The image of an open normal subgroup under a continuous surjection from a compact group.

Equations

• TauCeti.levelImage α hα U = { toSubgroup := Subgroup.map α.toMonoidHom ↑U.toOpenSubgroup, isOpen' := ⋯, isNormal' := ⋯ }

@[simp]

theorem TauCeti.levelImage_toSubgroup {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 ⇑α) (U : OpenNormalSubgroup A) : ↑(levelImage α hα U).toOpenSubgroup = Subgroup.map α.toMonoidHom ↑U.toOpenSubgroup

def TauCeti.levelMap {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 ⇑α) (U : OpenNormalSubgroup A) : A ⧸ ↑U.toOpenSubgroup →* B ⧸ ↑(levelImage α hα U).toOpenSubgroup

The finite quotient map induced by α at U.

Equations

• TauCeti.levelMap α hα U = QuotientGroup.map (↑U.toOpenSubgroup) (↑(TauCeti.levelImage α hα U).toOpenSubgroup) α.toMonoidHom ⋯

@[simp]

theorem TauCeti.levelMap_mk {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 ⇑α) (U : OpenNormalSubgroup A) (a : A) : (levelMap α hα U) ↑a = ↑(α a)

theorem TauCeti.levelMap_surjective {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 ⇑α) (U : OpenNormalSubgroup A) : Function.Surjective ⇑(levelMap α hα U)

The finite quotient map induced by a surjection is surjective.

@[reducible, inline]

abbrev TauCeti.levelProblem {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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) : FiniteEmbeddingProblem G

The finite embedding problem obtained by restricting to the image of G in B/α(U).

Equations

• TauCeti.levelProblem α hα f U = TauCeti.FiniteEmbeddingProblem.ofSurjective (TauCeti.levelMap α hα U) ⋯ ((QuotientGroup.mk' ↑(TauCeti.levelImage α hα U).toOpenSubgroup).comp f.toMonoidHom) ⋯

@[reducible, inline]

abbrev TauCeti.LevelSolution {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) : Type (max 0 u v)

A continuous lift of f at the finite quotient A/U.

Equations

• TauCeti.LevelSolution α hα f U = { β : G →ₜ* A ⧸ ↑U.toOpenSubgroup // ∀ (g : G), (TauCeti.levelMap α hα U) (β g) = (QuotientGroup.mk' ↑(TauCeti.levelImage α hα U).toOpenSubgroup) (f g) }

def TauCeti.levelSolutionEquiv {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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) : { β : G →* (levelProblem α hα f U).E // (levelProblem α hα f U).IsSolution β } ≃ LevelSolution α hα f U

Range restriction identifies solutions of the embedding problem with lifts into A/U.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.levelSolutionEquiv_apply_coe {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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) (β : { β : G →* (levelProblem α hα f U).E // (levelProblem α hα f U).IsSolution β }) (g : G) : ↑((levelSolutionEquiv α hα f U) β) g = ↑(↑β g)

The lift into A/U associated with a solution has the same underlying map.

theorem TauCeti.levelSolutionEquiv_symm_apply_coe {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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) (g : G) : ↑(↑((levelSolutionEquiv α hα f U).symm β) g) = ↑β g

The solution associated with a lift into A/U has the same underlying map.

theorem TauCeti.nonempty_isSolution_levelProblem {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] {p : ℕ} (hG : HasPGroupSolutions p G) (hA : IsProP p A) (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) (U : OpenNormalSubgroup A) : Nonempty { β : G →* (levelProblem α hα f U).E // (levelProblem α hα f U).IsSolution β }

Every finite level has a solution when all finite p-kernel embedding problems do.

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

Solvability of all finite p-kernel embedding problems gives a solution at every level.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_levelSolution {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] (hG : IsTopologicallyFinitelyGenerated G) (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) (U : OpenNormalSubgroup A) : Finite (LevelSolution α hα f U)

Topological finite generation makes each level's solution set finite.