Fixed points of 2-groups on 𝔽₂-modules

A 2-group acting on a nontrivial finite 𝔽₂-module has a nonzero fixed vector; under a transitive action on the coordinates, an invariant nonzero submodule of 𝔽₂^ι contains the all-ones vector.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

Implementation notes

The eventual Mathlib home of fixed_points_nontrivial and invariant_submodule_all_ones is not obvious (they sit between GroupTheory.PGroup, RepresentationTheory, and the linear-algebra Module files); they are grouped here for now and will be placed during upstreaming.

theorem fixed_points_nontrivial {G : Type u_1} [Group G] (hG : IsPGroup 2 G) {M : Type u_2} [AddCommGroup M] [Module (ZMod 2) M] [Finite M] [Nontrivial M] [DistribMulAction G M] : ∃ (m : M), m ≠ 0 ∧ m ∈ MulAction.fixedPoints G M

A 2-group acting ZMod 2-linearly on a nontrivial finite 𝔽₂-module fixes some nonzero vector.

theorem invariant_submodule_all_ones {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) {ι : Type u_2} [Finite ι] [Nonempty ι] [MulAction G ι] [MulAction.IsPretransitive G ι] (V : Submodule (ZMod 2) (ι → ZMod 2)) (hV : ∀ (g : G), ∀ v ∈ V, (fun (i : ι) => v (g⁻¹ • i)) ∈ V) (hVne : V ≠ ⊥) : (fun (x : ι) => 1) ∈ V

A nonzero G-invariant 𝔽₂-subspace of ι → 𝔽₂, where the finite 2-group G acts pretransitively on ι, contains the all-ones vector.