The two-term Euler formula for pro-p groups

Let G be a topologically finitely generated pro-p group whose second cohomology vanishes on the trivial modules of order p; a group with cd_p G ≤ 1 is one, and so is a free pro-p group of finite rank. For a finite discrete p-primary G-module M the two-term Euler characteristic |H⁰(G, M)| / |H¹(G, M)| is multiplicative in the order of M:

|H¹(G, M)| * |M| = |H⁰(G, M)| * |M| ^ d(G),

where d(G) is the topological generator rank. For M = 𝔽_p this is |H¹(G, 𝔽_p)| = p ^ d(G), the count of generators through the continuous dual (TauCeti.IsProP.natCard_H1_of_natCard_eq); the general case follows by induction on |M| along the trivial filtration of TauCeti.exists_addSubgroup_natCard_eq_invariant_of_isProP, each step being the six-term exact sequence 0 → H⁰(N) → H⁰(M) → H⁰(M ⧸ N) → H¹(N) → H¹(M) → H¹(M ⧸ N) → H²(N) = 0 of the explicit long exact sequence, read through the alternating identity AddMonoidHom.card_mul_card_mul_card_of_exact.

Applied to the permutation module Coind_U^G 𝔽_p of an open subgroup U, which has order p ^ [G : U], Shapiro's lemma turns the identity into the two-term Euler formula

d(U) + [G : U] = 1 + [G : U] * d(G),   that is   1 - d(U) = [G : U] * (1 - d(G)) in ℤ,

the case cd_p G ≤ 1 of the Euler characteristic formula χ(U) = [G : U] * χ(G). For a free pro-p group of finite rank it becomes the Schreier index formula for the generator rank of an open subgroup, TauCeti.Topology.Algebra.Group.Profinite.Free.OpenSubgroup.

Main results

• TauCeti.IsProP.natCard_H1_of_natCard_eq: |H¹(G, A)| = p ^ d(G) for a trivial module A of order p.
• TauCeti.IsProP.natCard_H1_mul_natCard: the multiplicative Euler identity |H¹(G, M)| * |M| = |H⁰(G, M)| * |M| ^ d(G).
• TauCeti.IsProP.topologicalGeneratorRankNat_add_index and TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_eq: the two-term Euler formula for an open subgroup, in ℕ and in ℤ.
• TauCeti.CohomologicalDimensionLE.natCard_H1_mul_natCard, TauCeti.CohomologicalDimensionLE.topologicalGeneratorRankNat_add_index: the same under the hypothesis cd_p G ≤ 1.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §4.1 and §4.2.
• H. Koch, Galois Theory of p-Extensions, §5.4 and Example 6.3.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.3.2) and Ch. III §9.

theorem TauCeti.IsProP.natCard_H1_of_natCard_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) {A : Type v} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] (hA : Nat.card A = p) (htriv : ∀ (g : G) (a : A), g • a = a) : Nat.card (ContCohomology.H1 G A) = p ^ topologicalGeneratorRankNat G hfg

H¹ with trivial coefficients of order p counts generators. For a topologically finitely generated profinite pro-p group G and a discrete module A of order p with trivial action, H¹(G, A) has p ^ d(G) elements: it is the group of continuous characters G → A, and the additive group A is isomorphic to ZMod p.

theorem TauCeti.IsProP.natCard_H1_mul_natCard {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (h2 : ∀ (A : Type v) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [inst_4 : ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton (ContCohomology.H2 G A)) (M : Type v) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : IsPPrimaryTorsion p M) : Nat.card (ContCohomology.H1 G M) * Nat.card M = Nat.card ↥(ContCohomology.H0 G M) * Nat.card M ^ topologicalGeneratorRankNat G hfg

The Euler characteristic of a finite p-primary module is multiplicative in its order. Let G be a topologically finitely generated profinite pro-p group whose explicit H² vanishes on the discrete modules of order p with trivial action. Then for every finite discrete p-primary G-module M,

|H¹(G, M)| * |M| = |H⁰(G, M)| * |M| ^ d(G).

For M of order p with trivial action this is |H¹(G, M)| = p ^ d(G); in general it is the additivity of the Euler characteristic |H⁰| / |H¹| along the trivial filtration of M.

theorem TauCeti.IsProP.topologicalGeneratorRankNat_add_index {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (h2 : ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [inst_4 : ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton (ContCohomology.H2 G A)) (U : OpenSubgroup G) : topologicalGeneratorRankNat ↥↑U ⋯ + (↑U).index = 1 + (↑U).index * topologicalGeneratorRankNat G hfg

The two-term Euler formula. Let G be a topologically finitely generated profinite pro-p group whose explicit H² vanishes on the discrete modules of order p with trivial action, and let U be an open subgroup. Then d(U) + [G : U] = 1 + [G : U] * d(G), the natural-number form of 1 - d(U) = [G : U] * (1 - d(G)).

The proof applies TauCeti.IsProP.natCard_H1_mul_natCard to the permutation module Coind_U^G 𝔽_p, of order p ^ [G : U], and reads both sides through Shapiro's lemma.

theorem TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (h2 : ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [inst_4 : ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton (ContCohomology.H2 G A)) (U : OpenSubgroup G) : 1 - ↑(topologicalGeneratorRankNat ↥↑U ⋯) = ↑(↑U).index * (1 - ↑(topologicalGeneratorRankNat G hfg))

The two-term Euler formula, in ℤ. Under the hypotheses of TauCeti.IsProP.topologicalGeneratorRankNat_add_index, 1 - d(U) = [G : U] * (1 - d(G)).

theorem TauCeti.CohomologicalDimensionLE.natCard_H1_mul_natCard {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hcd : CohomologicalDimensionLE p G 1) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : IsPPrimaryTorsion p M) : Nat.card (ContCohomology.H1 G M) * Nat.card M = Nat.card ↥(ContCohomology.H0 G M) * Nat.card M ^ topologicalGeneratorRankNat G hfg

The Euler characteristic of a finite p-primary module under cd_p G ≤ 1. For a topologically finitely generated profinite pro-p group G with cd_p G ≤ 1 and a finite discrete p-primary G-module M, |H¹(G, M)| * |M| = |H⁰(G, M)| * |M| ^ d(G).

theorem TauCeti.CohomologicalDimensionLE.topologicalGeneratorRankNat_add_index {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hcd : CohomologicalDimensionLE p G 1) (U : OpenSubgroup G) : topologicalGeneratorRankNat ↥↑U ⋯ + (↑U).index = 1 + (↑U).index * topologicalGeneratorRankNat G hfg

The two-term Euler formula under cd_p G ≤ 1. For a topologically finitely generated profinite pro-p group G with cd_p G ≤ 1 and an open subgroup U, d(U) + [G : U] = 1 + [G : U] * d(G).

theorem TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hcd : CohomologicalDimensionLE p G 1) (U : OpenSubgroup G) : 1 - ↑(topologicalGeneratorRankNat ↥↑U ⋯) = ↑(↑U).index * (1 - ↑(topologicalGeneratorRankNat G hfg))

The two-term Euler formula under cd_p G ≤ 1, in ℤ: 1 - d(U) = [G : U] * (1 - d(G)) for an open subgroup U of a topologically finitely generated profinite pro-p group with cd_p G ≤ 1.