Fixed points of pro-p groups on finite p-primary modules

Let G be a pro-p group acting continuously on a finite discrete additive group M in which every element has p-power order. This file proves the fixed-point input to the trivial-filtration theorem for such coefficients. If M is nontrivial then G fixes a nonzero element of M, which may be taken of order p, so M contains a copy of 𝔽_p with trivial action. Applied to the quotient of M by a G-stable subgroup N ≠ ⊤, this gives an element x ∉ N with p • x ∈ N that is fixed modulo N. Iterating this relative form builds the G-stable chain of subgroups from ⊥ to ⊤ with 𝔽_p-factors and trivial action; the iteration is carried out in TauCeti.Topology.Algebra.Group.Profinite.ProP.Filtration.

These statements are the dévissage input for the cohomology of pro-p groups: a property of finite discrete p-primary coefficient modules that holds for 𝔽_p with trivial action and is stable under extensions, such as the vanishing of a cohomological functor in a fixed degree, holds for every such module.

The finite case, a p-group acting on a nonzero finite p-group fixes a nonzero element, is Mathlib's IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point; this file extends it to pro-p groups. The order computations for p-primary additive groups are in TauCeti.GroupTheory.PGroup.Additive, and the induced action on the quotient by a G-stable subgroup, AddSubgroup.quotientDistribMulAction, is in TauCeti.Algebra.GroupAction.QuotientAddGroup.

Main results

• TauCeti.exists_ne_zero_invariant_of_isProP: a pro-p group acting continuously on a nontrivial finite discrete p-primary additive group fixes a nonzero element.
• TauCeti.exists_ne_zero_nsmul_eq_zero_invariant_of_isProP: the fixed element may be taken of order p; TauCeti.exists_addSubgroup_natCard_eq_invariant_of_isProP packages it as a G-stable subgroup of order p with trivial action.
• TauCeti.exists_notMem_nsmul_mem_smul_sub_mem_of_isProP: the relative form, a fixed element of order p modulo a G-stable subgroup N ≠ ⊤.

References

• J.-P. Serre, Galois Cohomology, Chapter I, §4.1.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 7.7.

theorem TauCeti.exists_ne_zero_invariant_of_isProP_of_isOpen_ker {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddGroup M] [DistribMulAction G M] [Finite M] (hG : IsProP p G) [Nontrivial M] (hK : IsOpen ↑(MulAction.toPermHom G M).ker) (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (m : M), m ≠ 0 ∧ ∀ (g : G), g • m = m

Nonzero fixed points, open-kernel form. A pro-p group acting on a nontrivial finite p-primary additive group M with open kernel fixes a nonzero element. This form asks for no topology on M, only that the kernel of the action be open in G, and so applies to quotients M ⧸ N by G-stable subgroups.

theorem TauCeti.exists_ne_zero_nsmul_eq_zero_invariant_of_isProP_of_isOpen_ker {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddGroup M] [DistribMulAction G M] [Finite M] (hG : IsProP p G) [Nontrivial M] (hK : IsOpen ↑(MulAction.toPermHom G M).ker) (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (m : M), m ≠ 0 ∧ p • m = 0 ∧ ∀ (g : G), g • m = m

Fixed points of order p, open-kernel form. The nonzero fixed element can be taken to have order p.

theorem TauCeti.exists_ne_zero_invariant_of_isProP {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddGroup M] [DistribMulAction G M] [Finite M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hG : IsProP p G) [Nontrivial M] (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (m : M), m ≠ 0 ∧ ∀ (g : G), g • m = m

The trivial-filtration theorem, first form. A pro-p group acting continuously on a nontrivial finite discrete p-primary additive group fixes a nonzero element.

theorem TauCeti.exists_ne_zero_nsmul_eq_zero_invariant_of_isProP {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddGroup M] [DistribMulAction G M] [Finite M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hG : IsProP p G) [Nontrivial M] (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (m : M), m ≠ 0 ∧ p • m = 0 ∧ ∀ (g : G), g • m = m

A pro-p group acting continuously on a nontrivial finite discrete p-primary additive group fixes a nonzero element of order p.

theorem TauCeti.exists_addSubgroup_natCard_eq_invariant_of_isProP {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddGroup M] [DistribMulAction G M] [Finite M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hG : IsProP p G) [Nontrivial M] (htors : ∀ (m : M), ∃ (k : ℕ), p ^ k • m = 0) : ∃ (N : AddSubgroup M), Nat.card ↥N = p ∧ ∀ (g : G), ∀ x ∈ N, g • x = x

A nontrivial finite discrete p-primary additive group with a continuous action of a pro-p group contains a G-stable subgroup of order p on which G acts trivially: a copy of 𝔽_p with trivial action.

theorem TauCeti.exists_notMem_nsmul_mem_smul_sub_mem_of_isProP {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [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 : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) (hN' : N ≠ ⊤) : ∃ x ∉ N, p • x ∈ N ∧ ∀ (g : G), g • x - x ∈ N

The trivial-filtration theorem, relative form. For a G-stable subgroup N ≠ ⊤ of a finite discrete p-primary additive group M with a continuous action of a pro-p group G, there is x ∉ N with p • x ∈ N whose class modulo N is fixed by G: the quotient M ⧸ N, with the induced action AddSubgroup.quotientDistribMulAction, contains a copy of 𝔽_p with trivial action.