Cancellation of direct summands

Azumaya's cancellation argument says that a module whose endomorphism ring is local cancels from a finite direct sum. Concretely, if End(P) is local and M × P ≃ N × P, then M ≃ N. This is the one-summand form of Krull--Schmidt cancellation; iterating it over an indecomposable decomposition cancels an arbitrary Krull--Schmidt module.

This theorem does not require finite generation. Finiteness enters applications only in proving that the common summand decomposes into pieces with local endomorphism rings. A module of finite length does, by Fitting's lemma, so every common summand of finite length cancels. The modules being compared need not have finite length themselves.

A consequence is that two surjections s t : M → P onto a projective module of finite length differ by an automorphism of M.

Main results

• TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isLocalRing_end: a common summand with local endomorphism ring cancels from a linear equivalence.
• TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isFiniteLength: a common summand of finite length cancels from a linear equivalence.
• TauCeti.exists_linearEquiv_comp_eq_of_surjective: two surjections onto a projective module of finite length differ by an automorphism of their source.

References

• G. Azumaya, Corrections and supplementaries to my paper concerning Krull--Remak--Schmidt's theorem, Nagoya Math. J. 1 (1950), 117--124.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Proposition (5.6.10)(i).
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.

theorem TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isLocalRing_end {A : Type u} [Semiring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {P : Type x} [AddCommGroup P] [Module A P] [IsLocalRing (Module.End A P)] (h : Nonempty ((M × P) ≃ₗ[A] N × P)) : Nonempty (M ≃ₗ[A] N)

Cancellation of a summand with local endomorphism ring. If End_A(P) is local, a linear equivalence M × P ≃ N × P induces a linear equivalence M ≃ N.

No finiteness assumption is needed. The local endomorphism hypothesis already implies that P is indecomposable; this is the one-summand cancellation step iterated in Krull--Schmidt--Azumaya cancellation.

theorem TauCeti.nonempty_linearEquiv_of_prod_linearEquiv_of_isFiniteLength {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {P : Type x} [AddCommGroup P] [Module A P] (hP : IsFiniteLength A P) (h : Nonempty ((M × P) ≃ₗ[A] N × P)) : Nonempty (M ≃ₗ[A] N)

Cancellation of a summand of finite length. If P has finite length, a linear equivalence M × P ≃ N × P induces a linear equivalence M ≃ N.

No finiteness is required of M and N.

theorem TauCeti.exists_linearEquiv_comp_eq_of_surjective {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {P : Type x} [AddCommGroup P] [Module A P] [Module.Projective A P] (hP : IsFiniteLength A P) {s t : M →ₗ[A] P} (hs : Function.Surjective ⇑s) (ht : Function.Surjective ⇑t) : ∃ (θ : M ≃ₗ[A] M), t ∘ₗ ↑θ = s

Two surjections onto a projective module of finite length differ by an automorphism. If P is projective of finite length and s t : M → P are surjective, then t ∘ θ = s for some automorphism θ of M.