From a stable isomorphism to an isomorphism over ℤ_p[G]

Let G be a finite group. If two ℤ_p[G]-modules become isomorphic after adding finitely generated projective modules, M ⊕ P ≃ N ⊕ Q, and their rationalizations differ by the rationalization of a finitely generated projective module F, M ⊗ ℚ_p ≃ (N ⊕ F) ⊗ ℚ_p, then already M ≃ N ⊕ F (NSW (5.6.11)). For F = ℤ_p[G]^m this turns a stable isomorphism into an isomorphism M ≃ N ⊕ ℤ_p[G]^m once the rational representations are known.

The proof has three steps. Rationalizing the stable isomorphism and cancelling the rational representation N ⊗ ℚ_p gives (F ⊕ P) ⊗ ℚ_p ≃ Q ⊗ ℚ_p. Swan's theorem then gives F ⊕ P ≃ Q, since both are finitely generated projective. Finally M ⊕ P ≃ N ⊕ F ⊕ P, and Krull-Schmidt cancellation of P over ℤ_p[G] gives M ≃ N ⊕ F.

Main results

• TauCeti.nonempty_linearEquiv_prod_of_stable: a stable isomorphism M ⊕ P ≃ N ⊕ Q together with M ⊗ ℚ_p ≃ (N ⊕ F) ⊗ ℚ_p for a finitely generated projective F gives M ≃ N ⊕ F.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Proposition (5.6.11).

theorem TauCeti.nonempty_linearEquiv_prod_of_stable (p : ℕ) [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [Finite G] {M : Type u_2} {N : Type u_3} {F : Type u_4} {P : Type u_5} {Q : Type u_6} [AddCommGroup M] [Module ℤ_[p] M] [Module (MonoidAlgebra ℤ_[p] G) M] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] [AddCommGroup N] [Module ℤ_[p] N] [Module (MonoidAlgebra ℤ_[p] G) N] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) N] [Module.Finite ℤ_[p] N] [AddCommGroup F] [Module ℤ_[p] F] [Module (MonoidAlgebra ℤ_[p] G) F] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) F] [Module.Finite (MonoidAlgebra ℤ_[p] G) F] [Module.Projective (MonoidAlgebra ℤ_[p] G) F] [AddCommGroup P] [Module (MonoidAlgebra ℤ_[p] G) P] [Module.Finite (MonoidAlgebra ℤ_[p] G) P] [Module.Projective (MonoidAlgebra ℤ_[p] G) P] [AddCommGroup Q] [Module (MonoidAlgebra ℤ_[p] G) Q] [Module.Finite (MonoidAlgebra ℤ_[p] G) Q] [Module.Projective (MonoidAlgebra ℤ_[p] G) Q] (h : Nonempty ((M × P) ≃ₗ[MonoidAlgebra ℤ_[p] G] N × Q)) (hrat : Nonempty (TensorProduct ℤ_[p] M ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] G] TensorProduct ℤ_[p] (N × F) ℚ_[p])) : Nonempty (M ≃ₗ[MonoidAlgebra ℤ_[p] G] N × F)

From a stable isomorphism to an isomorphism (NSW (5.6.11)). Let G be a finite group and let M, N be ℤ_p[G]-modules with N finitely generated over ℤ_p. Suppose that M ⊕ P ≃ N ⊕ Q for finitely generated projective ℤ_p[G]-modules P and Q, and that M ⊗ ℚ_p ≃ (N ⊕ F) ⊗ ℚ_p for a finitely generated projective ℤ_p[G]-module F. Then M ≃ N ⊕ F as ℤ_p[G]-modules. The case of interest is the free module F = ℤ_p[G]^m.