Conjugacy of Sylow subgroups in profinite groups

Any two Sylow pro-p subgroups of a profinite group are conjugate. This is containment read against maximality: a Sylow pro-p subgroup lies in a conjugate of any other by IsProP.exists_le_map_conj, and a conjugate of a Sylow pro-p subgroup is again Sylow pro-p, so IsProPSylow.eq_of_le upgrades that containment to an equality.

Main results

• IsProPSylow.exists_map_conj_eq: any two Sylow pro-p subgroups are conjugate.
• IsProPSylow.eq_of_normal: a normal Sylow pro-p subgroup is unique.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.3.

theorem TauCeti.IsProPSylow.exists_map_conj_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P Q : Subgroup G} (hP : IsProPSylow p P) (hQ : IsProPSylow p Q) : ∃ (g : G), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) P = Q

Any two Sylow pro-p subgroups of a profinite group are conjugate.

theorem TauCeti.IsProPSylow.eq_of_normal (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (P Q : Subgroup G) (hP : IsProPSylow p P) (hQ : IsProPSylow p Q) (hn : P.Normal) : P = Q

A normal Sylow pro-p subgroup is the unique Sylow pro-p subgroup.