Swan's theorem for ℤ_p[G]

For a finite group G, two finitely generated projective ℤ_p[G]-modules are isomorphic when their rationalizations are isomorphic. This is Swan's theorem, NSW (5.6.10)(ii).

The proof first detects the reductions modulo p by counting maps to every simple 𝔽_p[G]-module. Those counts are dimensions of invariant spaces in conjugation representations. Projective lifts turn the dimensions into integral invariant ranks, which the character formula computes from traces. Traces at p-singular elements vanish for projective modules. For a p-regular element, restriction to its cyclic subgroup reduces trace equality to the prime-to-p case of Swan's theorem. The resulting equivalence modulo p lifts to an integral equivalence because both modules are projective.

Main result

• TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat: finitely generated projective ℤ_p[G]-modules with isomorphic rationalizations are isomorphic.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Proposition (5.6.10)(ii).
• R. G. Swan, Induced representations and projective modules, Ann. of Math. 71 (1960).

theorem TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat (p : ℕ) [Fact (Nat.Prime p)] {G : Type u} [Group G] [Finite G] (M : Type v) (N : Type w) [AddCommGroup M] [Module ℤ_[p] M] [Module (MonoidAlgebra ℤ_[p] G) M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] [Module.Finite (MonoidAlgebra ℤ_[p] G) M] [Module.Projective (MonoidAlgebra ℤ_[p] G) M] [AddCommGroup N] [Module ℤ_[p] N] [Module (MonoidAlgebra ℤ_[p] G) N] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) N] [Module.Finite (MonoidAlgebra ℤ_[p] G) N] [Module.Projective (MonoidAlgebra ℤ_[p] G) N] (h : Nonempty (TensorProduct ℤ_[p] M ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] G] TensorProduct ℤ_[p] N ℚ_[p])) : Nonempty (M ≃ₗ[MonoidAlgebra ℤ_[p] G] N)

Swan's theorem for ℤ_p[G] (NSW (5.6.10)(ii)). Two finitely generated projective ℤ_p[G]-modules with isomorphic rationalizations are isomorphic.