Sylow subgroups of profinite groups

A Sylow pro-p subgroup is a closed pro-p subgroup whose image in every quotient by an open normal subgroup has index prime to p; for a profinite group these quotients are exactly the finite continuous ones. This file introduces that predicate and identifies its finite-level content in two ways: for a profinite group the prime-to-p condition is equivalent to prime-to-p supernatural index, and for a discrete group the predicate picks out exactly the subgroups of finite index underlying Mathlib's Sylow subgroups.

The finite comparison supplies the nonempty finite-level systems from which profinite Sylow subgroups are constructed. Existence and conjugacy in an arbitrary profinite group still require a separate compatible inverse-limit argument.

Main definitions and results

• IsProPSylow: the predicate for a Sylow pro-p subgroup.
• IsProPSylow.toSylow: the image in a quotient by an open normal subgroup, as a Mathlib Sylow subgroup of that quotient.
• IsProPSylow.map_continuousMulEquiv, IsProPSylow.map_conj: the predicate is preserved by isomorphisms of topological groups, in particular by conjugation.
• IsProP.isProPSylow_top: a pro-p group is its own Sylow pro-p subgroup.
• IsProPSylow.not_dvd_index_of_le: an open subgroup containing a Sylow pro-p subgroup of a compact group has index prime to p.
• isProPSylow_iff_isClosed_and_isProP_and_not_dvd_profiniteIndex: its supernatural-index formulation.
• isProPSylow_iff_isPGroup_and_not_dvd_index: its specialization to a discrete group.
• Sylow.isProPSylow: a Sylow subgroup of finite index in a discrete group satisfies the profinite predicate.
• isProPSylow_iff_exists_sylow_eq: agreement with Mathlib's bundled Sylow subgroups.

References

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

def TauCeti.IsProPSylow (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] (P : Subgroup G) : Prop

A subgroup P of a topological group is a Sylow pro-p subgroup when it is closed, is itself pro-p, and its image in every quotient by an open normal subgroup has index not divisible by p.

The definition is meaningful for an arbitrary topological group; for a profinite group the quotients above are exactly the finite continuous ones. Compactness and total disconnectedness enter the existence and conjugacy theorems, rather than the predicate.

Equations

• TauCeti.IsProPSylow p P = (IsClosed ↑P ∧ TauCeti.IsProP p ↥P ∧ ∀ (U : OpenNormalSubgroup G), ¬p ∣ (Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) P).index)

theorem TauCeti.isProPSylow_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} : IsProPSylow p P ↔ IsClosed ↑P ∧ IsProP p ↥P ∧ ∀ (U : OpenNormalSubgroup G), ¬p ∣ (Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) P).index

A subgroup is Sylow pro-p exactly when it is closed, pro-p, and its image in every quotient by an open normal subgroup has index prime to p.

theorem TauCeti.IsProPSylow.isClosed {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} (hP : IsProPSylow p P) : IsClosed ↑P

A Sylow pro-p subgroup is closed.

theorem TauCeti.IsProPSylow.isProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} (hP : IsProPSylow p P) : IsProP p ↥P

A Sylow pro-p subgroup is pro-p in its subspace topology.

theorem TauCeti.IsProPSylow.not_dvd_index {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} (hP : IsProPSylow p P) (U : OpenNormalSubgroup G) : ¬p ∣ (Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) P).index

The image of a Sylow pro-p subgroup in every quotient by an open normal subgroup has index prime to p.

def TauCeti.IsProPSylow.toSylow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [Fact (Nat.Prime p)] (hP : IsProPSylow p P) (U : OpenNormalSubgroup G) : Sylow p (G ⧸ ↑U.toOpenSubgroup)

The image of a Sylow pro-p subgroup in the quotient by an open normal subgroup, packaged as a Mathlib Sylow subgroup of that quotient: it is a p-group of index prime to p.

Equations

• hP.toSylow U = ⋯.toSylow ⋯

@[simp]

theorem TauCeti.IsProPSylow.toSylow_coe {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [Fact (Nat.Prime p)] (hP : IsProPSylow p P) (U : OpenNormalSubgroup G) : ↑(hP.toSylow U) = Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) P

The underlying subgroup of IsProPSylow.toSylow is the image of P in the quotient.

theorem TauCeti.IsProPSylow.map_continuousMulEquiv {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} {H : Type v} [Group H] [TopologicalSpace H] (hP : IsProPSylow p P) (e : G ≃ₜ* H) : IsProPSylow p (Subgroup.map (↑e) P)

The image of a Sylow pro-p subgroup under an isomorphism of topological groups is a Sylow pro-p subgroup.

theorem TauCeti.IsProPSylow.map_conj {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [SeparatelyContinuousMul G] (hP : IsProPSylow p P) (g : G) : IsProPSylow p (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) P)

A conjugate of a Sylow pro-p subgroup is a Sylow pro-p subgroup.

theorem TauCeti.IsProP.isProPSylow_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [Fact (Nat.Prime p)] (hG : IsProP p G) : IsProPSylow p ⊤

A pro-p topological group is its own Sylow pro-p subgroup: the top subgroup is closed, is pro-p, and its image in every quotient by an open normal subgroup is everything, hence of index 1.

theorem TauCeti.isProPSylow_iff_isClosed_and_isProP_and_not_dvd_profiniteIndex {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [CompactSpace G] [IsTopologicalGroup G] (q : Nat.Primes) : IsProPSylow (↑q) P ↔ IsClosed ↑P ∧ IsProP ↑q ↥P ∧ ¬Supernatural.primePower q 1 ∣ P.profiniteIndex

A subgroup of a profinite group is Sylow pro-p exactly when it is closed, is pro-p, and its supernatural index is prime to p.

theorem TauCeti.IsProPSylow.not_dvd_index_of_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [CompactSpace G] [SeparatelyContinuousMul G] (hP : IsProPSylow p P) (V : OpenSubgroup G) (hPV : P ≤ ↑V) : ¬p ∣ (↑V).index

An open subgroup containing a Sylow pro-p subgroup of a compact group has index prime to p. This is the finite-index content of the prime-to-p condition in isProPSylow_iff_isClosed_and_isProP_and_not_dvd_profiniteIndex: every open subgroup V ≥ P has [G : V] prime to p. (The converse fails: an open subgroup of index prime to p contains some Sylow pro-p subgroup, but not necessarily the given P.)

@[simp]

theorem TauCeti.isProPSylow_iff_isPGroup_and_not_dvd_index {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [DiscreteTopology G] : IsProPSylow p P ↔ IsPGroup p ↥P ∧ ¬p ∣ P.index

On a discrete group, a subgroup is Sylow pro-p exactly when it is a p-group of index prime to p.

theorem Sylow.isProPSylow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Fact (Nat.Prime p)] (Q : Sylow p G) [(↑Q).FiniteIndex] : TauCeti.IsProPSylow p ↑Q

A Mathlib Sylow subgroup of finite index in a discrete group is a Sylow pro-p subgroup.

theorem TauCeti.isProPSylow_iff_exists_sylow_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} [DiscreteTopology G] [Fact (Nat.Prime p)] [P.FiniteIndex] : IsProPSylow p P ↔ ∃ (Q : Sylow p G), ↑Q = P

A subgroup of finite index in a discrete group satisfies the profinite predicate exactly when it is the underlying subgroup of a Mathlib Sylow subgroup.

theorem TauCeti.exists_isProPSylow_of_finite {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Fact (Nat.Prime p)] [Finite G] : ∃ (P : Subgroup G), IsProPSylow p P

Every finite discrete group has a Sylow pro-p subgroup. This is the finite-level existence input for the inverse-limit construction of profinite Sylow subgroups.