Generator rank and relation rank of an elementary abelian pro-p group

Let G be a finite elementary abelian p-group, that is, a topologically finitely generated profinite group whose pro-p Frattini subgroup Φ(G) is trivial (such a group is automatically pro-p); the model is (ℤ/p)^X = X → Multiplicative (ZMod p) for a finite type X. Its topological generator rank d = d(G) satisfies |G| = p ^ d, and its second cohomology with trivial coefficients 𝔽_p has order p ^ (d (d + 1) / 2): the relation rank of G is d (d + 1) / 2. In the model, d((ℤ/p)^X) = #X and r((ℤ/p)^X) = #X (#X + 1) / 2.

The last section drops the finiteness of the index type: the product (ℤ/p)^ι of copies of ℤ/p indexed by an arbitrary type ι has topological generator rank #ι, as a cardinal, so it is topologically finitely generated exactly when ι is finite, and ∏_{i ∈ ℕ} ℤ/p has rank ℵ₀. This is the basic example of an abelian pro-p group of infinite rank: the pro-p Frattini subgroup of (ℤ/p)^ι is trivial for every ι, so for infinite ι the Frattini quotient is the whole, infinite, group, and no finite set generates a dense subgroup.

The count is read off a minimal presentation. A minimal presentation G ≅ F ⧸ R by the free pro-p group F of rank d has R = Φ(F) (TauCeti.presentedProP.topologicalClosure_normalClosure_eq_proPFrattini), which is the first term λ_1(F) of the lower p-series, so R ⧸ Rᵖ[R, F] = λ_1(F) ⧸ λ_2(F) = gr_1(F) is the degree-one graded piece, of order p ^ (d + (d choose 2)) (TauCeti.freeProP.natCard_gradedPiece_one). Since H²(G, 𝔽_p) has p ^ d(R ⧸ Rᵖ[R, F]) elements (TauCeti.presentedProP.natCard_H2) and R ⧸ Rᵖ[R, F] is elementary abelian, its rank is its 𝔽_p-dimension d + (d choose 2) = d (d + 1) / 2.

This is the value against which the normalisation of H² is checked: an H² counting d choose 2 or d ^ 2 classes for (ℤ/p)^d would be wrong. The counting statements are about the order of the explicit continuous cohomology H2 G (ZMod p), with the action of G on 𝔽_p carried as an instance as in TauCeti.Topology.Algebra.Group.Profinite.ProP.Relation.Rank; no triviality hypothesis is needed, since G is pro-p and a pro-p group can only act trivially on 𝔽_p (TauCeti.IsProP.smul_zmod_eq_self). The count is then read as the 𝔽_p-dimension of the continuous cohomology cohomFp p G 2 with trivial coefficients, through TauCeti.cohomFpLinearEquivH2.

Main results

• TauCeti.natCard_H2_of_proPFrattini_eq_bot: for a topologically finitely generated profinite group G with Φ(G) = 1, H²(G, 𝔽_p) has p ^ (d(G) (d(G) + 1) / 2) elements; TauCeti.finite_H2_of_proPFrattini_eq_bot records its finiteness, and TauCeti.finrank_cohomFp_two_of_proPFrattini_eq_bot reads the count as dim H²(G, 𝔽_p) = d(G) (d(G) + 1) / 2.
• TauCeti.topologicalGeneratorRankNat_pi_multiplicative_zmod: d((ℤ/p)^X) = #X for finite X; TauCeti.topologicalGeneratorRank_pi_multiplicative_zmod: d((ℤ/p)^ι) = #ι as cardinals for an arbitrary index type ι, with the consequences TauCeti.isTopologicallyFinitelyGenerated_pi_multiplicative_zmod_iff and TauCeti.topologicalGeneratorRank_nat_pi_multiplicative_zmod, the example d(∏_{i ∈ ℕ} ℤ/p) = ℵ₀.
• TauCeti.natCard_H2_pi_multiplicative_zmod: H²((ℤ/p)^X, 𝔽_p) has p ^ (#X (#X + 1) / 2) elements.
• TauCeti.proPFrattini_multiplicative_zmod_eq_bot and TauCeti.topologicalGeneratorRankNat_multiplicative_zmod: the cyclic group ℤ/p itself has trivial pro-p Frattini subgroup and d(ℤ/p) = 1.
• TauCeti.finrank_cohomFp_one_multiplicative_zmod and TauCeti.finrank_cohomFp_two_multiplicative_zmod: H¹(ℤ/p, 𝔽_p) and H²(ℤ/p, 𝔽_p) are one-dimensional.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.5).
• J.-P. Serre, Galois Cohomology, Chapter I, §4.2 and §4.3.

theorem TauCeti.natCard_H2_of_proPFrattini_eq_bot {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hfg : IsTopologicallyFinitelyGenerated G) (hΦ : proPFrattini p G = ⊥) : Nat.card (ContCohomology.H2 G (ZMod p)) = p ^ (topologicalGeneratorRankNat G hfg * (topologicalGeneratorRankNat G hfg + 1) / 2)

The relation rank of a finite elementary abelian p-group. Let G be a topologically finitely generated profinite group with trivial pro-p Frattini subgroup. Then H²(G, 𝔽_p) has p ^ (d (d + 1) / 2) elements for every continuous action of G on 𝔽_p (which is necessarily trivial), where d = d(G) is the topological generator rank: the relation rank of G is d (d + 1) / 2.

theorem TauCeti.finite_H2_of_proPFrattini_eq_bot {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hfg : IsTopologicallyFinitelyGenerated G) (hΦ : proPFrattini p G = ⊥) : Finite (ContCohomology.H2 G (ZMod p))

H²(G, 𝔽_p) is finite for a topologically finitely generated profinite group G with trivial pro-p Frattini subgroup.

theorem TauCeti.finrank_cohomFp_two_of_proPFrattini_eq_bot {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hfg : IsTopologicallyFinitelyGenerated G) (hΦ : proPFrattini p G = ⊥) : Module.finrank (ZMod p) ↑(cohomFp p G 2).toModuleCat = topologicalGeneratorRankNat G hfg * (topologicalGeneratorRankNat G hfg + 1) / 2

The relation rank of a finite elementary abelian p-group, as a dimension. Let G be a topologically finitely generated profinite group with trivial pro-p Frattini subgroup and topological generator rank d = d(G). Then H²(G, 𝔽_p) with trivial coefficients is d (d + 1) / 2-dimensional over 𝔽_p.

The example (ℤ/p)ⁿ

@[simp]

theorem TauCeti.natCard_pi_multiplicative_zmod (p : ℕ) (X : Type u) [Finite X] : Nat.card (X → Multiplicative (ZMod p)) = p ^ Nat.card X

The group (ℤ/p)^X, a product of #X copies of ℤ/p, has p ^ #X elements.

@[simp]

theorem TauCeti.proPFrattini_pi_multiplicative_zmod_eq_bot (p : ℕ) (X : Type u) [Fact (Nat.Prime p)] : proPFrattini p (X → Multiplicative (ZMod p)) = ⊥

The pro-p Frattini subgroup of (ℤ/p)^X is trivial.

@[simp]

theorem TauCeti.topologicalGeneratorRankNat_pi_multiplicative_zmod (p : ℕ) (X : Type u) [Finite X] [Fact (Nat.Prime p)] (h : IsTopologicallyFinitelyGenerated (X → Multiplicative (ZMod p))) : topologicalGeneratorRankNat (X → Multiplicative (ZMod p)) h = Nat.card X

d((ℤ/p)^X) = #X. The topological generator rank of the finite elementary abelian group (ℤ/p)^X is #X.

@[simp]

theorem TauCeti.natCard_H2_pi_multiplicative_zmod (p : ℕ) (X : Type u) [Finite X] [Fact (Nat.Prime p)] [DistribMulAction (X → Multiplicative (ZMod p)) (ZMod p)] [ContinuousSMul (X → Multiplicative (ZMod p)) (ZMod p)] : Nat.card (ContCohomology.H2 (X → Multiplicative (ZMod p)) (ZMod p)) = p ^ (Nat.card X * (Nat.card X + 1) / 2)

r((ℤ/p)^X) = #X (#X + 1) / 2. For the finite elementary abelian group (ℤ/p)^X, H²((ℤ/p)^X, 𝔽_p) has p ^ (#X (#X + 1) / 2) elements.

The example ℤ/p

@[simp]

theorem TauCeti.proPFrattini_multiplicative_zmod_eq_bot (p : ℕ) [Fact (Nat.Prime p)] : proPFrattini p (Multiplicative (ZMod p)) = ⊥

The pro-p Frattini subgroup of the cyclic group ℤ/p is trivial.

@[simp]

theorem TauCeti.topologicalGeneratorRankNat_multiplicative_zmod (p : ℕ) [Fact (Nat.Prime p)] (h : IsTopologicallyFinitelyGenerated (Multiplicative (ZMod p))) : topologicalGeneratorRankNat (Multiplicative (ZMod p)) h = 1

d(ℤ/p) = 1. The topological generator rank of the cyclic group ℤ/p is 1.

@[simp]

theorem TauCeti.finrank_cohomFp_one_multiplicative_zmod (p : ℕ) [Fact (Nat.Prime p)] : Module.finrank (ZMod p) ↑(cohomFp p (Multiplicative (ZMod p)) 1).toModuleCat = 1

H¹(ℤ/p, 𝔽_p) is one-dimensional: the cyclic group ℤ/p has topological generator rank one.

@[simp]

theorem TauCeti.finrank_cohomFp_two_multiplicative_zmod (p : ℕ) [Fact (Nat.Prime p)] : Module.finrank (ZMod p) ↑(cohomFp p (Multiplicative (ZMod p)) 2).toModuleCat = 1

H²(ℤ/p, 𝔽_p) is one-dimensional: the relation rank of the cyclic group ℤ/p is 1 · 2 / 2 = 1.

The example (ℤ/p)^ι for an arbitrary index type

theorem TauCeti.linearIndependent_ofMul_proj_pi_multiplicative_zmod (p : ℕ) [Fact (Nat.Prime p)] (ι : Type u) : LinearIndependent (ZMod p) fun (i : ι) => Additive.ofMul (ContinuousMonoidHom.proj i)

The coordinate projections of (ℤ/p)^ι are linearly independent characters. Read in the continuous 𝔽_p-dual of the product, the projections (ℤ/p)^ι → ℤ/p onto the coordinates are linearly independent over 𝔽_p.

@[simp]

theorem TauCeti.topologicalGeneratorRank_pi_multiplicative_zmod (p : ℕ) [Fact (Nat.Prime p)] (ι : Type u) : topologicalGeneratorRank (ι → Multiplicative (ZMod p)) = Cardinal.mk ι

d((ℤ/p)^ι) = #ι. The topological generator rank of the product (ℤ/p)^ι of copies of ℤ/p indexed by an arbitrary type ι is the cardinality of ι. For finite ι this is the natural-number statement TauCeti.topologicalGeneratorRankNat_pi_multiplicative_zmod.

theorem TauCeti.isTopologicallyFinitelyGenerated_pi_multiplicative_zmod_iff (p : ℕ) [Fact (Nat.Prime p)] (ι : Type u) : IsTopologicallyFinitelyGenerated (ι → Multiplicative (ZMod p)) ↔ Finite ι

The product (ℤ/p)^ι is topologically finitely generated exactly when ι is finite.

theorem TauCeti.topologicalGeneratorRank_nat_pi_multiplicative_zmod (p : ℕ) [Fact (Nat.Prime p)] : topologicalGeneratorRank (ℕ → Multiplicative (ZMod p)) = Cardinal.aleph0

d(∏_{i ∈ ℕ} ℤ/p) = ℵ₀. The countable product of copies of ℤ/p has countably infinite topological generator rank.