The pro-p Frattini/Burnside criterion

The "surjective on the Frattini quotient ⇒ surjective" criterion for pro-p groups, in index-p detection form — no Frattini subgroup object is introduced; the criterion quantifies over the open normal subgroups of index p directly (they are exactly the kernels of the maps to the Frattini quotient's ℤ/p-lines, and this is the form the Lemmas 3.6–3.8 proof's surjectivity legs check on generators):

• coatom_normal_of_pGroup / coatom_index_of_pGroup — the finite ingredients: a maximal subgroup of a finite p-group is normal of index p (finite p-groups are nilpotent, so the normalizer condition makes maximal subgroups normal; the resulting simple quotient is an abelian simple p-group, i.e. ℤ/p).
• eq_top_of_forall_map_eq_top — a closed subgroup of a profinite group whose image in every open-normal finite quotient is everything is everything (density via the open-normal neighbourhood basis).
• eq_top_of_forall_not_le_index_p — the criterion, subgroup form: a closed subgroup of a pro-p group contained in no open normal subgroup of index p is the whole group. (This is H·Φ(K) = K ⇒ H = K: the open normal subgroups of index p are precisely the maximal open subgroups, by the finite ingredients, and Φ(K) is their intersection.)
• surjective_of_forall_not_le_index_p / surjective_of_forall_index_p_quotient_surjective — the hom forms (Burnside basis criterion): a continuous homomorphism into a pro-p group whose composites to all index-p quotients are surjective is surjective.

Everything is proved (no axioms, no sorries; std-3). Paper use: Lemma 3.7 / Prop. 3.8's lift legs show constructed endomorphisms of D₀ are surjective by checking on B/2B = D₀^{ab} ⊗ 𝔽₂ — i.e. exactly on the index-2 quotients (p = 2).

Finite p-groups: maximal subgroups are normal of index p

theorem GQ2.coatom_normal_of_pGroup {p : ℕ} [Fact (Nat.Prime p)] {Q : Type u_1} [Group Q] [Finite Q] (hQ : IsPGroup p Q) {M : Subgroup Q} (hM : IsCoatom M) : M.Normal

A maximal subgroup of a finite p-group is normal (nilpotency ⇒ normalizer condition).

theorem GQ2.coatom_index_of_pGroup {p : ℕ} [Fact (Nat.Prime p)] {Q : Type u_1} [Group Q] [Finite Q] (hQ : IsPGroup p Q) {M : Subgroup Q} (hM : IsCoatom M) : M.index = p

A maximal subgroup of a finite p-group has index p (the quotient is a simple abelian p-group, i.e. ℤ/p).

The profinite criterion

theorem GQ2.eq_top_of_forall_map_eq_top {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [TotallyDisconnectedSpace K] {H : Subgroup K} (hHc : IsClosed ↑H) (h : ∀ (U : OpenNormalSubgroup K), Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) H = ⊤) : H = ⊤

A closed subgroup of a profinite group whose image in every open-normal finite quotient is everything is everything (the open normal subgroups are a neighbourhood basis at 1, so full images at every level mean density).

theorem GQ2.eq_top_of_forall_not_le_index_p {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [TotallyDisconnectedSpace K] (hK : IsProP p K) {H : Subgroup K} (hHc : IsClosed ↑H) (h : ∀ (M : OpenNormalSubgroup K), (↑M.toOpenSubgroup).index = p → ¬H ≤ ↑M.toOpenSubgroup) : H = ⊤

The pro-p Frattini criterion, subgroup form: a closed subgroup of a pro-p group contained in no open normal subgroup of index p is the whole group. (Equivalently H·Φ(K) = K ⇒ H = K: by coatom_normal_of_pGroup/coatom_index_of_pGroup the index-p open normal subgroups are exactly the maximal open subgroups.)

theorem GQ2.surjective_of_forall_not_le_index_p {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [TotallyDisconnectedSpace K] [T2Space K] {G : Type u_2} [Group G] [TopologicalSpace G] [CompactSpace G] (hK : IsProP p K) (f : G →ₜ* K) (h : ∀ (M : OpenNormalSubgroup K), (↑M.toOpenSubgroup).index = p → ¬f.range ≤ ↑M.toOpenSubgroup) : Function.Surjective ⇑f

The Burnside basis / Frattini criterion, hom form: a continuous homomorphism from a compact group into a pro-p group whose range lies in no index-p open normal subgroup is surjective.

theorem GQ2.surjective_of_forall_index_p_quotient_surjective {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [TotallyDisconnectedSpace K] [T2Space K] {G : Type u_2} [Group G] [TopologicalSpace G] [CompactSpace G] (hK : IsProP p K) (f : G →ₜ* K) (h : ∀ (M : OpenNormalSubgroup K), (↑M.toOpenSubgroup).index = p → Function.Surjective (⇑(QuotientGroup.mk' ↑M.toOpenSubgroup) ∘ ⇑f)) : Function.Surjective ⇑f

Convenience form: it suffices that the composite to every index-p quotient is surjective (the check the Lemmas 3.6–3.8 proof's legs perform on the marked generators).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 3.7 = ⟦lem-squarerootHNN⟧ (= lemma 3.8 in current tex)
• Prop 3.8 = ⟦prop-orientationlift⟧ (= proposition 3.9 in current tex)