Finite p-group quotients of topological groups

A nontrivial finite p-group quotient of a topological group by an open normal subgroup V has an open normal subgroup W > V such that W ⧸ V has order p and G ⧸ W is a p-group. This is the inductive step for reducing statements about finite p-group quotients to the prime-order case.

Main result

• TauCeti.exists_isOpen_normal_lt_card_quotient_eq_prime: the existence of such a W.

theorem TauCeti.exists_isOpen_normal_lt_card_quotient_eq_prime {p : ℕ} (hp : Nat.Prime p) {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {V : Subgroup G} [V.Normal] (hV : IsOpen ↑V) [Finite (G ⧸ V)] [Nontrivial (G ⧸ V)] (hpV : IsPGroup p (G ⧸ V)) : ∃ (W : Subgroup G) (x : W.Normal), V < W ∧ IsOpen ↑W ∧ Nat.card (↥W ⧸ V.subgroupOf W) = p ∧ IsPGroup p (G ⧸ W)

A nontrivial finite p-group quotient G ⧸ V by an open normal subgroup has an open normal overgroup W > V with W ⧸ V of order p and G ⧸ W a p-group: W is the preimage of a central subgroup of order p.