Existence of Sylow subgroups in profinite groups

Every profinite group has a Sylow pro-p subgroup. The construction takes the inverse limit of the finite sets of Sylow p-subgroups of its finite continuous quotients. The transition map sends a Sylow subgroup to its image under the quotient map; Mathlib's finite Sylow theory says that these transition maps are surjective. Compactness, in the form of nonemptiness of a cofiltered limit of nonempty finite types, then supplies a compatible family.

The subgroup upstairs is limitSubgroup of that family, the intersection of its inverse images. Compatibility shows that its image in every finite quotient is exactly the chosen Sylow subgroup (map_mk'_limitSubgroup), which gives both the pro-p property and the prime-to-p index condition.

Main results

• isProPSylow_limitSubgroup: a compatible family of Sylow p-subgroups of the finite quotients cuts out a Sylow pro-p subgroup.
• exists_isProPSylow: every profinite group has a Sylow pro-p subgroup.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Corollary 2.3.6.

theorem TauCeti.isProPSylow_limitSubgroup {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (S : (U : OpenNormalSubgroup G) → Sylow p (G ⧸ ↑U.toOpenSubgroup)) (hS : ∀ ⦃U V : OpenNormalSubgroup G⦄ (hUV : U ≤ V), Subgroup.map (QuotientGroup.mapOfLE hUV) ↑(S U) = ↑(S V)) : IsProPSylow p (limitSubgroup fun (U : OpenNormalSubgroup G) => ↑(S U))

Sylow subgroups from a compatible family. A family S of Sylow p-subgroups of the finite continuous quotients of a profinite group, compatible along the quotient maps, cuts out a Sylow pro-p subgroup, whose image in each G ⧸ U is S U (map_mk'_limitSubgroup).

theorem TauCeti.exists_isProPSylow (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ∃ (P : Subgroup G), IsProPSylow p P

Every profinite group has a Sylow pro-p subgroup.