Solvability with elementary abelian kernel

TauCeti.HasElementaryAbelianSolutions p G says that every finite embedding problem for G with commutative kernel killed by p has a solution. For prime p such a kernel is exactly an elementary abelian p-group, whence the name; for composite p the condition is weaker. The finite groups are taken in the universe of G, as every finite group is isomorphic to one in that universe.

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

Solvability with elementary abelian kernel. Every finite embedding problem for G, with groups in the universe of G, whose kernel ker α is commutative and killed by p, has a solution. For prime p these kernels are the elementary abelian p-groups.

Equations

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

theorem TauCeti.hasElementaryAbelianSolutions_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : HasElementaryAbelianSolutions p G ↔ ∀ (P : FiniteEmbeddingProblem G), (∀ x ∈ P.α.ker, x ^ p = 1) → (∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) → ∃ (β : G →* P.E), P.IsSolution β

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