Cancellation of a Noetherian summand

A Noetherian module P cancels from direct sums, M × P ≃ N × P → M ≃ N, as soon as each of its indecomposable direct summands has a local endomorphism ring. The summands with local endomorphism ring cancel one at a time by Azumaya's argument TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isLocalRing_end; the ascending chain condition makes the splitting of P into indecomposable summands terminate.

The splitting is run as a well-founded induction on the complement of a summand. If a summand Q with complement K is neither zero nor indecomposable, it splits as Q₁ ⊕ Q₂ with both parts nonzero; then Q₂ is a summand with complement K ⊔ Q₁ and Q₁ one with complement K ⊔ Q₂, and both complements strictly contain K. Over a Noetherian module there is no infinite strictly ascending chain of submodules, so the induction closes.

This is the form in which Krull-Schmidt cancellation is applied to finitely generated modules over a finite algebra over a complete Noetherian local ring, where the endomorphism rings of indecomposable modules are local but the modules need not have finite length.

Main results

• TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isNoetherian: a Noetherian module whose indecomposable direct summands have local endomorphism rings cancels from a linear equivalence.

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.nonempty_linearEquiv_of_prod_linearEquiv_of_isNoetherian {A : Type u} [Ring A] {P : Type x} [AddCommGroup P] [Module A P] {M : Type v} {N : Type w} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsNoetherian A P] (hP : ∀ (Q K : Submodule A P), IsCompl Q K → IsIndecomposableModule A ↥Q → IsLocalRing (Module.End A ↥Q)) (h : Nonempty ((M × P) ≃ₗ[A] N × P)) : Nonempty (M ≃ₗ[A] N)

Cancellation of a Noetherian summand. If P is a Noetherian module each of whose indecomposable direct summands has a local endomorphism ring, then a linear equivalence M × P ≃ N × P induces a linear equivalence M ≃ N. No hypothesis is placed on M and N.