Krull-Schmidt cancellation over finite p-adic group algebras

For a finite monoid G, in particular a finite group, finitely generated modules over the group algebra ℤ_p[G] cancel from direct sums: M × P ≃ N × P with P finitely generated gives M ≃ N. This is the specialization to R = ℤ_p and A = ℤ_p[G] of TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isAdicComplete; a finitely generated ℤ_p[G]-module is finitely generated over ℤ_p because ℤ_p[G] is.

⚠ The corresponding statement over ℤ[G] fails in general: Swan's stably free, non-free modules over the integral group rings of generalized quaternion groups. The completeness of ℤ_p is what makes the endomorphism rings of indecomposable ℤ_p[G]-modules local.

Together with Schanuel's lemma, cancellation shows that two maps with the same range from a finitely generated projective ℤ_p[G]-module have isomorphic kernels. In particular the kernel of a surjection from ℤ_p[G]^n onto a module depends only on n and the module, not on the surjection.

Main results

• TauCeti.nonempty_linearEquiv_of_prod_linearEquiv: finitely generated ℤ_p[G]-modules cancel.
• TauCeti.nonempty_ker_linearEquiv_of_range_eq: maps with the same range from a finitely generated projective ℤ_p[G]-module have isomorphic kernels.

References

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

theorem TauCeti.nonempty_linearEquiv_of_prod_linearEquiv (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Monoid G] [Finite G] (M : Type v) (N : Type w) (P : Type x) [AddCommGroup M] [Module (MonoidAlgebra ℤ_[p] G) M] [AddCommGroup N] [Module (MonoidAlgebra ℤ_[p] G) N] [AddCommGroup P] [Module (MonoidAlgebra ℤ_[p] G) P] [Module.Finite (MonoidAlgebra ℤ_[p] G) P] (h : Nonempty ((M × P) ≃ₗ[MonoidAlgebra ℤ_[p] G] N × P)) : Nonempty (M ≃ₗ[MonoidAlgebra ℤ_[p] G] N)

Krull-Schmidt cancellation over ℤ_p[G] (NSW (5.6.10)(i)). For a finite monoid G, in particular a finite group, a finitely generated ℤ_p[G]-module P cancels from direct sums: a linear equivalence M × P ≃ N × P induces a linear equivalence M ≃ N. No hypothesis is placed on M and N.

theorem TauCeti.nonempty_ker_linearEquiv_of_range_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Monoid G] [Finite G] {P : Type v} {E : Type w} [AddCommGroup P] [Module (MonoidAlgebra ℤ_[p] G) P] [Module.Finite (MonoidAlgebra ℤ_[p] G) P] [Module.Projective (MonoidAlgebra ℤ_[p] G) P] [AddCommGroup E] [Module (MonoidAlgebra ℤ_[p] G) E] {a b : P →ₗ[MonoidAlgebra ℤ_[p] G] E} (h : a.range = b.range) : Nonempty (↥a.ker ≃ₗ[MonoidAlgebra ℤ_[p] G] ↥b.ker)

Kernels of maps with the same range. Two ℤ_p[G]-linear maps a b : P → E with the same range, from a finitely generated projective ℤ_p[G]-module P, have isomorphic kernels. In particular two surjections from ℤ_p[G]^n onto the same module have isomorphic kernels.