The Auslander–Reiten pairing on Hom cocycles

For a map f : P₁ → P₀ between finite projective modules, let Z be the maps P₁ → N vanishing on ker f, and let B be the maps obtained by precomposition with f. The Nakayama Hom pairing induces a surjection

Hom_A(N, D Tr(f)) → D (Z / B).

Its kernel consists exactly of maps extending across an embedding of N into an injective module. Thus quotienting the Hom space by maps through injectives gives the dual of the cocycle quotient. Unlike the full Hom cokernel, Z / B imposes the cocycle condition required for a projective presentation with nonzero kernel. The pairing is defined over a commutative ring; surjectivity and the kernel criterion use a field. No minimality or finite-dimensionality of the algebra or N is required. Postcomposition on Hom cocycle classes is dual to precomposition on translate Hom, so the pairing is contravariantly natural in the coefficient module.

In presentation-level Auslander–Reiten duality, identifying the cocycle quotient with Ext¹ gives a pairing between extension classes and maps into the translate modulo maps through injectives.

References

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

The construction uses TauCeti.nakayamaHomEquiv and LinearMap.auslanderReitenTranslateEquivKerNakayama.

noncomputable def LinearMap.auslanderReitenCocyclePairing {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [CommRing k] [Algebra k A] [Module k N] [IsScalarTower k A N] (f : P₁ →ₗ[A] P₀) : (N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) →ₗ[k] Module.Dual k (f.HomCocycleQuotient N)

The Auslander–Reiten pairing restricts a translate Hom functional to the Hom cocycles and descends it modulo the coboundaries.

@[simp]

theorem LinearMap.auslanderReitenCocyclePairing_apply_mk {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [CommRing k] [Algebra k A] [Module k N] [IsScalarTower k A N] (f : P₁ →ₗ[A] P₀) (g : N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) (h : ↥(lcomp k N f.ker.subtype).ker) : (f.auslanderReitenCocyclePairing g) (Submodule.Quotient.mk h) = ((TauCeti.nakayamaHomEquiv k A P₁ N).symm (f.auslanderReitenTranslateToNakayama ∘ₗ g)) ↑h

Evaluation of the pairing on a cocycle class is restriction of the Nakayama Hom functional. This characterizes the pairing without unfolding its construction.

theorem LinearMap.auslanderReitenCocyclePairing_naturality {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [CommRing k] [Algebra k A] [Module k N] [IsScalarTower k A N] {N' : Type u_1} [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] (f : P₁ →ₗ[A] P₀) (g : N →ₗ[A] N') (h : N' →ₗ[A] TauCeti.AuslanderReitenTranslate k f) : (f.homCocycleQuotientMap g).dualMap (f.auslanderReitenCocyclePairing h) = f.auslanderReitenCocyclePairing (h ∘ₗ g)

Dualizing postcomposition on Hom cocycle classes agrees with precomposition on the translate side of the Auslander–Reiten pairing.

@[instance_reducible]

def LinearMap.instAddCommGroupAuslanderReitenTranslate {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [Field k] [Algebra k A] (f : P₁ →ₗ[A] P₀) : AddCommGroup (TauCeti.AuslanderReitenTranslate k f)

The additive group inherited from the dual, made available locally so that nested quotient instance synthesis can find it in the public quotient signatures.

theorem LinearMap.auslanderReitenCocyclePairing_surjective {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [Field k] [Algebra k A] [Module k N] [IsScalarTower k A N] (f : P₁ →ₗ[A] P₀) : Function.Surjective ⇑f.auslanderReitenCocyclePairing

Every functional on Hom cocycles modulo coboundaries is obtained by pairing with a map into the Auslander–Reiten translate.

theorem LinearMap.auslanderReitenCocyclePairing_eq_zero_iff {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [Field k] [Algebra k A] [Module k N] [IsScalarTower k A N] (f : P₁ →ₗ[A] P₀) (g : N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) : f.auslanderReitenCocyclePairing g = 0 ↔ (TauCeti.nakayamaHomEquiv k A P₁ N).symm (f.auslanderReitenTranslateToNakayama ∘ₗ g) ∈ (lcomp k N f.ker.subtype).dualMap.range

A map has zero cocycle pairing exactly when its Nakayama functional is in the image of dual restriction to the kernel of the presenting arrow.

theorem LinearMap.auslanderReitenCocyclePairing_eq_zero_iff_exists_extension {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [Field k] [Algebra k A] [Module k N] [IsScalarTower k A N] {I : Type s} [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) : f.auslanderReitenCocyclePairing g = 0 ↔ ∃ (h : I →ₗ[A] TauCeti.AuslanderReitenTranslate k f), h ∘ₗ j = g

The kernel of the Auslander–Reiten cocycle pairing consists exactly of maps extending across any fixed embedding into an injective module.

noncomputable def LinearMap.auslanderReitenCocycleQuotientEquiv {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [Field k] [Algebra k A] [Module k N] [IsScalarTower k A N] {I : Type s} [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) : ((N →ₗ[A] TauCeti.AuslanderReitenTranslate k f) ⧸ (lcomp k (TauCeti.AuslanderReitenTranslate k f) j).range) ≃ₗ[k] Module.Dual k (f.HomCocycleQuotient N)

An embedding into an injective module computes the quotient of translate Hom by injectively trivial maps. The cocycle pairing identifies this quotient with the dual of Hom cocycles modulo coboundaries.

@[simp]

theorem LinearMap.auslanderReitenCocycleQuotientEquiv_mk {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [Field k] [Algebra k A] [Module k N] [IsScalarTower k A N] {I : Type s} [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) : (f.auslanderReitenCocycleQuotientEquiv j hj) (Submodule.Quotient.mk g) = f.auslanderReitenCocyclePairing g

On a representative, quotient duality is the cocycle pairing.

@[simp]

theorem LinearMap.auslanderReitenCocycleQuotientEquiv_symm_pairing {k : Type u} {A : Type v} [Ring A] {P₀ : Type w} {P₁ : Type z} {N : Type t} [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] [Field k] [Algebra k A] [Module k N] [IsScalarTower k A N] {I : Type s} [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) : (f.auslanderReitenCocycleQuotientEquiv j hj).symm (f.auslanderReitenCocyclePairing g) = Submodule.Quotient.mk g

Inverse quotient duality returns the class of any map giving the functional.