Dévissage of finite p-primary coefficients for pro-p groups

Let G be a pro-p group. A finite discrete p-primary G-module M is built from copies of 𝔽_p with trivial action: by the trivial-filtration theorem TauCeti.exists_addSubgroup_natCard_eq_invariant_of_isProP, every nonzero such M contains a G-stable subgroup N of order p on which G acts trivially, and M ⧸ N is again finite and p-primary, of smaller order. Hence a property of finite discrete p-primary G-modules which holds for the zero module and for the trivial modules of order p, and which passes from N and M ⧸ N to M for every such extension, holds for every M. This is the dévissage induction principle TauCeti.IsProP.finite_pPrimary_induction, the pro-p case of dévissage (NSW (3.3.2), final clause; Koch takes it as the definition of cohomological dimension for pro-p groups), and the instance of the general principle TauCeti.ContCohomology.finite_induction_of_exists_addSubgroup for the p-primary modules. The principle itself needs no topology on G beyond the pro-p hypothesis; compactness enters only through the long exact cohomology sequence in the corollaries below.

For a compact pro-p group G, two properties of the continuous cohomology Hⁿ(G, -) in a fixed degree n are run through it, using exactness of the long exact sequence at Hⁿ(G, M) (TauCeti.ContCohomology.DiscreteShortExact.longExact_exact₂), which passes a property from Hⁿ(G, N) and Hⁿ(G, M ⧸ N) to Hⁿ(G, M). If Hⁿ(G, A) vanishes for every discrete G-module A of order p with trivial action, then it vanishes for every finite discrete p-primary G-module M, whatever the action; and if Hⁿ(G, A) is finite for every such A, then Hⁿ(G, M) is finite for every such M. The test class consists of the trivial modules of order p; the file also records the vanishing statement over all finite trivial modules killed by p, that is over the finite elementary abelian p-groups with trivial action, as a corollary and as an equivalence. It does not identify the trivial modules of order p with the single module 𝔽_p.

The coefficients range over finite modules only. Passing from finite p-primary coefficients to all discrete p-primary torsion coefficients, as in the vanishing predicate TauCeti.CohomologicalDimensionLE, is a separate reduction that rests on the compatibility of continuous cohomology with filtered colimits of coefficients, and is not part of this file.

Main results

• TauCeti.IsProP.finite_pPrimary_induction: the dévissage induction principle: a property of finite discrete p-primary modules of a pro-p group holds everywhere once it holds for the zero module and the trivial modules of order p and is closed under extensions by a trivial module of order p.
• TauCeti.IsProP.subsingleton_continuousCohomology_of_forall_natCard_eq_smul_eq_self: for a compact pro-p group, vanishing of Hⁿ on the trivial modules of order p gives vanishing on every finite discrete p-primary module.
• TauCeti.IsProP.subsingleton_continuousCohomology_of_forall_smul_eq_self: the same with the finite trivial modules killed by p as test class.
• TauCeti.IsProP.forall_subsingleton_continuousCohomology_iff_forall_natCard_eq and TauCeti.IsProP.forall_subsingleton_continuousCohomology_iff: vanishing on every finite discrete p-primary module is equivalent to vanishing on either test class.
• TauCeti.IsProP.finite_continuousCohomology_of_forall_natCard_eq_smul_eq_self: for a compact pro-p group, finiteness of Hⁿ on the trivial modules of order p gives finiteness on every finite discrete p-primary module.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Proposition (3.3.2).
• J.-P. Serre, Galois Cohomology, Chapter I, §3.3 and §4.1.
• H. Koch, Galois Theory of p-Extensions, Springer (2002), Definition 5.1.

theorem TauCeti.IsProP.finite_pPrimary_induction {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (hG : IsProP p G) {motive : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : TopologicalSpace M] → [DiscreteTopology M] → [inst_3 : DistribMulAction G M] → [ContinuousSMul G M] → Prop} (zero : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [inst_4 : ContinuousSMul G M] [Subsingleton M], motive M) (prime : ∀ (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) → motive A) (extension : ∀ (A B C : 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] [inst_6 : AddCommGroup B] [inst_7 : TopologicalSpace B] [inst_8 : DiscreteTopology B] [inst_9 : DistribMulAction G B] [inst_10 : ContinuousSMul G B] [Finite B] [inst_12 : AddCommGroup C] [inst_13 : TopologicalSpace C] [inst_14 : DiscreteTopology C] [inst_15 : DistribMulAction G C] [inst_16 : ContinuousSMul G C] [Finite C] (a : ContCohomology.DiscreteShortExact G A B C), Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → IsAddPGroup p A → IsAddPGroup p B → IsAddPGroup p C → motive A → motive C → motive B) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : IsAddPGroup p M) : motive M

The dévissage induction principle for pro-p groups. Let G be a pro-p group and let motive be a property of discrete G-modules. Suppose that motive holds for the zero module and for every discrete G-module of order p with trivial action, and that motive is closed under extensions by such a module: for every short exact sequence 0 → A → B → C → 0 of finite discrete p-primary G-modules with A of order p and trivial action, motive A and motive C imply motive B. Then motive holds for every finite discrete p-primary G-module.

theorem TauCeti.IsProP.subsingleton_continuousCohomology_of_forall_natCard_eq_smul_eq_self {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) {n : ℕ} (h : ∀ (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 n (ofDiscreteModule ℤ G A)).toModuleCat) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : IsAddPGroup p M) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat

Dévissage for pro-p groups. Let G be a compact pro-p group. If Hⁿ(G, A) vanishes for every discrete G-module A of order p on which G acts trivially, then Hⁿ(G, M) vanishes for every finite discrete p-primary G-module M.

theorem TauCeti.IsProP.subsingleton_continuousCohomology_of_forall_smul_eq_self {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) {n : ℕ} (h : ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], (∀ (a : A), p • a = 0) → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G A)).toModuleCat) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : IsAddPGroup p M) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat

Dévissage for pro-p groups, elementary abelian test class. Let G be a compact pro-p group. If Hⁿ(G, A) vanishes for every finite discrete G-module A killed by p on which G acts trivially, then Hⁿ(G, M) vanishes for every finite discrete p-primary G-module M.

theorem TauCeti.IsProP.forall_subsingleton_continuousCohomology_iff_forall_natCard_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : (∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M] [Finite M], IsAddPGroup p M → Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) ↔ ∀ (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 n (ofDiscreteModule ℤ G A)).toModuleCat

Dévissage for pro-p groups, as an equivalence. For a compact pro-p group G and a degree n, the continuous cohomology Hⁿ(G, M) vanishes for every finite discrete p-primary G-module M if and only if it vanishes for every discrete G-module of order p on which G acts trivially.

theorem TauCeti.IsProP.forall_subsingleton_continuousCohomology_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : (∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M] [Finite M], IsAddPGroup p M → Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) ↔ ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], (∀ (a : A), p • a = 0) → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G A)).toModuleCat

Dévissage for pro-p groups, as an equivalence with the elementary abelian test class. For a compact pro-p group G and a degree n, the continuous cohomology Hⁿ(G, M) vanishes for every finite discrete p-primary G-module M if and only if it vanishes for every finite discrete G-module killed by p on which G acts trivially.

theorem TauCeti.IsProP.finite_continuousCohomology_of_forall_natCard_eq_smul_eq_self {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) {n : ℕ} (h : ∀ (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) → Finite ↑(continuousCohomology n (ofDiscreteModule ℤ G A)).toModuleCat) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : IsAddPGroup p M) : Finite ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat

Finiteness dévissage for pro-p groups. Let G be a compact pro-p group. If Hⁿ(G, A) is finite for every discrete G-module A of order p on which G acts trivially, then Hⁿ(G, M) is finite for every finite discrete p-primary G-module M.