Indecomposable modules in the projective stable category

A finite-length indecomposable module remains indecomposable modulo maps through projectives exactly when it is not projective. Between two such non-projective modules, the quotient reflects isomorphisms and detects isomorphism classes.

These results connect stable equivalences, such as the Auslander--Bridger transpose, to isomorphism classes of actual modules. They use Fitting's local-endomorphism-ring criterion and the fact that precisely projective modules become zero in the stable category. The ring is arbitrary; no self-injectivity or field hypothesis is needed.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Section IV.1.

@[simp]

theorem ModuleCat.indecomposable_projectiveStableFunctor_obj_iff {A : Type u} [Ring A] (M : ModuleCat A) (hM : IsFiniteLength A ↑M) (hiM : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable ((TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj M) ↔ ¬CategoryTheory.Projective M

A finite-length indecomposable module remains indecomposable in the projective stable category exactly when it is not projective.

@[simp]

theorem ModuleCat.isIso_projectiveStableFunctor_map_iff {A : Type u} [Ring A] {M N : ModuleCat A} (f : M ⟶ N) (hM : IsFiniteLength A ↑M) (hN : IsFiniteLength A ↑N) (hiM : CategoryTheory.Indecomposable M) (hiN : CategoryTheory.Indecomposable N) (hpM : ¬CategoryTheory.Projective M) : CategoryTheory.IsIso ((TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.map f) ↔ CategoryTheory.IsIso f

The projective stable quotient reflects invertibility between non-projective, finite-length indecomposable modules.

@[simp]

theorem ModuleCat.nonempty_iso_projectiveStableFunctor_obj_iff {A : Type u} [Ring A] (M N : ModuleCat A) (hM : IsFiniteLength A ↑M) (hN : IsFiniteLength A ↑N) (hiM : CategoryTheory.Indecomposable M) (hiN : CategoryTheory.Indecomposable N) (hpM : ¬CategoryTheory.Projective M) : Nonempty ((TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj M ≅ (TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj N) ↔ Nonempty (M ≅ N)

Two non-projective finite-length indecomposable modules are stably isomorphic exactly when they are isomorphic as modules. Only the source needs an explicit non-projectivity hypothesis: a stable isomorphism forces the other module to be non-projective as well.