Sylow subgroups of commutative profinite groups

In a commutative profinite group G, a Sylow pro-p subgroup P maps isomorphically onto the maximal pro-p quotient G(p) = G ⧸ proPKernel p G: the restriction of the quotient map to P is a topological group isomorphism P ≃ₜ* G(p). In particular a pro-p subgroup of G meets the pro-p kernel trivially. Conversely, a closed subgroup that maps bijectively onto G(p) is Sylow pro-p, so the bijection characterizes the Sylow pro-p subgroups of a commutative profinite group.

The isomorphism transfers questions about a Sylow pro-p subgroup, a subgroup of G, to the maximal pro-p quotient, a quotient of G determined by its universal property. This is the form in which the p-Sylow subgroups of the profinite integers are identified with ℤ_p, in TauCeti.Topology.Algebra.Group.Profinite.ZHat.PadicInt.

Main results

• TauCeti.IsProP.disjoint_proPKernel: in a commutative profinite group, a pro-p subgroup meets the pro-p kernel trivially.
• TauCeti.IsProPSylow.bijective_domRestrict_maximalProPQuotient_mk: a Sylow pro-p subgroup maps bijectively onto the maximal pro-p quotient.
• TauCeti.IsProPSylow.continuousMulEquivMaximalProPQuotient: the resulting topological group isomorphism P ≃ₜ* G(p).
• TauCeti.isProPSylow_iff_isClosed_and_bijective_domRestrict_maximalProPQuotient_mk: the closed subgroups mapping bijectively onto G(p) are exactly the Sylow pro-p subgroups.

References

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

theorem TauCeti.IsProP.disjoint_proPKernel {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsMulCommutative G] {P : Subgroup G} (hP : IsProP p ↥P) : Disjoint P (proPKernel p G)

In a commutative profinite group, a pro-p subgroup meets the pro-p kernel trivially: a nontrivial element of the subgroup has nontrivial image of p-power order in some finite quotient, hence survives in a p-group quotient.

theorem TauCeti.IsProPSylow.bijective_domRestrict_maximalProPQuotient_mk {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsMulCommutative G] {P : Subgroup G} (hP : IsProPSylow p P) : Function.Bijective ⇑((maximalProPQuotient.mk p G).domRestrict P)

A Sylow pro-p subgroup of a commutative profinite group maps bijectively onto the maximal pro-p quotient.

noncomputable def TauCeti.IsProPSylow.continuousMulEquivMaximalProPQuotient {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsMulCommutative G] {P : Subgroup G} (hP : IsProPSylow p P) : ↥P ≃ₜ* maximalProPQuotient p G

A Sylow pro-p subgroup of a commutative profinite group is its maximal pro-p quotient: the quotient map restricts to a topological group isomorphism P ≃ₜ* G(p).

Equations

• hP.continuousMulEquivMaximalProPQuotient = { toMulEquiv := MulEquiv.ofBijective ((TauCeti.maximalProPQuotient.mk p G).domRestrict P) ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.IsProPSylow.continuousMulEquivMaximalProPQuotient_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsMulCommutative G] {P : Subgroup G} (hP : IsProPSylow p P) (x : ↥P) : hP.continuousMulEquivMaximalProPQuotient x = (maximalProPQuotient.mk p G) ↑x

The isomorphism from a Sylow pro-p subgroup onto the maximal pro-p quotient is the quotient map.

theorem TauCeti.isProPSylow_iff_isClosed_and_bijective_domRestrict_maximalProPQuotient_mk {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsMulCommutative G] {P : Subgroup G} : IsProPSylow p P ↔ IsClosed ↑P ∧ Function.Bijective ⇑((maximalProPQuotient.mk p G).domRestrict P)

The Sylow pro-p subgroups of a commutative profinite group are exactly the closed subgroups that map bijectively onto the maximal pro-p quotient.