The injectively trivial part of the Auslander–Reiten pairing

A morphism N → D Tr(f) factors through an injective object exactly when its Nakayama Hom functional belongs to the image of dual restriction to ker f. This identifies the subspace killed on the Hom side of Auslander–Reiten duality. The cocycle pairing kills exactly the same morphisms as the injective stable quotient. It therefore identifies injective stable Hom into the translate with the scalar dual of Hom cocycles modulo coboundaries, naturally in the coefficient module. Descending cocycles to the presenting image identifies this quotient with Ext¹ of the cokernel. Thus the pairing gives Auslander–Reiten duality stableHom(N, D Tr(f)) ≃ D Ext¹(coker f,N), with Hom taken modulo injectives.

The statement uses the existing injective stable category of modules and does not depend on a choice of injective envelope. It applies to arbitrary algebras over a field and maps between finite projectives, without minimality or exactness.

References

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

theorem LinearMap.auslanderReitenTranslate_injectiveStableFunctor_map_eq_zero_iff {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (g : ↑N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) : (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.map (ModuleCat.ofHom g) = 0 ↔ (TauCeti.nakayamaHomEquiv k A P₁ ↑N).symm (f.auslanderReitenTranslateToNakayama ∘ₗ g) ∈ (lcomp k (↑N) f.ker.subtype).dualMap.range

Maps into D Tr(f) factoring through injective objects correspond exactly to the image of dual restriction to the kernel of f under the Nakayama Hom pairing.

theorem LinearMap.auslanderReitenCocyclePairing_eq_zero_iff_injectiveStableFunctor_map_eq_zero {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (g : ↑N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) : f.auslanderReitenCocyclePairing g = 0 ↔ (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.map (ModuleCat.ofHom g) = 0

The cocycle pairing kills exactly the morphisms killed by the injective stable quotient functor.

noncomputable def LinearMap.auslanderReitenStableHomEquiv {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) : ((TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj N ⟶ (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj ↧(TauCeti.AuslanderReitenTranslate k f)) ≃ₗ[k] Module.Dual k (f.HomCocycleQuotient ↑N)

Injective stable Hom into D Tr(f) is the scalar dual of Hom cocycles modulo coboundaries. This comparison does not choose an injective embedding.

@[simp]

theorem LinearMap.auslanderReitenStableHomEquiv_map {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (g : N ⟶ ↧(TauCeti.AuslanderReitenTranslate k f)) : (f.auslanderReitenStableHomEquiv N) ((TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.map g) = f.auslanderReitenCocyclePairing (ModuleCat.Hom.hom g)

The stable Hom comparison sends the stable class of a map to its cocycle pairing.

@[simp]

theorem LinearMap.auslanderReitenStableHomEquiv_symm_pairing {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (g : N ⟶ ↧(TauCeti.AuslanderReitenTranslate k f)) : (f.auslanderReitenStableHomEquiv N).symm (f.auslanderReitenCocyclePairing (ModuleCat.Hom.hom g)) = (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.map g

The inverse comparison sends a cocycle pairing to the stable class of its map.

theorem LinearMap.auslanderReitenStableHomEquiv_naturality {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) {N N' : ModuleCat A} (g : N ⟶ N') (h : (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj N' ⟶ (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj ↧(TauCeti.AuslanderReitenTranslate k f)) : (f.auslanderReitenStableHomEquiv N) (CategoryTheory.CategoryStruct.comp ((TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.map g) h) = (f.homCocycleQuotientMap (ModuleCat.Hom.hom g)).dualMap ((f.auslanderReitenStableHomEquiv N') h)

Precomposition in the injective stable category corresponds to the dual of postcomposition on Hom cocycle classes.

noncomputable def LinearMap.auslanderReitenExtEquiv {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) : ((TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj N ⟶ (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj ↧(TauCeti.AuslanderReitenTranslate k f)) ≃ₗ[k] Module.Dual k (CategoryTheory.Abelian.Ext (↧(P₀ ⧸ f.range)) N 1)

Auslander–Reiten duality: injective stable Hom into D Tr(f) is the scalar dual of the first extension group of the cokernel of f.

@[simp]

theorem LinearMap.auslanderReitenExtEquiv_apply {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (h : (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj N ⟶ (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj ↧(TauCeti.AuslanderReitenTranslate k f)) (x : f.HomCocycleQuotient ↑N) : ((f.auslanderReitenExtEquiv N) h) ((f.homCocycleQuotientEquivExt N) x) = ((f.auslanderReitenStableHomEquiv N) h) x

Evaluate duality at the extension class corresponding to a Hom cocycle class.

theorem LinearMap.auslanderReitenExtEquiv_naturality {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [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₁] (f : P₁ →ₗ[A] P₀) {N N' : ModuleCat A} (g : N ⟶ N') (h : (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj N' ⟶ (TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.obj ↧(TauCeti.AuslanderReitenTranslate k f)) (α : CategoryTheory.Abelian.Ext (↧(P₀ ⧸ f.range)) N 1) : ((f.auslanderReitenExtEquiv N) (CategoryTheory.CategoryStruct.comp ((TauCeti.ExactStructure.abelian (ModuleCat A)).injectiveStableFunctor.map g) h)) α = ((f.auslanderReitenExtEquiv N') h) (α.comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯)

Precomposition in injective stable Hom is dual to pushforward of extension classes.