Injectively trivial maps into the Auslander–Reiten translate

For an arrow f : P₁ → P₀ between finite projectives, a map g : N → D Tr(f) determines a scalar functional on Hom_A(P₁,N) by the Nakayama Hom pairing. This functional is in the image of dual restriction to ker f exactly when g extends across an embedding of N into an injective module.

Equivalently, the functional vanishes on maps P₁ → N killing ker f exactly when g factors through that embedding. These maps are the Hom cocycles of a projective presentation. The criterion identifies the injectively trivial maps that must be quotiented out in Auslander–Reiten duality, without identifying a general presentation's Hom cokernel with Ext¹.

No minimality, finite-dimensionality of the algebra, or exactness assumption on f is required. The injective module can have a different universe from the presenting modules; Small is the hypothesis used by Mathlib's injective extension property across universes.

References

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

The comparison uses nakayamaHomEquiv and LinearMap.auslanderReitenTranslateEquivKerNakayama.

theorem LinearMap.auslanderReitenTranslate_exists_extension_iff {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} {N : Type t} {I : Type s} [AddCommGroup P₀] [Module A P₀] [Module.Finite A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] [Module.Finite A P₁] [Module.Projective A P₁] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [AddCommGroup I] [Module A I] [Module k I] [IsScalarTower k A I] [Small.{s, v} A] [Module.Injective A I] (f : P₁ →ₗ[A] P₀) (j : N →ₗ[A] I) (hj : Function.Injective ⇑j) (g : N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) : (∃ (h : I →ₗ[A] TauCeti.AuslanderReitenTranslate k f), h ∘ₗ j = g) ↔ (TauCeti.nakayamaHomEquiv k A P₁ N).symm (f.auslanderReitenTranslateToNakayama ∘ₗ g) ∈ (lcomp k N f.ker.subtype).dualMap.range

Under Nakayama Hom duality, dual restriction to the kernel of a presenting map detects exactly the maps into its translate that extend across an injective embedding.