Invariants of projective p-adic group-algebra modules

Let X be an integral representation of a finite group and let Y be a projective modular representation obtained from X by reduction modulo p. Taking invariants commutes with this reduction: every invariant of Y has an invariant lift, and an invariant vector of X that is divisible by p in X is already divisible by p inside X^G. Consequently

#Y^G = p ^ rank_{ℤ_p}(X^G).

This is the numerical bridge between modular Hom spaces and the ordinary characters of their projective ℤ_p[G]-lifts. The latter determine rank(X^G) by the character-average formula. Together these facts are the fixed-point calculation in Swan's rational detection theorem for projective integral representations.

Main results

• Representation.finrank_invariants_baseChange_ratPadic: extending scalars from ℤ_p to ℚ_p preserves the rank of the invariant submodule.
• Representation.natCard_invariants_eq_pow_finrank_of_reduction: the invariant count above, for an arbitrary equivariant semilinear reduction map with the expected kernel. The cardinality of the reduction of a finite free ℤ_p-module is TauCeti.natCard_quotient_padicInt_smul_top.
• Representation.natCard_invariants_eq_pow_finrank_of_bijective: the same count when the projective modular representation is identified with the reduction of a ℤ_p[G]-module.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Proposition (5.6.10).
• J.-P. Serre, Linear Representations of Finite Groups, Part III, §15–16.
• R. G. Swan, Induced representations and projective modules, Ann. of Math. 71 (1960).

theorem Representation.finrank_invariants_baseChange_ratPadic (p : ℕ) [Fact (Nat.Prime p)] {G : Type u} [Group G] [Finite G] {V : Type v} [AddCommGroup V] [Module ℤ_[p] V] [Module.Finite ℤ_[p] V] [Module.IsTorsionFree ℤ_[p] V] (ρ : Representation ℤ_[p] G V) : Module.finrank ℚ_[p] ↥(baseChange ℚ_[p] ρ).invariants = Module.finrank ℤ_[p] ↥ρ.invariants

Extending a finite torsion-free ℤ_p-representation to ℚ_p preserves the rank of its invariant submodule. This is the rational counterpart to invariant lifting modulo p: it lets the integral invariant count be read from the rationalized representation.

theorem Representation.natCard_invariants_eq_pow_finrank_of_reduction (p : ℕ) [Fact (Nat.Prime p)] {G : Type u} [Group G] [Finite G] {V : Type v} [AddCommGroup V] [Module ℤ_[p] V] [Module.Finite ℤ_[p] V] [Module.IsTorsionFree ℤ_[p] V] {W : Type w} [AddCommGroup W] [Module (ZMod p) W] (ρ : Representation ℤ_[p] G V) (σ : Representation (ZMod p) G W) [Module.Projective (MonoidAlgebra (ZMod p) G) σ.asModule] (f : V →ₛₗ[PadicInt.toZMod] W) (hf : Function.Surjective ⇑f) (hfg : ∀ (g : G) (x : V), f ((ρ g) x) = (σ g) (f x)) (hker : ∀ (x : V), f x = 0 ↔ x ∈ ↑p • ⊤) : Nat.card ↥σ.invariants = p ^ Module.finrank ℤ_[p] ↥ρ.invariants

Invariant vectors commute numerically with projective reduction modulo p. Let ρ be an integral representation and σ a projective modular representation. Suppose that the equivariant semilinear surjection f : V → W has kernel pV. Then #(σ^G) = p ^ rank_{ℤ_p}(ρ^G).

More precisely, f restricts to a surjection ρ^G → σ^G with kernel p ρ^G, so σ^G is the reduction modulo p of the finite free ℤ_p-module ρ^G.

theorem Representation.natCard_invariants_eq_pow_finrank_of_bijective (p : ℕ) [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [Finite G] {W : Type u_2} [AddCommGroup W] [Module (ZMod p) W] (η : Representation (ZMod p) G W) [Module.Projective (MonoidAlgebra (ZMod p) G) η.asModule] (X : Type u_3) [AddCommGroup X] [Module ℤ_[p] X] [Module (MonoidAlgebra ℤ_[p] G) X] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) X] [Module.Finite ℤ_[p] X] [Module.IsTorsionFree ℤ_[p] X] (f : X ⧸ Ideal.span {↑p} • ⊤ →ₛₗ[MonoidAlgebra.mapRingHom G PadicInt.toZMod] η.asModule) (hf : Function.Bijective ⇑f) : Nat.card ↥η.invariants = p ^ Module.finrank ℤ_[p] ↥(ofModule' X).invariants

Invariant counts of projective lifts. If a projective 𝔽_p[G]-representation η is the reduction of a ℤ_p[G]-module X, then #η^G = p ^ rank (X^G).