H²(G, 𝔽_p) counts the relations of a pro-p group

Let G be a profinite group with H²(G, 𝔽_p) = 0, for instance a free pro-p group, and let N be a closed normal subgroup contained in the pro-p Frattini subgroup Φ(G). The transgression H¹(N, 𝔽_p)^G → H²(G ⧸ N, 𝔽_p) is then bijective (TauCeti.transgression_bijective_of_le_proPFrattini), and H¹(N, 𝔽_p)^G is the continuous 𝔽_p-dual of N ⧸ Nᵖ[N, G] (TauCeti.natCard_H1ConjInvariants). So H²(G ⧸ N, 𝔽_p) is finite exactly when N ⧸ Nᵖ[N, G] is topologically finitely generated, and then it has p ^ d(N ⧸ Nᵖ[N, G]) elements.

Applied to a minimal presentation G ≅ ⟨X ∣ rels⟩ of a pro-p group, that is a presentation whose relators lie in the Frattini subgroup of the free pro-p group F on X (TauCeti.presentedProP.subset_proPFrattini_iff_card_eq), with relation subgroup R the closed normal closure of the relators, this identifies the order of H²(G, 𝔽_p) with p ^ d(R ⧸ Rᵖ[R, F]). By Burnside's basis theorem for normal generation (TauCeti.IsProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_le_iff), the exponent d(R ⧸ Rᵖ[R, F]) is the least number of generators of R as a closed normal subgroup of F: the exponent r in the order p ^ r of H²(G, 𝔽_p) counts the relations of G. Since H²(G, 𝔽_p) does not see the presentation, that count is the same for every minimal presentation of G. This is the presentation independence of the relation rank.

For a presentation G ≅ ⟨X ∣ rels⟩ on a finite type X that need not be minimal, the count is the five-term exact sequence of 1 → R → F → G → 1,

0 → H¹(G, 𝔽_p) → H¹(F, 𝔽_p) → H¹(R, 𝔽_p)^F → H²(G, 𝔽_p) → H²(F, 𝔽_p) = 0,

in which H¹(F, 𝔽_p) has dimension #X, H¹(G, 𝔽_p) has dimension d(G) and H¹(R, 𝔽_p)^F has dimension d(R ⧸ Rᵖ[R, F]): exactness gives #X + r(G) = d(G) + d(R ⧸ Rᵖ[R, F]) (TauCeti.presentedProP.card_add_finrank_H2). The surjectivity of the transgression alone shows that H²(G, 𝔽_p) is finite as soon as R ⧸ Rᵖ[R, F] is topologically finitely generated, in particular when there are finitely many relators, on any generating type X (TauCeti.presentedProP.finite_H2_of_finite).

Since H²(G, 𝔽_p) is killed by p it is a vector space over 𝔽_p (TauCeti.ContCohomology.instModuleZModH2), and its dimension is the relation rank r(G) of G. Read as an identity of cardinals, dim H²(G, 𝔽_p) = d(R ⧸ Rᵖ[R, F]) needs no finiteness hypothesis, exactly as Burnside's basis theorem (TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual) does not: a topologically finitely generated pro-p group with infinitely many relations has an H²(G, 𝔽_p) of infinite dimension. When R ⧸ Rᵖ[R, F] is topologically finitely generated the dimension is the natural-number rank, the exponent r in the count p ^ r above.

The statements are about the order and the dimension of H²(G, 𝔽_p), for the explicit continuous cohomology H2 of the trivial G-module 𝔽_p; the action of G on ZMod p is carried as an instance together with the hypothesis that it is trivial, as in TauCeti.Topology.Algebra.Group.Profinite.ProP.InvariantDual. The statements about a quotient G ≅ F ⧸ R of a free pro-p group F (TauCeti.finite_H2_iff_of_le_proPFrattini, TauCeti.natCard_H2_of_le_proPFrattini and TauCeti.card_add_finrank_H2_of_isClosed) carry the action of F on 𝔽_p in the same way, as an instance with the hypothesis that it is trivial. The TauCeti.presentedProP statements about a presentation do not: they supply the trivial action of F internally, and only the action of G appears. The count and the finiteness for a presentation on a finite type are also stated on the canonical carrier cohomFp p G 2 of the relation rank, in which no action appears at all (TauCeti.presentedProP.card_add_finrank_cohomFp_two and TauCeti.presentedProP.module_finite_cohomFp_two_of_finite).

Main results

• TauCeti.natCard_H2_quotient_of_le_proPFrattini: for profinite G with H²(G, 𝔽_p) = 0 and N ≤ Φ(G) closed normal, H²(G ⧸ N, 𝔽_p) has p ^ d(N ⧸ Nᵖ[N, G]) elements; TauCeti.finite_H2_quotient_iff_of_le_proPFrattini is the finiteness criterion.
• TauCeti.h2DualEquiv: for G ≅ F ⧸ R with F a free pro-p group and R ≤ Φ(F) closed normal, the inverse transgression identifies H²(G, 𝔽_p) with the continuous 𝔽_p-dual of R ⧸ Rᵖ[R, F].
• TauCeti.natCard_H2_of_le_proPFrattini: for G ≅ F ⧸ R with F a free pro-p group and R ≤ Φ(F) closed normal, H²(G, 𝔽_p) has p ^ d(R ⧸ Rᵖ[R, F]) elements; TauCeti.finite_H2_iff_of_le_proPFrattini is the finiteness criterion, and TauCeti.lift_rank_H2_of_le_proPFrattini, TauCeti.finrank_H2_of_le_proPFrattini are the dimension form of the count, as cardinals and as natural numbers.
• TauCeti.presentedProP.natCard_H2: for a minimal presentation ⟨X ∣ rels⟩ ≅ G with relation subgroup R, H²(G, 𝔽_p) has p ^ d(R ⧸ Rᵖ[R, F]) elements, and TauCeti.presentedProP.natCard_H2_le_pow_iff: it has at most p ^ n elements exactly when R is generated as a closed normal subgroup of F by at most n elements.
• TauCeti.presentedProP.lift_rank_H2: the relation rank, dim_{𝔽_p} H²(G, 𝔽_p) = d(R ⧸ Rᵖ[R, F]), as an identity of cardinals, with TauCeti.presentedProP.finrank_H2 its topologically finitely generated case, and TauCeti.presentedProP.finrank_H2_le_iff: that dimension is at most n exactly when R is generated as a closed normal subgroup of F by at most n elements.
• TauCeti.presentedProP.finite_H2_iff: H²(G, 𝔽_p) is finite exactly when R ⧸ Rᵖ[R, F] is topologically finitely generated.
• TauCeti.natCard_H2_mul_pow_card_of_isClosed and TauCeti.card_add_finrank_H2_of_isClosed: for G ≅ F ⧸ R with F free pro-p on a finite type X and R closed normal with R ⧸ Rᵖ[R, F] topologically finitely generated, |H²(G, 𝔽_p)| · p ^ #X = p ^ (d(G) + d(R ⧸ Rᵖ[R, F])) and #X + dim H²(G, 𝔽_p) = d(G) + d(R ⧸ Rᵖ[R, F]); no minimality is assumed.
• TauCeti.presentedProP.card_add_finrank_H2 and TauCeti.presentedProP.card_add_finrank_cohomFp_two: the same identity for a presentation ⟨X ∣ rels⟩ ≅ G on a finite type, on the explicit and on the canonical carrier.
• TauCeti.finite_H2_of_isClosed, TauCeti.presentedProP.finite_H2_of_finite and TauCeti.presentedProP.module_finite_cohomFp_two_of_finite: H²(G, 𝔽_p) is finite when R ⧸ Rᵖ[R, F] is topologically finitely generated, in particular for finitely many relators on any generating type.
• TauCeti.presentedProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_of_finite: finitely many relators make R ⧸ Rᵖ[R, F] topologically finitely generated, and TauCeti.presentedProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_le_card: they bound d(R ⧸ Rᵖ[R, F]), the least number of generators of R as a closed normal subgroup.
• TauCeti.presentedProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_eq: the count d(R ⧸ Rᵖ[R, F]) is the same for any two minimal presentations of G, and TauCeti.presentedProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_iff: so is its finiteness.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.5).
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), §1.4.
• J.-P. Serre, Galois Cohomology, Chapter I, §4.3.

theorem TauCeti.finite_H2_quotient_iff_of_le_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {N : Subgroup G} [N.Normal] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] [Subsingleton (ContCohomology.H2 G (ZMod p))] (hN : IsClosed ↑N) (hle : N ≤ proPFrattini p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Finite (ContCohomology.H2 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) (ZMod p))) ↔ IsTopologicallyFinitelyGenerated (↥N ⧸ (pLowerCentralStep p N).subgroupOf N)

Finiteness of H²(G ⧸ N, 𝔽_p). Let G be a profinite group acting trivially on 𝔽_p with H²(G, 𝔽_p) = 0, and let N ≤ Φ(G) be a closed normal subgroup. Then H²(G ⧸ N, 𝔽_p) is finite exactly when N ⧸ Nᵖ[N, G] is topologically finitely generated.

theorem TauCeti.natCard_H2_quotient_of_le_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {N : Subgroup G} [N.Normal] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] [Subsingleton (ContCohomology.H2 G (ZMod p))] (hN : IsClosed ↑N) (hle : N ≤ proPFrattini p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥N ⧸ (pLowerCentralStep p N).subgroupOf N)) : Nat.card (ContCohomology.H2 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) (ZMod p))) = p ^ topologicalGeneratorRankNat (↥N ⧸ (pLowerCentralStep p N).subgroupOf N) h

H²(G ⧸ N, 𝔽_p) counts the generators of N ⧸ Nᵖ[N, G]. Let G be a profinite group acting trivially on 𝔽_p with H²(G, 𝔽_p) = 0, and let N ≤ Φ(G) be a closed normal subgroup with N ⧸ Nᵖ[N, G] topologically finitely generated. Then H²(G ⧸ N, 𝔽_p) has p ^ d(N ⧸ Nᵖ[N, G]) elements, where d is the topological generator rank.

noncomputable def TauCeti.h2QuotientEquiv {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : ContCohomology.H2 (freeProP p X ⧸ R) ↥(FixedPoints.addSubgroup (↥R) (ZMod p)) ≃+ ContCohomology.H2 G (ZMod p)

Transport of H²(F ⧸ R, 𝔽_p ^ R) along a topological isomorphism F ⧸ R ≃ₜ* G, when both F and G act trivially on 𝔽_p; TauCeti.h2QuotientEquiv_apply reads it on the explicit models.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.h2QuotientEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (x : ContCohomology.H2 (freeProP p X ⧸ R) ↥(FixedPoints.addSubgroup (↥R) (ZMod p))) : (h2QuotientEquiv e htrivF htriv) x = (ContCohomology.explicitMap2 (freeProP p X ⧸ R) (↥(FixedPoints.addSubgroup (↥R) (ZMod p))) G (ZMod p) (↑e.symm) (FixedPoints.addSubgroup (↥R) (ZMod p)).subtype ⋯ ⋯) x

On the explicit models, the transport of H²(F ⧸ R, 𝔽_p ^ R) along e : F ⧸ R ≃ₜ* G is the pullback along e.symm, with the coefficients 𝔽_p ^ R = 𝔽_p read through the inclusion.

noncomputable def TauCeti.h2DualEquiv {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hRc : IsClosed ↑R) (hR : R ≤ proPFrattini p (freeProP p X)) (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : ContCohomology.H2 G (ZMod p) ≃+ continuousZModDual p (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)

H²(G, 𝔽_p) is the continuous 𝔽_p-dual of R ⧸ Rᵖ[R, F]. Let F be the free pro-p group on X, let R ≤ Φ(F) be a closed normal subgroup, and let G ≅ F ⧸ R be a group acting trivially on 𝔽_p, as does F. The inverse of the transgression H¹(R, 𝔽_p)^F → H²(F ⧸ R, 𝔽_p), followed by the identification of the invariant classes with the characters of R ⧸ Rᵖ[R, F] (TauCeti.ContCohomology.H1ConjInvariantsEquivOfSmulEqSelf), identifies H²(G, 𝔽_p) with the continuous 𝔽_p-dual of R ⧸ Rᵖ[R, F]. Its defining equation is TauCeti.h2DualEquiv_h2QuotientEquiv_transgression.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.h2DualEquiv_h2QuotientEquiv_transgression {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hRc : IsClosed ↑R) (hR : R ≤ proPFrattini p (freeProP p X)) (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (y : ↥(ContCohomology.H1ConjInvariants (freeProP p X) (ZMod p) R)) : (h2DualEquiv hRc hR e htrivF htriv) ((h2QuotientEquiv e htrivF htriv) ((ContCohomology.transgression (freeProP p X) (ZMod p) R hRc) y)) = (ContCohomology.H1ConjInvariantsEquivOfSmulEqSelf htrivF p hRc ⋯) y

The dual equivalence inverts the transgression: the class of H²(G, 𝔽_p) transgressed from an invariant class y ∈ H¹(R, 𝔽_p)^F is sent to the character of R ⧸ Rᵖ[R, F] that y represents.

theorem TauCeti.finite_H2_iff_of_le_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hRc : IsClosed ↑R) (hR : R ≤ proPFrattini p (freeProP p X)) (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Finite (ContCohomology.H2 G (ZMod p)) ↔ IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)

Finiteness of H²(G, 𝔽_p) for a quotient of a free pro-p group. Let F be the free pro-p group on X, let R ≤ Φ(F) be a closed normal subgroup, and let G ≅ F ⧸ R be a group acting trivially on 𝔽_p, as does F. Then H²(G, 𝔽_p) is finite exactly when R ⧸ Rᵖ[R, F] is topologically finitely generated.

theorem TauCeti.natCard_H2_of_le_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hRc : IsClosed ↑R) (hR : R ≤ proPFrattini p (freeProP p X)) (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) : Nat.card (ContCohomology.H2 G (ZMod p)) = p ^ topologicalGeneratorRankNat (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) h

H²(G, 𝔽_p) counts the generators of R ⧸ Rᵖ[R, F] for a quotient of a free pro-p group. Let F be the free pro-p group on X, let R ≤ Φ(F) be a closed normal subgroup with R ⧸ Rᵖ[R, F] topologically finitely generated, and let G ≅ F ⧸ R be a group acting trivially on 𝔽_p, as does F. Then H²(G, 𝔽_p) has p ^ d(R ⧸ Rᵖ[R, F]) elements, where d is the topological generator rank.

theorem TauCeti.lift_rank_H2_of_le_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hRc : IsClosed ↑R) (hR : R ≤ proPFrattini p (freeProP p X)) (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Cardinal.lift.{u, v} (Module.rank (ZMod p) (ContCohomology.H2 G (ZMod p))) = Cardinal.lift.{v, u} (topologicalGeneratorRank (↥R ⧸ (pLowerCentralStep p R).subgroupOf R))

dim H²(G, 𝔽_p) is the rank of R ⧸ Rᵖ[R, F] for a quotient of a free pro-p group. Let F be the free pro-p group on X, let R ≤ Φ(F) be a closed normal subgroup, and let G ≅ F ⧸ R be a group acting trivially on 𝔽_p, as does F. Then the dimension of H²(G, 𝔽_p) over 𝔽_p is the topological generator rank of R ⧸ Rᵖ[R, F]. No finiteness hypothesis is needed, and the statement is an identity of cardinals; TauCeti.finrank_H2_of_le_proPFrattini is the finite case.

theorem TauCeti.finrank_H2_of_le_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hRc : IsClosed ↑R) (hR : R ≤ proPFrattini p (freeProP p X)) (e : freeProP p X ⧸ R ≃ₜ* G) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) : Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p)) = topologicalGeneratorRankNat (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) h

dim H²(G, 𝔽_p) counts the generators of R ⧸ Rᵖ[R, F] for a quotient of a free pro-p group. Let F be the free pro-p group on X, let R ≤ Φ(F) be a closed normal subgroup with R ⧸ Rᵖ[R, F] topologically finitely generated, and let G ≅ F ⧸ R be a group acting trivially on 𝔽_p, as does F. Then H²(G, 𝔽_p) has dimension d(R ⧸ Rᵖ[R, F]) over 𝔽_p, where d is the topological generator rank. This is the finite case of TauCeti.lift_rank_H2_of_le_proPFrattini.

theorem TauCeti.natCard_H2_quotient_mul_pow_card_of_isClosed {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] (hRc : IsClosed ↑R) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) : Nat.card (ContCohomology.H2 (freeProP p X ⧸ R) ↥(FixedPoints.addSubgroup (↥R) (ZMod p))) * p ^ Nat.card X = p ^ (topologicalGeneratorRankNat (freeProP p X ⧸ R) ⋯ + topologicalGeneratorRankNat (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) h)

The five-term count for a quotient of a free pro-p group of finite rank. Let F be the free pro-p group on a finite type X, acting trivially on 𝔽_p, and let R be a closed normal subgroup with R ⧸ Rᵖ[R, F] topologically finitely generated. Then |H²(F ⧸ R, 𝔽_p ^ R)| · p ^ #X = p ^ (d(F ⧸ R) + d(R ⧸ Rᵖ[R, F])): the five-term sequence of 1 → R → F → F ⧸ R → 1 has |H¹(F, 𝔽_p)| = p ^ #X, |H¹(F ⧸ R, 𝔽_p ^ R)| = p ^ d(F ⧸ R), |H¹(R, 𝔽_p)^F| = p ^ d(R ⧸ Rᵖ[R, F]) and H²(F, 𝔽_p) = 0.

theorem TauCeti.finite_H2_of_isClosed {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] (hRc : IsClosed ↑R) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : freeProP p X ⧸ R ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) : Finite (ContCohomology.H2 G (ZMod p))

H²(G, 𝔽_p) is finite when the relation subgroup is finitely normally generated. Let F be the free pro-p group on any type X, let R be a closed normal subgroup with R ⧸ Rᵖ[R, F] topologically finitely generated, and let G ≅ F ⧸ R act trivially on 𝔽_p, as does F. Then H²(G, 𝔽_p) is finite: it is the image of the finite H¹(R, 𝔽_p)^F under the transgression, which is surjective since H²(F, 𝔽_p) = 0.

theorem TauCeti.natCard_H2_mul_pow_card_of_isClosed {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] (hRc : IsClosed ↑R) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : freeProP p X ⧸ R ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) : Nat.card (ContCohomology.H2 G (ZMod p)) * p ^ Nat.card X = p ^ (topologicalGeneratorRankNat G ⋯ + topologicalGeneratorRankNat (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) h)

The five-term count for a group presented by a free pro-p group of finite rank. Let F be the free pro-p group on a finite type X, let R be a closed normal subgroup with R ⧸ Rᵖ[R, F] topologically finitely generated, and let G ≅ F ⧸ R act trivially on 𝔽_p, as does F. Then |H²(G, 𝔽_p)| · p ^ #X = p ^ (d(G) + d(R ⧸ Rᵖ[R, F])), where G is topologically finitely generated as a quotient of F.

theorem TauCeti.card_add_finrank_H2_of_isClosed {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [DistribMulAction (freeProP p X) (ZMod p)] [ContinuousSMul (freeProP p X) (ZMod p)] {R : Subgroup (freeProP p X)} [R.Normal] (hRc : IsClosed ↑R) (htrivF : ∀ (g : freeProP p X) (m : ZMod p), g • m = m) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : freeProP p X ⧸ R ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) : Nat.card X + Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p)) = topologicalGeneratorRankNat G ⋯ + topologicalGeneratorRankNat (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) h

The generator, relation and normal-generator counts of a presentation. Let F be the free pro-p group on a finite type X, let R be a closed normal subgroup with R ⧸ Rᵖ[R, F] topologically finitely generated, and let G ≅ F ⧸ R act trivially on 𝔽_p, as does F. Then

#X + dim H²(G, 𝔽_p) = d(G) + d(R ⧸ Rᵖ[R, F]),

where d(R ⧸ Rᵖ[R, F]) is the least number of generators of R as a closed normal subgroup of F, and G is topologically finitely generated as a quotient of F. No minimality of the presentation is assumed.

theorem TauCeti.presentedProP.exists_finset_card_eq_image_val_eq {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} (hrels : rels.Finite) : ∃ (s : Finset ↥(Subgroup.normalClosure rels).topologicalClosure), s.card = Nat.card ↑rels ∧ Subtype.val '' ↑s = rels

A finite set of relators is a finset of its closed normal closure R in the free pro-p group, with as many elements: rels is the image under Subtype.val of a finset of R of Nat.card rels elements.

theorem TauCeti.presentedProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_of_finite {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {rels : Set (freeProP p X)} (hrels : rels.Finite) : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)

A finite relator set normally generates its relation subgroup finitely. For a finite set of relators rels, with closed normal closure R in the free pro-p group F, the quotient R ⧸ Rᵖ[R, F] is topologically finitely generated.

theorem TauCeti.presentedProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_le_card {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {rels : Set (freeProP p X)} (hrels : rels.Finite) : topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) ⋯ ≤ Nat.card ↑rels

The relators bound the least number of normal generators. For a finite set of relators rels with closed normal closure R in the free pro-p group F, the topological generator rank of R ⧸ Rᵖ[R, F], which is the least number of generators of R as a closed normal subgroup, is at most the number of relators.

theorem TauCeti.presentedProP.card_add_finrank_H2 {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] {rels : Set (freeProP p X)} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) : Nat.card X + Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p)) = topologicalGeneratorRankNat G ⋯ + topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) h

The generator, relation and normal-generator counts of a presentation. Let G ≅ ⟨X ∣ rels⟩ be a presentation, on a finite type X, of a group acting trivially on 𝔽_p, and let R be the closed normal closure of the relators, with R ⧸ Rᵖ[R, F] topologically finitely generated. Then

#X + dim H²(G, 𝔽_p) = d(G) + d(R ⧸ Rᵖ[R, F]),

where d(R ⧸ Rᵖ[R, F]) is the least number of generators of R as a closed normal subgroup of F, and G is topologically finitely generated as a group presented on a finite type. The presentation need not be minimal.

theorem TauCeti.presentedProP.finite_H2_of_finite {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {rels : Set (freeProP p X)} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (hrels : rels.Finite) : Finite (ContCohomology.H2 G (ZMod p))

H²(G, 𝔽_p) is finite for finitely many relators. Let G ≅ ⟨X ∣ rels⟩ be a presentation, on any type X, by finitely many relators, of a group acting trivially on 𝔽_p. Then H²(G, 𝔽_p) is finite.

theorem TauCeti.presentedProP.card_add_finrank_cohomFp_two {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] {rels : Set (freeProP p X)} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (e : presentedProP p X rels ≃ₜ* G) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) : Nat.card X + Module.finrank (ZMod p) ↑(cohomFp p G 2).toModuleCat = topologicalGeneratorRankNat G ⋯ + topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) h

The generator, relation and normal-generator counts of a presentation, on the canonical carrier. Let G ≅ ⟨X ∣ rels⟩ be a presentation on a finite type X, and let R be the closed normal closure of the relators, with R ⧸ Rᵖ[R, F] topologically finitely generated. Then

#X + dim H²(G, 𝔽_p) = d(G) + d(R ⧸ Rᵖ[R, F]),

where d(R ⧸ Rᵖ[R, F]) is the least number of generators of R as a closed normal subgroup of F, and G is topologically finitely generated as a group presented on a finite type. The presentation need not be minimal.

theorem TauCeti.presentedProP.module_finite_cohomFp_two_of_finite {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {rels : Set (freeProP p X)} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (e : presentedProP p X rels ≃ₜ* G) (hrels : rels.Finite) : Module.Finite (ZMod p) ↑(cohomFp p G 2).toModuleCat

H²(G, 𝔽_p) is finite-dimensional for finitely many relators, on any type of generators, so that the relation rank r(G) = dim_{𝔽_p} H²(G, 𝔽_p) of a group presented by finitely many relators is a natural number.

theorem TauCeti.presentedProP.finite_H2_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Finite (ContCohomology.H2 G (ZMod p)) ↔ IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)

Finiteness of H²(G, 𝔽_p) from a minimal presentation. Let G ≅ ⟨X ∣ rels⟩ be a presentation of a group acting trivially on 𝔽_p whose relators lie in the Frattini subgroup of the free pro-p group F on X, and let R be the closed normal closure of the relators. Then H²(G, 𝔽_p) is finite exactly when R ⧸ Rᵖ[R, F] is topologically finitely generated.

theorem TauCeti.presentedProP.natCard_H2 {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) : Nat.card (ContCohomology.H2 G (ZMod p)) = p ^ topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) h

H²(G, 𝔽_p) counts the relations of a minimal presentation. Let G ≅ ⟨X ∣ rels⟩ be a presentation of a group acting trivially on 𝔽_p whose relators lie in the Frattini subgroup of the free pro-p group F on X, and let R be the closed normal closure of the relators, with R ⧸ Rᵖ[R, F] topologically finitely generated. Then H²(G, 𝔽_p) has p ^ d(R ⧸ Rᵖ[R, F]) elements, where d is the topological generator rank.

theorem TauCeti.presentedProP.natCard_H2_le_pow_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) (n : ℕ) : Nat.card (ContCohomology.H2 G (ZMod p)) ≤ p ^ n ↔ ∃ (s : Finset ↥(Subgroup.normalClosure rels).topologicalClosure), s.card ≤ n ∧ (Subgroup.normalClosure (Subtype.val '' ↑s)).topologicalClosure = (Subgroup.normalClosure rels).topologicalClosure

The order of H²(G, 𝔽_p) bounds the number of relations. Let G ≅ ⟨X ∣ rels⟩ be a presentation of a group acting trivially on 𝔽_p whose relators lie in the Frattini subgroup of the free pro-p group F on X, and let R be the closed normal closure of the relators, with R ⧸ Rᵖ[R, F] topologically finitely generated. Then H²(G, 𝔽_p) has at most p ^ n elements exactly when R is generated as a closed normal subgroup of F by at most n elements.

theorem TauCeti.presentedProP.lift_rank_H2 {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : Cardinal.lift.{u, v} (Module.rank (ZMod p) (ContCohomology.H2 G (ZMod p))) = Cardinal.lift.{v, u} (topologicalGeneratorRank (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure))

The relation rank of a pro-p group is the dimension of H²(G, 𝔽_p), cardinal form. Let G ≅ ⟨X ∣ rels⟩ be a presentation of a group acting trivially on 𝔽_p whose relators lie in the Frattini subgroup of the free pro-p group F on X, and let R be the closed normal closure of the relators. Then the dimension of H²(G, 𝔽_p) over 𝔽_p is d(R ⧸ Rᵖ[R, F]), the relation rank of G, as an identity of cardinals and with no finiteness hypothesis: a group with infinitely many relations has an H²(G, 𝔽_p) of infinite dimension. TauCeti.presentedProP.finrank_H2 is the finite case.

theorem TauCeti.presentedProP.finrank_H2 {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) : Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p)) = topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) h

The relation rank of a pro-p group is the dimension of H²(G, 𝔽_p). Let G ≅ ⟨X ∣ rels⟩ be a presentation of a group acting trivially on 𝔽_p whose relators lie in the Frattini subgroup of the free pro-p group F on X, and let R be the closed normal closure of the relators, with R ⧸ Rᵖ[R, F] topologically finitely generated. Then H²(G, 𝔽_p) has dimension d(R ⧸ Rᵖ[R, F]) over 𝔽_p, the least number of generators of R as a closed normal subgroup of F. This is the finite case of TauCeti.presentedProP.lift_rank_H2.

theorem TauCeti.presentedProP.finrank_H2_le_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (rels : Set (freeProP p X)) (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (e : presentedProP p X rels ≃ₜ* G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) (n : ℕ) : Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p)) ≤ n ↔ ∃ (s : Finset ↥(Subgroup.normalClosure rels).topologicalClosure), s.card ≤ n ∧ (Subgroup.normalClosure (Subtype.val '' ↑s)).topologicalClosure = (Subgroup.normalClosure rels).topologicalClosure

The dimension of H²(G, 𝔽_p) bounds the number of relations. Let G ≅ ⟨X ∣ rels⟩ be a presentation of a group acting trivially on 𝔽_p whose relators lie in the Frattini subgroup of the free pro-p group F on X, and let R be the closed normal closure of the relators, with R ⧸ Rᵖ[R, F] topologically finitely generated. Then H²(G, 𝔽_p) has dimension at most n over 𝔽_p exactly when R is generated as a closed normal subgroup of F by at most n elements.

theorem TauCeti.presentedProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {Y : Type w} (rels : Set (freeProP p X)) (rels' : Set (freeProP p Y)) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) (hrels' : rels' ⊆ ↑(proPFrattini p (freeProP p Y))) (e : presentedProP p X rels ≃ₜ* G) (e' : presentedProP p Y rels' ≃ₜ* G) : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) ↔ IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels').topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels').topologicalClosure).subgroupOf (Subgroup.normalClosure rels').topologicalClosure)

Presentation independence of the finiteness of the relation rank. For two minimal presentations G ≅ ⟨X ∣ rels⟩ and G ≅ ⟨Y ∣ rels'⟩ of the same group, with relators in the Frattini subgroups of the free pro-p groups F on X and F' on Y and relation subgroups R and R', the quotient R ⧸ Rᵖ[R, F] is topologically finitely generated exactly when R' ⧸ R'ᵖ[R', F'] is: both mean that H²(G, 𝔽_p) is finite.

theorem TauCeti.presentedProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_eq {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {Y : Type w} (rels : Set (freeProP p X)) (rels' : Set (freeProP p Y)) {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) (hrels' : rels' ⊆ ↑(proPFrattini p (freeProP p Y))) (e : presentedProP p X rels ≃ₜ* G) (e' : presentedProP p Y rels' ≃ₜ* G) (h : IsTopologicallyFinitelyGenerated (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure)) : topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels).topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels).topologicalClosure).subgroupOf (Subgroup.normalClosure rels).topologicalClosure) h = topologicalGeneratorRankNat (↥(Subgroup.normalClosure rels').topologicalClosure ⧸ (pLowerCentralStep p (Subgroup.normalClosure rels').topologicalClosure).subgroupOf (Subgroup.normalClosure rels').topologicalClosure) ⋯

Presentation independence of the relation rank. For two minimal presentations G ≅ ⟨X ∣ rels⟩ and G ≅ ⟨Y ∣ rels'⟩ of the same group, with relators in the Frattini subgroups of the free pro-p groups F on X and F' on Y and relation subgroups R and R', the counts d(R ⧸ Rᵖ[R, F]) and d(R' ⧸ R'ᵖ[R', F']) agree: both are the exponent of the order p ^ r of H²(G, 𝔽_p). Finite generation of R' ⧸ R'ᵖ[R', F'] is supplied by TauCeti.presentedProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_iff.