Sylow subgroups and the poset of pro-p subgroups

Every pro-p subgroup of a profinite group is contained in a Sylow pro-p subgroup, and the Sylow pro-p subgroups are exactly the maximal ones. The containment statement is proved in the sharper conjugacy form: given one Sylow pro-p subgroup P, every pro-p subgroup Q lies in a conjugate of P. At each finite continuous quotient the image of Q is a p-group and the image of P is a Sylow subgroup, so finite Sylow theory supplies a nonempty set of elements conjugating P past Q; these sets are closed and downward directed, and a point of their intersection conjugates P past Q in every finite quotient, hence past Q itself.

Maximality runs the same finite-level comparison without compactness: a pro-p subgroup containing a Sylow pro-p subgroup has the same image in every finite quotient, and a Sylow pro-p subgroup is closed, so the two subgroups agree. Together with containment this identifies the Sylow pro-p subgroups with the maximal pro-p subgroups, and shows that a pro-p group is its own unique Sylow pro-p subgroup.

Main results

• IsProP.exists_le_map_conj: a pro-p subgroup lies in a conjugate of any given Sylow pro-p subgroup.
• IsProP.exists_le_isProPSylow: a pro-p subgroup lies in a Sylow pro-p subgroup.
• IsProPSylow.eq_of_le: a Sylow pro-p subgroup is maximal among the pro-p subgroups.
• isProPSylow_iff_isProP_and_maximal: the Sylow pro-p subgroups are exactly the maximal pro-p subgroups.
• IsProPSylow.eq_top: a Sylow pro-p subgroup of a pro-p profinite group is the whole group. Together with IsProP.isProPSylow_top this says that a pro-p profinite group is its own unique Sylow pro-p subgroup.

References

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

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

Containment in a conjugate. A pro-p subgroup of a profinite group is contained in a conjugate of any given Sylow pro-p subgroup.

theorem TauCeti.IsProP.exists_le_isProPSylow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {Q : Subgroup G} (hQ : IsProP p ↥Q) : ∃ (P : Subgroup G), IsProPSylow p P ∧ Q ≤ P

Containment. Every pro-p subgroup of a profinite group is contained in a Sylow pro-p subgroup.

theorem TauCeti.IsProPSylow.eq_of_le {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 : IsProP p ↥Q) (hPQ : P ≤ Q) : P = Q

Maximality. A pro-p subgroup of a profinite group that contains a Sylow pro-p subgroup is equal to it. Equivalently, a closed pro-p subgroup of index prime to p is maximal among the pro-p subgroups.

theorem TauCeti.isProPSylow_of_maximal {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {Q : Subgroup G} (hQ : IsProP p ↥Q) (hmax : ∀ (R : Subgroup G), IsProP p ↥R → Q ≤ R → R ≤ Q) : IsProPSylow p Q

A maximal pro-p subgroup of a profinite group is a Sylow pro-p subgroup.

theorem TauCeti.isProPSylow_iff_isProP_and_maximal {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} : IsProPSylow p P ↔ IsProP p ↥P ∧ ∀ (R : Subgroup G), IsProP p ↥R → P ≤ R → R ≤ P

The Sylow pro-p subgroups are the maximal pro-p subgroups. Closedness is not part of the right-hand side: a maximal pro-p subgroup is closed because it is Sylow.

theorem TauCeti.IsProPSylow.eq_top {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hP : IsProPSylow p P) (hG : IsProP p G) : P = ⊤

A Sylow pro-p subgroup of a pro-p group is the whole group.