The trivial filtration of a finite p-primary module under a pro-p group

Let G be a pro-p group acting continuously on a finite discrete additive group M in which every element has p-power order. Iterating the relative fixed-point theorem exists_notMem_nsmul_mem_smul_sub_mem_of_isProP, which supplies for each G-stable subgroup N ≠ ⊤ an element x ∉ N with p • x ∈ N fixed modulo N, this file builds the trivial filtration of M: a G-stable increasing chain of subgroups from ⊥ to ⊤ in which every successive factor is a copy of 𝔽_p with trivial G-action. The chain has length the p-adic valuation of |M|, the composition length of M, and is constant at ⊤ from there on. The successive quotients are then packaged as additive groups equivalent to ZMod p, with the induced actions trivial. The ambient finite p-primary group need not be killed by p.

Main results

• TauCeti.exists_filtration_of_isProP: the G-stable filtration with 𝔽_p-factors and trivial action, of length padicValNat p (Nat.card M), described by generators.
• TauCeti.exists_filtration_with_trivial_factors_of_isProP: the same filtration with explicit additive equivalences of the factors with ZMod p and trivial quotient actions.

theorem TauCeti.exists_filtration_of_isProP {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hG : IsProP p G) (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (N : ℕ → AddSubgroup M), N 0 = ⊥ ∧ Monotone N ∧ (∀ (i : ℕ), padicValNat p (Nat.card M) ≤ i → N i = ⊤) ∧ (∀ (i : ℕ) (g : G), ∀ x ∈ N i, g • x ∈ N i) ∧ (∀ i ≤ padicValNat p (Nat.card M), Nat.card ↥(N i) = p ^ i) ∧ ∀ i < padicValNat p (Nat.card M), ∃ (x : M), N (i + 1) = N i ⊔ AddSubgroup.zmultiples x ∧ x ∉ N i ∧ p • x ∈ N i ∧ ∀ (g : G), g • x - x ∈ N i

The trivial-filtration theorem. A finite discrete p-primary additive group M with a continuous action of a pro-p group G has a G-stable increasing chain of subgroups N 0 = ⊥ ≤ N 1 ≤ … reaching ⊤ after padicValNat p (Nat.card M) steps, the composition length of M, and constant at ⊤ from there on, with |N i| = p ^ i along the way. Each step adjoins an element x with x ∉ N i, p • x ∈ N i and g • x - x ∈ N i for every g, so every factor N (i + 1) ⧸ N i is a copy of 𝔽_p with trivial G-action.

theorem TauCeti.exists_filtration_with_trivial_factors_of_isProP {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hG : IsProP p G) (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (N : ℕ → AddSubgroup M) (hN : ∀ (i : ℕ) (g : G), ∀ x ∈ N i, g • x ∈ N i), N 0 = ⊥ ∧ Monotone N ∧ (∀ (i : ℕ), padicValNat p (Nat.card M) ≤ i → N i = ⊤) ∧ (∀ i ≤ padicValNat p (Nat.card M), Nat.card ↥(N i) = p ^ i) ∧ ∀ i < padicValNat p (Nat.card M), Nonempty (↥(N (i + 1)) ⧸ (N i).addSubgroupOf (N (i + 1)) ≃+ ZMod p) ∧ ∀ (g : G) (y : ↥(N (i + 1)) ⧸ (N i).addSubgroupOf (N (i + 1))), g • y = y

A finite discrete p-primary group with a continuous pro-p action has a stable filtration whose successive quotients are additively equivalent to ZMod p and have trivial induced action. Only indices below the composition length contribute a factor; the chain is constant at ⊤ thereafter.