Essential surjectivity of the stable transpose

Every finitely presented right module is the transpose of a finite projective presentation of a finitely presented left module. Dualizing a right presentation with values in the regular module A produces the left presentation; evaluation recovers the original right module when that presentation is transposed.

Consequently the stable transpose functor is essentially surjective for every choice of finite projective presentations, over an arbitrary ring. This is the object-level part of the Auslander–Bridger duality between finitely presented stable left and right modules.

References

• M. Auslander, M. Bridger, Stable module theory, Section 2.1.

theorem TauCeti.FiniteProjectivePresentation.exists_transpose_linearEquiv {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) : ∃ (M : ModuleCat A) (_ : Module.FinitePresentation A ↑M) (P : FiniteProjectivePresentation M), Nonempty (AuslanderReitenTranspose P.p ≃ₗ[Aᵐᵒᵖ] ↑N)

Every finite projective right presentation is recovered by transposing a finite projective left presentation. The recovered module is linearly isomorphic before passing to the stable category.

instance TauCeti.stableTransposeFunctor_essSurj {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) : (stableTransposeFunctor P).EssSurj

The stable transpose attached to any family of finite projective presentations is essentially surjective onto the opposite category of finitely presented stable right modules.

instance TauCeti.stableTranspose_essSurj {A : Type u} [Ring A] : (stableTranspose A).EssSurj

The stable transpose formed using chosen finite projective presentations is essentially surjective.