The three-term Euler formula for pro-p groups

Let G be a topologically finitely generated pro-p group whose third cohomology vanishes on the trivial modules of order p; a group with cd_p G ≤ 2 is one. For a finite discrete p-primary G-module M of order p ^ k, the three-term Euler characteristic |H⁰| * |H²| / |H¹| is multiplicative in the order of M:

|H⁰(G, M)| * |H²(G, M)| * p ^ (k * d(G)) = |H¹(G, M)| * p ^ k * |H²(G, 𝔽_p)| ^ k,

where d(G) is the topological generator rank and 𝔽_p carries the trivial action. For M = 𝔽_p the identity is a tautology, given that |H¹(G, 𝔽_p)| = p ^ d(G); the general case follows by induction on k along the trivial filtration of TauCeti.exists_addSubgroup_natCard_eq_invariant_of_isProP, each step being the nine-term exact sequence

0 → H⁰(N) → H⁰(M) → H⁰(M ⧸ N) → H¹(N) → H¹(M) → H¹(M ⧸ N) → H²(N) → H²(M) → H²(M ⧸ N) → 0

of the explicit long exact sequence, exact on the right because H³(G, N) = 0, and read through the alternating identity AddMonoidHom.card_mul_card_mul_card_mul_card_mul_card_of_exact. The cancellation in the induction step uses that H¹(G, M ⧸ N) is finite, which holds over any topologically finitely generated group.

Applied to the permutation module Coind_U^G 𝔽_p of an open subgroup U, of order p ^ [G : U], Shapiro's lemma in degrees 0, 1 and 2 turns the identity into the three-term Euler formula: if H²(G, 𝔽_p) is finite then so is H²(U, 𝔽_p) ≅ H²(G, Coind_U^G 𝔽_p) (TauCeti.IsProP.finite_cohomFp_openSubgroup, by the finiteness dévissage, with no hypothesis on H³), and in ℤ

1 - d(U) + dim H²(U, 𝔽_p) = [G : U] * (1 - d(G) + dim H²(G, 𝔽_p)).

Here 1 = dim H⁰ and d = dim H¹ for the trivial module 𝔽_p, so this is the identity χ(U) = [G : U] * χ(G) for the truncated Euler characteristic χ = Σ_{i ≤ 2} (-1)^i dim Hⁱ(-, 𝔽_p). When H²(G, 𝔽_p) and H²(U, 𝔽_p) are both one-dimensional, as for a Demushkin group G and an open subgroup U that is again Demushkin, it becomes the rank formula d(U) - 2 = [G : U] * (d(G) - 2).

Main results

• TauCeti.IsProP.natCard_H0_mul_natCard_H2_mul_pow: the multiplicative three-term Euler identity for a finite p-primary module of order p ^ k.
• TauCeti.IsProP.natCard_H2_openSubgroup_mul_pow: the identity for Coind_U^G 𝔽_p, read through Shapiro's lemma as an identity between |H²(U, 𝔽_p)|, d(U), [G : U], d(G) and |H²(G, 𝔽_p)|.
• TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_add_finrank_H2: the three-term Euler formula in ℤ.
• TauCeti.CohomologicalDimensionLE.natCard_H0_mul_natCard_H2_mul_pow, TauCeti.CohomologicalDimensionLE.natCard_H2_openSubgroup_mul_pow, TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_add_finrank_H2: the same under the hypothesis cd_p G ≤ 2.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §4.1.
• H. Koch, Galois Theory of p-Extensions, §5.4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. III §3.

theorem TauCeti.IsProP.natCard_H0_mul_natCard_H2_mul_pow {p : ℕ} [hp : 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)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x) (h3 : ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ G A)).toModuleCat) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] {k : ℕ} (hk : Nat.card M = p ^ k) : Nat.card ↥(ContCohomology.H0 G M) * Nat.card (ContCohomology.H2 G M) * p ^ (k * topologicalGeneratorRankNat G hfg) = Nat.card (ContCohomology.H1 G M) * p ^ k * Nat.card (ContCohomology.H2 G (ZMod p)) ^ k

The three-term 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 canonical H³ vanishes on the discrete modules of order p with trivial action, and let 𝔽_p carry the trivial action. Then for every finite discrete G-module M of order p ^ k,

|H⁰(G, M)| * |H²(G, M)| * p ^ (k * d(G)) = |H¹(G, M)| * p ^ k * |H²(G, 𝔽_p)| ^ k.

For M = 𝔽_p this is |H¹(G, 𝔽_p)| = p ^ d(G); in general it is the additivity of the Euler characteristic |H⁰| * |H²| / |H¹| along the trivial filtration of M. The identity holds for Nat.card with no finiteness hypothesis on H²(G, 𝔽_p), an infinite H² contributing the factor 0 to both sides.

theorem TauCeti.IsProP.natCard_H2_openSubgroup_mul_pow {p : ℕ} [hp : 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)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x) (h3 : ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ G A)).toModuleCat) (U : OpenSubgroup G) : p * Nat.card (ContCohomology.H2 (↥↑U) (ZMod p)) * p ^ ((↑U).index * topologicalGeneratorRankNat G hfg) = p ^ topologicalGeneratorRankNat ↥↑U ⋯ * p ^ (↑U).index * Nat.card (ContCohomology.H2 G (ZMod p)) ^ (↑U).index

The three-term Euler identity for the permutation module of an open subgroup, read through Shapiro's lemma. Let G be a topologically finitely generated profinite pro-p group whose canonical H³ vanishes on the discrete modules of order p with trivial action, let 𝔽_p carry the trivial action, and let U be an open subgroup. Then

p * |H²(U, 𝔽_p)| * p ^ ([G : U] * d(G)) = p ^ d(U) * p ^ [G : U] * |H²(G, 𝔽_p)| ^ [G : U].

This is TauCeti.IsProP.natCard_H0_mul_natCard_H2_mul_pow for Coind_U^G 𝔽_p, of order p ^ [G : U], with Hⁱ(G, Coind_U^G 𝔽_p) ≅ Hⁱ(U, 𝔽_p) for i = 0, 1, 2.

theorem TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_add_finrank_H2 {p : ℕ} [hp : 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)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x) (h3 : ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ G A)).toModuleCat) (U : OpenSubgroup G) [Finite (ContCohomology.H2 G (ZMod p))] : 1 - ↑(topologicalGeneratorRankNat ↥↑U ⋯) + ↑(Module.finrank (ZMod p) (ContCohomology.H2 (↥↑U) (ZMod p))) = ↑(↑U).index * (1 - ↑(topologicalGeneratorRankNat G hfg) + ↑(Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p))))

The three-term Euler formula. Let G be a topologically finitely generated profinite pro-p group whose canonical H³ vanishes on the discrete modules of order p with trivial action, with H²(G, 𝔽_p) finite for the trivial action on 𝔽_p, and let U be an open subgroup. Then, in ℤ,

1 - d(U) + dim H²(U, 𝔽_p) = [G : U] * (1 - d(G) + dim H²(G, 𝔽_p)),

the identity χ(U) = [G : U] * χ(G) for χ = dim H⁰ - dim H¹ + dim H² with 𝔽_p coefficients, since dim H⁰ = 1 and dim H¹ = d for the trivial module 𝔽_p. The space H²(U, 𝔽_p) is finite by TauCeti.IsProP.finite_cohomFp_openSubgroup.

theorem TauCeti.CohomologicalDimensionLE.natCard_H0_mul_natCard_H2_mul_pow {p : ℕ} [hp : 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)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x) (hcd : CohomologicalDimensionLE p G 2) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] {k : ℕ} (hk : Nat.card M = p ^ k) : Nat.card ↥(ContCohomology.H0 G M) * Nat.card (ContCohomology.H2 G M) * p ^ (k * topologicalGeneratorRankNat G hfg) = Nat.card (ContCohomology.H1 G M) * p ^ k * Nat.card (ContCohomology.H2 G (ZMod p)) ^ k

The three-term Euler identity under cd_p G ≤ 2. For a topologically finitely generated profinite pro-p group G with cd_p G ≤ 2, the trivial action on 𝔽_p, and a finite discrete G-module M of order p ^ k, |H⁰(G, M)| * |H²(G, M)| * p ^ (k * d(G)) = |H¹(G, M)| * p ^ k * |H²(G, 𝔽_p)| ^ k.

theorem TauCeti.CohomologicalDimensionLE.natCard_H2_openSubgroup_mul_pow {p : ℕ} [hp : 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)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x) (hcd : CohomologicalDimensionLE p G 2) (U : OpenSubgroup G) : p * Nat.card (ContCohomology.H2 (↥↑U) (ZMod p)) * p ^ ((↑U).index * topologicalGeneratorRankNat G hfg) = p ^ topologicalGeneratorRankNat ↥↑U ⋯ * p ^ (↑U).index * Nat.card (ContCohomology.H2 G (ZMod p)) ^ (↑U).index

The three-term Euler identity for an open subgroup under cd_p G ≤ 2. For a topologically finitely generated profinite pro-p group G with cd_p G ≤ 2, the trivial action on 𝔽_p, and an open subgroup U, p * |H²(U, 𝔽_p)| * p ^ ([G : U] * d(G)) = p ^ d(U) * p ^ [G : U] * |H²(G, 𝔽_p)| ^ [G : U].

theorem TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_add_finrank_H2 {p : ℕ} [hp : 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)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x) (hcd : CohomologicalDimensionLE p G 2) (U : OpenSubgroup G) [Finite (ContCohomology.H2 G (ZMod p))] : 1 - ↑(topologicalGeneratorRankNat ↥↑U ⋯) + ↑(Module.finrank (ZMod p) (ContCohomology.H2 (↥↑U) (ZMod p))) = ↑(↑U).index * (1 - ↑(topologicalGeneratorRankNat G hfg) + ↑(Module.finrank (ZMod p) (ContCohomology.H2 G (ZMod p))))

The three-term Euler formula under cd_p G ≤ 2. For a topologically finitely generated profinite pro-p group G with cd_p G ≤ 2 and H²(G, 𝔽_p) finite, and an open subgroup U, in ℤ: 1 - d(U) + dim H²(U, 𝔽_p) = [G : U] * (1 - d(G) + dim H²(G, 𝔽_p)).