Finite embedding problems with p-group kernel

Two solvability predicates for the finite embedding problems of a topological group G, and the reduction of one to the other.

• TauCeti.HasElementaryAbelianSolutions p G: every finite embedding problem for G whose kernel ker α is commutative and killed by p (elementary abelian, when p is prime) has a solution.
• TauCeti.HasPGroupSolutions p G: every finite embedding problem for G whose kernel is a p-group has a solution.

The second predicate implies the first, since a group killed by p is a p-group. The main theorem, TauCeti.HasElementaryAbelianSolutions.hasPGroupSolutions, is the converse for a prime p. A p-group kernel N = ker α is filtered by its lower p-central series λ_k(N), whose terms are normal in E and whose successive factors λ_k(N) ⧸ λ_{k+1}(N) are elementary abelian. A solution is built one layer at a time: a solution modulo λ_k(N), that is a homomorphism β_k : G → E ⧸ λ_k(N) with open kernel lying over π, is lifted through the surjection E ⧸ λ_{k+1}(N) ↠ E ⧸ λ_k(N), whose kernel is elementary abelian, by solving the finite embedding problem TauCeti.FiniteEmbeddingProblem.ofSurjective cut out by that surjection and β_k (TauCeti.HasElementaryAbelianSolutions.exists_comp_eq). Since the series reaches ⊥, the last stage is a solution of the original problem.

The two predicates quantify over the finite embedding problems whose groups live in the universe of G. Every finite group is isomorphic to one in any universe, so this is no restriction on the finite groups that occur, and it keeps the predicates free of universe parameters that nothing else would determine. Only the elementary abelian case consumes cohomology: the extension 1 → ker α → E → Q → 1 has a class in H²(Q, ker α), and its pullback along π to H²(G, ker α) is the obstruction to solving the problem, so the vanishing of H²(G, M) for the finite discrete G-modules M killed by p gives HasElementaryAbelianSolutions p G, and the theorem here extends it to p-group kernels.

Main definitions

• TauCeti.HasElementaryAbelianSolutions: every finite embedding problem with commutative kernel killed by p has a solution.
• TauCeti.HasPGroupSolutions: every finite embedding problem with p-group kernel has a solution.

Main results

• TauCeti.HasPGroupSolutions.hasElementaryAbelianSolutions: solvability with p-group kernel gives solvability with commutative kernel killed by p.
• TauCeti.HasElementaryAbelianSolutions.exists_comp_eq: under HasElementaryAbelianSolutions p G, a homomorphism β : G → F with open kernel lifts through a surjection φ : E ↠ F of finite groups whose kernel is commutative and killed by p.
• TauCeti.HasElementaryAbelianSolutions.hasPGroupSolutions: for a prime p, solvability with elementary abelian kernel gives solvability with p-group kernel.
• TauCeti.FiniteEmbeddingProblem.isPGroup_E: over a pro-p group, a finite embedding problem with p-group kernel involves only finite p-groups.

References

• J.-P. Serre, Galois Cohomology, Chapter I, §3.4, Proposition 16 and its proof.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, Chapter III, §5.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 7.6.

def TauCeti.HasPGroupSolutions (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

Solvability with p-group kernel. Every finite embedding problem for G, with groups in the universe of G, whose kernel ker α is a p-group has a solution.

Equations

• TauCeti.HasPGroupSolutions p G = ∀ (P : TauCeti.FiniteEmbeddingProblem G), IsPGroup p ↥P.α.ker → ∃ (β : G →* P.E), P.IsSolution β

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

The defining property of HasPGroupSolutions, as a lemma usable outside this module.

theorem TauCeti.HasPGroupSolutions.hasElementaryAbelianSolutions {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : HasPGroupSolutions p G) : HasElementaryAbelianSolutions p G

Solvability with p-group kernel gives solvability with commutative kernel killed by p: such a kernel is a p-group.

theorem TauCeti.HasElementaryAbelianSolutions.exists_comp_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : HasElementaryAbelianSolutions p G) {E F : Type u} [Group E] [Finite E] [Group F] (φ : E →* F) (hφ : Function.Surjective ⇑φ) (hpow : ∀ x ∈ φ.ker, x ^ p = 1) (hcomm : ∀ x ∈ φ.ker, ∀ y ∈ φ.ker, x * y = y * x) (β : G →* F) (hβ : IsOpen ↑β.ker) : ∃ (β' : G →* E), IsOpen ↑β'.ker ∧ φ.comp β' = β

Lifting through a commutative kernel killed by p. If every finite embedding problem for G with commutative kernel killed by p has a solution, then a homomorphism β : G → F with open kernel lifts, with open kernel, through every surjection φ : E ↠ F of finite groups whose kernel is commutative and killed by p.

theorem TauCeti.HasElementaryAbelianSolutions.hasPGroupSolutions {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fact (Nat.Prime p)] (h : HasElementaryAbelianSolutions p G) : HasPGroupSolutions p G

Solvability with p-group kernel from solvability with elementary abelian kernel. For a prime p, if every finite embedding problem for G with elementary abelian kernel has a solution, then every finite embedding problem for G whose kernel is a p-group has a solution.

theorem TauCeti.FiniteEmbeddingProblem.isPGroup_E {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hG : IsProP p G) (hP : IsPGroup p ↥P.α.ker) : IsPGroup p P.E

Over a pro-p group, a finite embedding problem with p-group kernel is an extension of finite p-groups: the quotient Q of G is a p-group, hence so is the extension E of Q by ker α.