Reflecting indecomposability from the projective stable category #
The projective stable quotient forgets projective summands. If a module has no nonzero projective retract, however, indecomposability of its stable image implies indecomposability of the module itself. This recovers actual indecomposability from stable constructions such as the Auslander–Bridger transpose, once projective summands have been excluded.
No finite-length, Artinian, or field hypothesis is needed for this implication.
References #
- M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.
theorem
ModuleCat.indecomposable_iff_isZero_projective_retract
{A : Type u}
[Ring A]
(M : ModuleCat A)
(hM : CategoryTheory.Indecomposable ((TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj M))
:
CategoryTheory.Indecomposable M ↔ ∀ {P : ModuleCat A} (a : CategoryTheory.Retract P M), CategoryTheory.Projective P → CategoryTheory.Limits.IsZero P
For a module whose stable image is indecomposable, actual indecomposability is equivalent to every projective retract being zero.