Projective ℤ_p[G]-modules with isomorphic rationalizations

Let G be a finite group. Swan's theorem (NSW (5.6.10)(ii)) says that a finitely generated projective ℤ_p[G]-module P is determined up to isomorphism by its rationalization P ⊗ ℚ_p. This file proves the comparison of hom counts that relates rationalizations to reductions modulo p, and deduces Swan's theorem when p does not divide |G|.

For lattices M and N (finitely generated ℤ_p[G]-modules, torsion-free over ℤ_p) with isomorphic rationalizations, clearing denominators gives injective ℤ_p[G]-linear maps M → N and N → M. Hence the free ℤ_p-modules Hom(P, M) and Hom(P, N) have the same rank for every finitely generated P. When P is projective, the maps from P into M ⧸ p • M are the reductions modulo p of Hom(P, M). Therefore P has as many maps into M ⧸ p • M as into N ⧸ p • N: the number of maps from a projective module into the reduction of a lattice depends only on the rationalization of the lattice (compare Serre's identity ⟨P, d(E)⟩ = ⟨P ⊗ ℚ_p, E⟩ between the Cartan and decomposition maps, which also computes this number).

When p ∤ |G|, the ideal (p) is the Jacobson radical of ℤ_p[G], so the reductions of M and N are semisimple. Comparing the numbers of maps between these finite semisimple modules identifies them, and projective covers lift the identification to M ≃ N. For general G the reduction M ⧸ p • M need not be semisimple, and this last step does not apply.

Main results

• TauCeti.natCard_linearMap_quotient_eq_of_tensorRat: a finitely generated projective ℤ_p[G]-module has equally many maps into the reductions modulo p of two lattices with isomorphic rationalizations.
• TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat_of_not_dvd: for p ∤ |G|, 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).
• J.-P. Serre, Linear Representations of Finite Groups, Part III, §15–16 (the cde triangle).
• R. G. Swan, Induced representations and projective modules, Ann. of Math. 71 (1960).

theorem TauCeti.natCard_linearMap_quotient_eq_of_tensorRat {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Monoid G] [Finite G] (P : Type v) [AddCommGroup P] [Module (MonoidAlgebra ℤ_[p] G) P] [Module.Finite (MonoidAlgebra ℤ_[p] G) P] [Module.Projective (MonoidAlgebra ℤ_[p] G) P] (M : 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.IsTorsionFree ℤ_[p] M] (N : Type x) [AddCommGroup N] [Module ℤ_[p] N] [Module (MonoidAlgebra ℤ_[p] G) N] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) N] [Module.Finite (MonoidAlgebra ℤ_[p] G) N] [Module.IsTorsionFree ℤ_[p] N] (h : Nonempty (TensorProduct ℤ_[p] M ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] G] TensorProduct ℤ_[p] N ℚ_[p])) : Nat.card (P →ₗ[MonoidAlgebra ℤ_[p] G] M ⧸ Ideal.span {↑p} • ⊤) = Nat.card (P →ₗ[MonoidAlgebra ℤ_[p] G] N ⧸ Ideal.span {↑p} • ⊤)

Maps from a projective module into reductions of rationally isomorphic lattices. Let P be a finitely generated projective ℤ_p[G]-module and M, N finitely generated ℤ_p[G]-modules, torsion-free over ℤ_p, with ℤ_p[G]-isomorphic rationalizations M ⊗ ℚ_p ≃ N ⊗ ℚ_p. Then there are as many ℤ_p[G]-linear maps from P to M ⧸ p • M as to N ⧸ p • N.

The rational isomorphism gives injective maps M → N and N → M, so the free ℤ_p-modules Hom(P, M) and Hom(P, N) have the same rank; the maps from P into a reduction are the reductions modulo p of these modules.

theorem TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat_of_not_dvd (p : ℕ) [Fact (Nat.Prime p)] {G : Type u} [Group G] [Finite G] (hG : ¬p ∣ Nat.card 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)

Projective ℤ_p[G]-modules are detected rationally when p ∤ |G| (Swan's theorem NSW (5.6.10)(ii) for a finite group of order prime to p). Two finitely generated projective ℤ_p[G]-modules with ℤ_p[G]-isomorphic rationalizations are isomorphic.

The reductions M ⧸ p • M and N ⧸ p • N are semisimple, because p generates the Jacobson radical of ℤ_p[G], and by TauCeti.natCard_linearMap_quotient_eq_of_tensorRat there are as many maps from M (or from N) into either reduction. Finite semisimple modules with these counts are isomorphic, and the isomorphism of reductions lifts to M ≃ N because M and N are projective.