The dévissage induction principle for finite discrete modules

Let G be a topological group and Q a class of discrete G-modules which is closed under equivariant surjections. Suppose that every nontrivial finite module in Q contains a subgroup P on which G acts trivially and whose order lies in a fixed set S of integers > 1. Then every finite module M in Q is built from such trivial modules by extensions: M ⧸ P is again in Q, of smaller order. Hence a property of discrete G-modules which holds for the zero module and passes along each extension 0 → P → M → M ⧸ P → 0 from M ⧸ P to M holds for every finite module in Q. This is the dévissage induction principle TauCeti.ContCohomology.finite_induction_of_exists_addSubgroup.

It is the common skeleton of two dévissages. For a pro-p group and the p-primary modules, the subgroup P of order p comes from the trivial-filtration theorem (TauCeti.IsProP.finite_pPrimary_induction). For the trivial modules killed by N, it comes from Cauchy's theorem, and has prime order dividing N (TauCeti.ContinuousCohomology.finite_continuousCohomology_of_forall_natCard_prime).

Main results

• TauCeti.ContCohomology.finite_induction_of_exists_addSubgroup: the dévissage induction principle.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Proposition (3.3.2).

theorem TauCeti.ContCohomology.finite_induction_of_exists_addSubgroup {G : Type u} [Group G] [TopologicalSpace G] {motive : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : TopologicalSpace M] → [DiscreteTopology M] → [inst_3 : DistribMulAction G M] → [ContinuousSMul G M] → Prop} (Q : (M : Type u) → [inst : AddCommGroup M] → [DistribMulAction G M] → Prop) (S : ℕ → Prop) (one_lt : ∀ (k : ℕ), S k → 1 < k) (map : ∀ (M M' : Type u) [inst : AddCommGroup M] [inst_1 : DistribMulAction G M] [inst_2 : AddCommGroup M'] [inst_3 : DistribMulAction G M'] (f : M →+[G] M'), Function.Surjective ⇑f → Q M → Q M') (exists_addSubgroup : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M] [Finite M] [Nontrivial M], Q M → ∃ (P : AddSubgroup M), S (Nat.card ↥P) ∧ ∀ (g : G), ∀ x ∈ P, g • x = x) (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) (extension : ∀ (A B C : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [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 : DiscreteShortExact G A B C), S (Nat.card A) → (∀ (g : G) (a : A), g • a = a) → Q B → Q C → motive C → motive B) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : Q M) : motive M

The dévissage induction principle. Let Q be a class of discrete G-modules closed under equivariant surjections, and S a set of natural numbers > 1. Suppose that every nontrivial finite discrete G-module in Q has an additive subgroup of order in S on which G acts trivially. Let motive be a property of discrete G-modules which holds for the zero module and is closed under extensions by such a subgroup: for every short exact sequence 0 → A → B → C → 0 of finite discrete G-modules with B and C in Q, and A of order in S with trivial action, motive C implies motive B. Then motive holds for every finite discrete G-module in Q.