Documentation

TauCeti.Topology.Algebra.Group.Profinite.ProP.MinimalPresentation

Minimal presentations of pro-p groups #

A continuous surjection f : G ↠ H of pro-p groups, with G topologically finitely generated, preserves the topological generator rank exactly when ker f ≤ Φ(G) (TauCeti.IsProP.topologicalGeneratorRankNat_eq_iff_ker_le_proPFrattini). Applied to the quotient map from a free pro-p group of finite rank onto a presented pro-p group, whose kernel is the closed normal closure of the relators (TauCeti.presentedProP.ker_mk), this characterizes minimal presentations: a presentation G ≅ ⟨X ∣ rels⟩ with X finite is minimal, meaning Nat.card X = d(G), exactly when every relator lies in the Frattini subgroup Φ(F) = closure (Fᵖ [F, F]) of the free pro-p group F on X. Every topologically finitely generated pro-p group has such a presentation, on any finite type of cardinality d(G). This is the condition R ≤ Φ(F) on the relation subgroup under which the relation rank of G is read off from the presentation, and it is the normalization a Demushkin relator satisfies.

Minimal presentations of a group on a given finite type are unique up to a change of basis of the free group. Two continuous surjections g, h : F ↠ H from the free pro-p group of finite rank, with ker g ≤ Φ(F), satisfy h = g ∘ α for a continuous automorphism α of F. Consequently two pro-p groups presented on the same finite type, the second presentation minimal, are topologically isomorphic exactly when an automorphism of the free group carries the relation subgroup of the first onto that of the second. This is the form in which an isomorphism of one-relator groups becomes a statement about the relators, as in Labute's classification of Demushkin groups.

Main results #

References #

A pro-p group presented on a finite type X has topological generator rank at most Nat.card X: it is the image of the free pro-p group on X, of rank Nat.card X, under the continuous surjection mk.

Minimal presentations. A pro-p group presented on a finite type X has topological generator rank Nat.card X exactly when every relator lies in the Frattini subgroup of the free pro-p group on X.

theorem TauCeti.presentedProP.linearIndependent_frattiniQuotient_of {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) :
LinearIndependent (ZMod p) fun (x : X) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p (presentedProP p X rels))) (of p rels x))

The generators of a minimal presentation are linearly independent in the Frattini quotient. If every relator lies in the Frattini subgroup of the free pro-p group on X, the classes of the canonical generators of ⟨X ∣ rels⟩ in its Frattini quotient are linearly independent over 𝔽_p, for a generating type X of any cardinality: the relation subgroup lies in the Frattini subgroup, so mk induces an injection of Frattini quotients.

A presentation G ≅ ⟨X ∣ rels⟩ of a topologically finitely generated group on a finite type X has all its relators in the Frattini subgroup of the free pro-p group on X exactly when it is minimal, that is when Nat.card X is the topological generator rank of G.

The relation subgroup of a minimal presentation of a group with trivial Frattini subgroup is the Frattini subgroup of the free group. For a presentation G ≅ ⟨X ∣ rels⟩ with relators in Φ(F), F the free pro-p group on X, of a topological group G with Φ(G) = 1, the closed normal closure of the relators is Φ(F).

theorem TauCeti.freeProP.exists_continuousMulEquiv_comp_eq {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] {H : Type v} [Group H] [TopologicalSpace H] [T2Space H] (g h : freeProP p X →ₜ* H) (hg : Function.Surjective ⇑g) (hker : (↑g).ker ≤ proPFrattini p (freeProP p X)) (hh : Function.Surjective ⇑h) :
∃ (α : freeProP p X ≃ₜ* freeProP p X), g.comp ↑α = h

Two surjections of a free pro-p group onto the same group differ by an automorphism when one of them is minimal. Let F be the free pro-p group on a finite type and let g, h : F → H be continuous surjections onto a Hausdorff group, the kernel of g lying in the Frattini subgroup Φ(F). Then h = g ∘ α for a continuous automorphism α of F.

theorem TauCeti.presentedProP.exists_continuousMulEquiv_topologicalClosure_normalClosure_image_eq {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {rels rels' : Set (freeProP p X)} [Finite X] (hrels' : rels' ⊆ ↑(proPFrattini p (freeProP p X))) (e : presentedProP p X rels ≃ₜ* presentedProP p X rels') :
∃ (α : freeProP p X ≃ₜ* freeProP p X), (∀ (x : freeProP p X), (mk p rels') (α x) = e ((mk p rels) x)) ∧ (Subgroup.normalClosure (⇑α '' rels)).topologicalClosure = (Subgroup.normalClosure rels').topologicalClosure

Isomorphic presentations with a minimal target differ by a change of basis. Let ⟨X ∣ rels⟩ and ⟨X ∣ rels'⟩ be pro-p groups presented on the same finite type, with the relators rels' in the Frattini subgroup of the free pro-p group F on X. Every topological isomorphism e between them lifts to a continuous automorphism α of F, and α carries the relation subgroup of the first presentation onto that of the second: the closed normal closure of the relators α '' rels is the closed normal closure of rels'. For one relator on each side this reads closure ⟪α r⟫ = closure ⟪r'⟫, since α '' {r} = {α r}.

theorem TauCeti.presentedProP.nonempty_continuousMulEquiv_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {rels rels' : Set (freeProP p X)} [Finite X] (hrels' : rels' ⊆ ↑(proPFrattini p (freeProP p X))) :

Presentations of isomorphic groups, one of them minimal, differ by a change of basis. Pro-p groups presented on the same finite type X, with the relators rels' in the Frattini subgroup of the free pro-p group F on X, are topologically isomorphic exactly when a continuous automorphism α of F carries the closed normal closure of rels onto that of rels', that is when the closed normal closure of α '' rels is the closed normal closure of rels'.

Existence of minimal presentations. A topologically finitely generated pro-p group has a presentation on any finite type of cardinality its topological generator rank, with all relators in the Frattini subgroup of the free pro-p group.