Recovering isomorphisms from the projective stable category

The projective stable quotient detects invertibility and isomorphism classes between finite-length modules with no nonzero projective retracts. Indecomposability is not required: the modules may be sums of non-projective indecomposables. This lets stable inverse comparisons recover actual modules after projective summands have been excluded.

The argument uses Mathlib's Fitting decomposition LinearMap.eventually_isCompl_ker_pow_range_pow. If an endomorphism becomes the identity in the quotient, its eventual kernel is a projective retract and hence vanishes.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.

theorem ModuleCat.isIso_projectiveStableFunctor_map_iff_of_isZero_projective_retract {A : Type u} [Ring A] {M N : ModuleCat A} (f : M ⟶ N) (hM : IsFiniteLength A ↑M) (hN : IsFiniteLength A ↑N) (hPM : ∀ {P : ModuleCat A} (a : CategoryTheory.Retract P M), CategoryTheory.Projective P → CategoryTheory.Limits.IsZero P) (hPN : ∀ {P : ModuleCat A} (a : CategoryTheory.Retract P N), CategoryTheory.Projective P → CategoryTheory.Limits.IsZero P) : CategoryTheory.IsIso ((TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.map f) ↔ CategoryTheory.IsIso f

The projective stable quotient detects invertibility between finite-length modules whose projective retracts are all zero. The modules need not be indecomposable.

theorem ModuleCat.nonempty_iso_projectiveStableFunctor_obj_iff_of_isZero_projective_retract {A : Type u} [Ring A] (M N : ModuleCat A) (hM : IsFiniteLength A ↑M) (hN : IsFiniteLength A ↑N) (hPM : ∀ {P : ModuleCat A} (a : CategoryTheory.Retract P M), CategoryTheory.Projective P → CategoryTheory.Limits.IsZero P) (hPN : ∀ {P : ModuleCat A} (a : CategoryTheory.Retract P N), CategoryTheory.Projective P → CategoryTheory.Limits.IsZero P) : Nonempty ((TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj M ≅ (TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj N) ↔ Nonempty (M ≅ N)

Stable isomorphism is equivalent to actual isomorphism for finite-length modules with no nonzero projective retracts. In particular this removes projective ambiguity without assuming that either module is indecomposable.