Recovery by minimal transposition

Let Q present a right module N, and let P present its right transpose Tr N, the cokernel of the A-valued dual of the presenting map of Q. Transposing P recovers N up to actual isomorphism exactly when N has no nonzero projective retracts, provided N and the transpose of P have finite length. The first map of P must have superfluous kernel, as it does for a minimal presentation. The presentation Q need not be minimal. The scalar-dual characterization gives the corresponding recovery by the Auslander–Reiten translate.

This removes the projective ambiguity from one composite of the Auslander–Bridger correspondence. Applied to a scalar dual, it is the recovery step for the inverse Tr D of the Auslander–Reiten translate. Using the A-valued right transpose keeps the recovery linear over Aᵐᵒᵖ, even for a noncommutative ring.

References

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

theorem TauCeti.FiniteProjectivePresentation.nonempty_linearEquiv_transpose_rightTranspose_iff_isZero_projective_retract {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) (P : FiniteProjectivePresentation Q.rightTranspose) (hP : IsSuperfluous P.p.ker) (hN : IsFiniteLength Aᵐᵒᵖ ↑N) (hTr : IsFiniteLength Aᵐᵒᵖ (AuslanderReitenTranspose P.p)) : Nonempty (AuslanderReitenTranspose P.p ≃ₗ[Aᵐᵒᵖ] ↑N) ↔ ∀ {R : ModuleCat Aᵐᵒᵖ} (a : CategoryTheory.Retract R N), CategoryTheory.Projective R → CategoryTheory.Limits.IsZero R

Transposition of a right transpose, using a presenting map with superfluous kernel, recovers the original right module exactly when it has no nonzero projective retracts. In particular this applies to a minimal presentation; the right presentation is arbitrary.

theorem TauCeti.FiniteProjectivePresentation.nonempty_linearEquiv_translate_rightTranspose_iff_isZero_projective_retract {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} {k : Type u_1} [CommSemiring k] [Algebra k A] [Module k ↑N] [IsScalarTower k Aᵐᵒᵖ ↑N] [Module.IsReflexive k ↑N] {E : Type u_2} [AddCommGroup E] [Module A E] [Module k E] (Q : FiniteProjectivePresentation N) (P : FiniteProjectivePresentation Q.rightTranspose) (hP : IsSuperfluous P.p.ker) (hN : IsFiniteLength Aᵐᵒᵖ ↑N) (hTr : IsFiniteLength Aᵐᵒᵖ (AuslanderReitenTranspose P.p)) [Module.IsReflexive k (AuslanderReitenTranspose P.p)] (e : E ≃ₗ[k] Module.Dual k ↑N) (he : ∀ (a : A) (x : E) (n : ↑N), (e (a • x)) n = (e x) (MulOpposite.op a • n)) : Nonempty (AuslanderReitenTranslate k P.p ≃ₗ[A] E) ↔ ∀ {R : ModuleCat Aᵐᵒᵖ} (a : CategoryTheory.Retract R N), CategoryTheory.Projective R → CategoryTheory.Limits.IsZero R

Applying D Tr to a presentation of the right transpose of N recovers the scalar dual D N exactly when N has no nonzero projective retracts. The scalar dual is specified by an equivariant pairing, and reflexivity suffices in place of a finite-dimensional field hypothesis. This is the recovery composite for the inverse Tr D correspondence.