Krull-Schmidt cancellation over a complete local ring

Let R be a complete Noetherian local ring and A an R-algebra, for instance the group algebra ℤ_p[G] of a finite group over the p-adic integers. For modules that are finitely generated over R, the input of the Krull-Schmidt theorem is available even though such modules need not have finite length: the endomorphism ring of an indecomposable one is local. Consequently these modules cancel from direct sums.

Locality is proved one endomorphism at a time. An endomorphism f of an A-module M that is finite over R is integral over R by Cayley-Hamilton, so the commutative subalgebra R[f] is a finite R-module. It is therefore complete along the extension of the maximal ideal of R, hence Henselian there, and its reduction is a finite-dimensional algebra over the residue field. Idempotents of R[f] are idempotents of End_A(M), so indecomposability of M leaves R[f] only the trivial ones, and R[f] is local by TauCeti.HenselianRing.isLocalRing_of_forall_isIdempotentElem. So f or 1 - f is a unit.

⚠ Completeness is essential: over ℤ the analogous cancellation fails for integral group rings (Swan's stably free non-free modules over generalized quaternion groups).

Main results

• TauCeti.isLocalRing_end_of_isIndecomposable_of_isAdicComplete: an indecomposable A-module that is finite over a complete Noetherian local ring R has a local endomorphism ring.
• TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isAdicComplete: Krull-Schmidt cancellation for a summand that is finite over a complete Noetherian local ring.

References

• C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, §6.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Proposition (5.6.10)(i).

theorem TauCeti.isLocalRing_end_of_isIndecomposable_of_isAdicComplete (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] {A : Type u_2} [Ring A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] [Module.Finite R M] (hM : IsIndecomposableModule A M) : IsLocalRing (Module.End A M)

Indecomposable modules over a complete local ring have local endomorphism rings. Let R be a complete Noetherian local ring and A an R-algebra. The endomorphism ring of an indecomposable A-module that is finitely generated over R is local.

theorem TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isAdicComplete (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] {A : Type u_2} [Ring A] [Algebra R A] {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] [Module R P] [IsScalarTower R A P] [Module.Finite R P] (h : Nonempty ((M × P) ≃ₗ[A] N × P)) : Nonempty (M ≃ₗ[A] N)

Krull-Schmidt cancellation over a complete local ring. Let R be a complete Noetherian local ring and A an R-algebra. If P is an A-module that is finitely generated over R, a linear equivalence M × P ≃ N × P of A-modules induces a linear equivalence M ≃ N. No hypothesis is placed on M and N.