Presentations of pro-p groups by free pro-p groups on pointed profinite spaces

A subset s of a profinite group G converging to 1 becomes, once 1 is added, a pointed profinite space (insert 1 s, 1). The presentation of G on s is the continuous homomorphism from the free pro-p group on this pointed space, TauCeti.freeProPInsertOne p s, to G that extends the inclusion of insert 1 s. It is surjective exactly when s generates G topologically, so every pro-p group is presented by the free pro-p group on a pointed profinite space, since every profinite group has a generating set converging to 1.

A set s converging to 1 is a basis converging to 1 of G (Ribes–Zalesskii, Profinite Groups, §3.3) when its presentation, or any continuous homomorphism from freeProPInsertOne p s sending the generator attached to each point to that point, is a topological isomorphism. The free pro-p group on (insert 1 s, 1) has topological generator rank #(s \ {1}), since (insert 1 s, 1) is the pointed one-point compactification of the discrete space s \ {1}; so for a basis s converging to 1 the cardinality #(s \ {1}) is the rank of G, and any two bases converging to 1 have the same cardinality once 1 is removed from each, as in Ribes–Zalesskii §3.3. Only #(s \ {1}) is invariant, not #s: both ∅ and {1} are bases converging to 1 of the trivial group, since freeProPInsertOne p s depends on s only through insert 1 s.

The presentation on s is minimal when its kernel lies in the Frattini subgroup of the free pro-p group. This is the condition under which a continuous homomorphic section makes the presentation an isomorphism (TauCeti.IsProP.continuousMulEquivOfLeftInverse); for presentations on a finite type it is the condition that the number of generators be the topological generator rank (TauCeti.presentedProP.subset_proPFrattini_iff_card_eq). Every pro-p group has a minimal presentation, on a dual family of a basis of its continuous 𝔽_p-dual, and the free pro-p group of a minimal presentation has the same topological generator rank as G.

Main definitions

• TauCeti.freeProPInsertOne: the free pro-p group on the pointed space (insert 1 s, 1).
• TauCeti.IsProP.presentation: the continuous homomorphism from it to G extending the inclusion.

Main results

• TauCeti.topologicalGeneratorRank_freeProPInsertOne: the free pro-p group on (insert 1 s, 1) has topological generator rank #(s \ {1}), because (insert 1 s, 1) is the pointed one-point compactification of the discrete space s \ {1}.
• TauCeti.ConvergesToOne.mk_diff_singleton_eq_topologicalGeneratorRank, TauCeti.ConvergesToOne.mk_diff_singleton_eq_of_continuousMulEquiv: for a basis s converging to 1, the cardinality #(s \ {1}) is the topological generator rank, so any two such bases of one group have the same cardinality once 1 is removed from each (Ribes–Zalesskii, Profinite Groups, §3.3).
• TauCeti.IsProP.presentation_surjective_iff: the presentation on s is surjective exactly when s generates G topologically.
• TauCeti.IsProP.exists_convergesToOne_presentation_surjective: every pro-p group is a quotient of the free pro-p group on a pointed profinite space.
• TauCeti.IsProP.exists_convergesToOne_presentation_surjective_ker_le_proPFrattini: every pro-p group has a minimal presentation, whose kernel lies in the Frattini subgroup of the free pro-p group and whose free pro-p group has the topological generator rank of G.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.8 and 3.3.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Section III.9.

@[reducible, inline]

abbrev TauCeti.freeProPInsertOne {G : Type u} [Group G] [TopologicalSpace G] (p : ℕ) (s : Set G) : Type u

The free pro-p group on the pointed space (insert 1 s, 1) cut out of a topological group G by a subset s. When s converges to 1 in a profinite group G, the subspace insert 1 s is a profinite space (TauCeti.ConvergesToOne.isClosed_insert_one), and this is the free pro-p group F_p(insert 1 s, 1) on a pointed profinite space.

Equations

• TauCeti.freeProPInsertOne p s = TauCeti.freeProCPointed (TauCeti.finiteGroupClassP p) ⟨1, ⋯⟩

theorem TauCeti.topologicalGeneratorRank_freeProPInsertOne_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {s : Set G} (hs : ConvergesToOne s) : topologicalGeneratorRank (freeProPInsertOne p s) ≤ Cardinal.mk ↑s

The free pro-p group on (insert 1 s, 1), for a set s converging to 1, has topological generator rank at most the cardinality of s: the generators attached to the points of s converge to 1 and generate it topologically.

theorem TauCeti.topologicalGeneratorRank_freeProPInsertOne {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [T2Space G] [Fact (Nat.Prime p)] {s : Set G} (hs : ConvergesToOne s) : topologicalGeneratorRank (freeProPInsertOne p s) = Cardinal.mk ↑(s \ {1})

The rank of the free pro-p group on a set converging to 1. For a set s converging to 1 in a Hausdorff group G, the pointed space (insert 1 s, 1) is the pointed one-point compactification of the discrete space s \ {1}, so the free pro-p group on it has topological generator rank exactly #(s \ {1}).

theorem TauCeti.ConvergesToOne.mk_diff_singleton_eq_topologicalGeneratorRank {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [T2Space G] [Fact (Nat.Prime p)] {s : Set G} (hs : ConvergesToOne s) {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : freeProPInsertOne p s ≃ₜ* H) : Cardinal.mk ↑(s \ {1}) = topologicalGeneratorRank H

A basis converging to 1 has the cardinality of the rank. If a topological group H is free pro-p on the pointed space (insert 1 s, 1) for a set s converging to 1, then the cardinality of s \ {1} is the topological generator rank of H.

theorem TauCeti.ConvergesToOne.mk_diff_singleton_eq_of_continuousMulEquiv {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [T2Space G] [Fact (Nat.Prime p)] {s : Set G} (hs : ConvergesToOne s) {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {G' : Type u} [Group G'] [TopologicalSpace G'] [T2Space G'] {t : Set G'} (ht : ConvergesToOne t) (e : freeProPInsertOne p s ≃ₜ* H) (e' : freeProPInsertOne p t ≃ₜ* H) : Cardinal.mk ↑(s \ {1}) = Cardinal.mk ↑(t \ {1})

Uniqueness of the cardinality of a basis converging to 1. Two sets s and t converging to 1 on whose pointed spaces one topological group H is free pro-p have the same cardinality once 1 is removed from each.

noncomputable def TauCeti.IsProP.presentation {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (s : Set G) : freeProPInsertOne p s →ₜ* G

The presentation of a pro-p group G on a subset s: the continuous homomorphism from the free pro-p group on the pointed space (insert 1 s, 1) to G that extends the inclusion of insert 1 s into G.

Equations

• hG.presentation s = TauCeti.freeProCPointed.lift ⋯ Subtype.val ⋯ ⋯

@[simp]

theorem TauCeti.IsProP.presentation_of {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (s : Set G) (x : ↑(insert 1 s)) : (hG.presentation s) (freeProCPointed.of (finiteGroupClassP p) ⟨1, ⋯⟩ x) = ↑x

The presentation sends the generator attached to a point of insert 1 s to that point.

theorem TauCeti.IsProP.presentation_comp_of {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (s : Set G) : ⇑(hG.presentation s) ∘ freeProCPointed.of (finiteGroupClassP p) ⟨1, ⋯⟩ = Subtype.val

The presentation composed with the generator map is the inclusion of insert 1 s.

theorem TauCeti.IsProP.presentation_surjective_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (s : Set G) : Function.Surjective ⇑(hG.presentation s) ↔ (Subgroup.closure s).topologicalClosure = ⊤

The presentation on s is surjective exactly when s generates G topologically.

theorem TauCeti.IsProP.exists_convergesToOne_presentation_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : ∃ (s : Set G), ConvergesToOne s ∧ Function.Surjective ⇑(hG.presentation s)

Every pro-p group is a quotient of the free pro-p group on a pointed profinite space: some subset s of G converging to 1 has surjective presentation.

theorem TauCeti.IsProP.exists_comp_presentation_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) [Fact (Nat.Prime p)] {ι : Type u} {g : ι → G} (hg : Filter.Tendsto g Filter.cofinite (nhds 1)) (b : Module.Basis ι (ZMod p) (continuousZModDual p G)) (hb : ∀ (i : ι) (x : continuousZModDual p G), (b.coord i) x = Multiplicative.toAdd ((Additive.toMul x) (g i))) (ψ : freeProPInsertOne p (Set.range g) →ₜ* Multiplicative (ZMod p)) : ∃ (χ : G →ₜ* Multiplicative (ZMod p)), χ.comp (hG.presentation (Set.range g)) = ψ

Characters factor through the presentation on a dual family. Let g tend to 1 and be a dual family of a basis b of the continuous 𝔽_p-dual of G. Every continuous 𝔽_p-character of the free pro-p group on (insert 1 (range g), 1) is a continuous 𝔽_p-character of G composed with the presentation on range g. This is what makes that presentation minimal.

theorem TauCeti.IsProP.exists_convergesToOne_presentation_surjective_ker_le_proPFrattini {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) [Fact (Nat.Prime p)] : ∃ (s : Set G), ConvergesToOne s ∧ Function.Surjective ⇑(hG.presentation s) ∧ (hG.presentation s).ker ≤ proPFrattini p (freeProPInsertOne p s) ∧ topologicalGeneratorRank (freeProPInsertOne p s) = topologicalGeneratorRank G

Every pro-p group has a minimal presentation by the free pro-p group on a pointed profinite space. Some subset s of G converging to 1 has surjective presentation whose kernel lies in the Frattini subgroup of the free pro-p group on (insert 1 s, 1), and that free pro-p group has the same topological generator rank as G. The subset is a dual family of a basis of the continuous 𝔽_p-dual of G.