Totally acyclic complexes and Gorenstein-projective modules

Let A be a ring. A cochain complex P of A-modules is totally acyclic when every term Pⁿ is finitely generated and projective, P is acyclic, and the dual complex Hom_A(P, A) is acyclic as well. A module is Gorenstein-projective when it is isomorphic to the degree-zero cycles Z⁰(P) of a totally acyclic complex P; the complex is then a complete resolution of the module.

Right modules over a ring R are the case A = Rᵐᵒᵖ, where Hom_{Rᵐᵒᵖ}(P, Rᵐᵒᵖ) is the usual R-dual of a complex of right R-modules.

The dual of Pⁿ is Pⁿ →ₗ[A] A, which is a right A-module, that is, an Aᵐᵒᵖ-module, through right multiplication on the target. The dual differential Hom_A(Pᵏ, A) → Hom_A(Pʲ, A) is precomposition with d : Pʲ ⟶ Pᵏ, which is LinearMap.lcomp Aᵐᵒᵖ A. Dual acyclicity is therefore recorded as exactness of the composable pairs of these precomposition maps.

Finite generation is required of every term of the complex. It is not implied by finite generation of a single module of cycles: adding a contractible complex F --𝟙--> F on an infinitely generated free module F away from degree zero preserves acyclicity, dual acyclicity and Z⁰(P).

Main definitions

• CochainComplex.IsTotallyAcyclic: a totally acyclic complex of finitely generated projective modules.
• TauCeti.IsGorensteinProjective: the modules isomorphic to the degree-zero cycles of a totally acyclic complex.
• TauCeti.alternatingMulRightComplex: the two-periodic complex ⋯ → A --·a--> A --·b--> A → ⋯ for a * b = 0 and b * a = 0.

Main results

• CochainComplex.IsTotallyAcyclic.of_iso and CochainComplex.IsTotallyAcyclic.shift: total acyclicity is invariant under isomorphisms and shifts of complexes.
• CochainComplex.IsTotallyAcyclic.isGorensteinProjective_cycles: the cycles of a totally acyclic complex in every degree are Gorenstein-projective, so the syzygies and cosyzygies of a Gorenstein-projective module in a complete resolution are Gorenstein-projective.
• TauCeti.IsGorensteinProjective.finite: Gorenstein-projective modules are finitely generated.
• TauCeti.isGorensteinProjective_of_projective: a finitely generated projective module is Gorenstein-projective, with complete resolution M --𝟙--> M in degrees -1 and 0.
• TauCeti.isTotallyAcyclic_alternatingMulRightComplex and TauCeti.isGorensteinProjective_span_singleton: for an exact pair of zero-divisors a, b, the two-periodic complex ⋯ → A --·a--> A --·b--> A → ⋯ is totally acyclic, so the left ideal A b is Gorenstein-projective. For A = k[x]/(xⁿ), a = xⁱ and b = xⁿ⁻ⁱ, this is the two-periodic complete resolution of A b ≅ A/(xⁱ); such modules need not be projective.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Mathematical Surveys and Monographs 262, American Mathematical Society (2021), Section 4.
• Edgar E. Enochs and Overtoun M. G. Jenda, Relative Homological Algebra, de Gruyter Expositions in Mathematics 30 (2000), Section 10.2.
• Inês B. Henriques and Liana M. Sega, Free resolutions over short Gorenstein local rings, Mathematische Zeitschrift 267 (2011), 645–663: exact pairs of zero-divisors.

structure CochainComplex.IsTotallyAcyclic {A : Type u} [Ring A] (P : CochainComplex (ModuleCat A) ℤ) : Prop

A cochain complex P of A-modules is totally acyclic when its terms are finitely generated projective modules, it is acyclic, and its A-dual Hom_A(P, A) is acyclic: for i + 1 = j and j + 1 = k, the precomposition maps Hom_A(Pᵏ, A) → Hom_A(Pʲ, A) → Hom_A(Pⁱ, A) are exact.

• finite (n : ℤ) : Module.Finite A ↑(P.X n)

  Every term is a finitely generated module.

• projective (n : ℤ) : CategoryTheory.Projective (P.X n)

  Every term is a projective module.

• acyclic : HomologicalComplex.Acyclic P

  The complex is acyclic.

• exact_dual (i j k : ℤ) (hij : i + 1 = j) (hjk : j + 1 = k) : Function.Exact ⇑(LinearMap.lcomp Aᵐᵒᵖ A (ModuleCat.Hom.hom (P.d j k))) ⇑(LinearMap.lcomp Aᵐᵒᵖ A (ModuleCat.Hom.hom (P.d i j)))

  The A-dual of the complex is acyclic.

theorem CochainComplex.IsTotallyAcyclic.of_iso {A : Type u} [Ring A] {P : CochainComplex (ModuleCat A) ℤ} (hP : P.IsTotallyAcyclic) {Q : CochainComplex (ModuleCat A) ℤ} (e : P ≅ Q) : Q.IsTotallyAcyclic

Total acyclicity is invariant under isomorphisms of complexes.

theorem CochainComplex.IsTotallyAcyclic.shift {A : Type u} [Ring A] {P : CochainComplex (ModuleCat A) ℤ} (hP : P.IsTotallyAcyclic) (m : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex (ModuleCat A) ℤ) m).obj P).IsTotallyAcyclic

A shift of a totally acyclic complex is totally acyclic.

def TauCeti.IsGorensteinProjective (A : Type u) [Ring A] : CategoryTheory.ObjectProperty (ModuleCat A)

A module M is Gorenstein-projective when it is isomorphic to the degree-zero cycles Z⁰(P) of a totally acyclic complex P, a complete resolution of M.

Equations

• TauCeti.IsGorensteinProjective A M = ∃ (P : CochainComplex (ModuleCat A) ℤ), P.IsTotallyAcyclic ∧ Nonempty (HomologicalComplex.cycles P 0 ≅ M)

theorem TauCeti.isGorensteinProjective_iff {A : Type u} [Ring A] (M : ModuleCat A) : IsGorensteinProjective A M ↔ ∃ (P : CochainComplex (ModuleCat A) ℤ), P.IsTotallyAcyclic ∧ Nonempty (HomologicalComplex.cycles P 0 ≅ M)

The defining property of a Gorenstein-projective module: it has a complete resolution.

instance TauCeti.instIsClosedUnderIsomorphismsModuleCatIsGorensteinProjective {A : Type u} [Ring A] : (IsGorensteinProjective A).IsClosedUnderIsomorphisms

theorem TauCeti.IsGorensteinProjective.finite {A : Type u} [Ring A] {M : ModuleCat A} (hM : IsGorensteinProjective A M) : Module.Finite A ↑M

A Gorenstein-projective module is finitely generated: the degree-zero cycles of an acyclic complex are a quotient of the term in degree -1.

theorem CochainComplex.IsTotallyAcyclic.isGorensteinProjective_cycles {A : Type u} [Ring A] {P : CochainComplex (ModuleCat A) ℤ} (hP : P.IsTotallyAcyclic) (n : ℤ) : TauCeti.IsGorensteinProjective A (HomologicalComplex.cycles P n)

The cycles of a totally acyclic complex in any degree n are Gorenstein-projective: the shift P⟦n⟧ is a complete resolution of Zⁿ(P).

theorem TauCeti.isGorensteinProjective_of_projective {A : Type u} [Ring A] (M : ModuleCat A) [Module.Finite A ↑M] [CategoryTheory.Projective M] : IsGorensteinProjective A M

A finitely generated projective module M is Gorenstein-projective: the complex M --𝟙--> M, concentrated in degrees -1 and 0, is a complete resolution of M.

@[reducible, inline]

noncomputable abbrev TauCeti.alternatingMulRightComplex {A : Type u} [Ring A] (a b : A) (hab : a * b = 0) (hba : b * a = 0) : CochainComplex (ModuleCat A) ℤ

The two-periodic complex ⋯ → A --·a--> A --·b--> A --·a--> ⋯ of free A-modules of rank one: every term is A, and the differential out of degree n is right multiplication by a for even n and by b for odd n.

Equations

• TauCeti.alternatingMulRightComplex a b hab hba = CochainComplex.of (fun (x : ℤ) => ↧A) (fun (n : ℤ) => ModuleCat.ofHom (LinearMap.toSpanSingleton A A (if Even n then a else b))) ⋯

@[simp]

theorem TauCeti.alternatingMulRightComplex_X {A : Type u} [Ring A] {a b : A} (hab : a * b = 0) (hba : b * a = 0) (n : ℤ) : (alternatingMulRightComplex a b hab hba).X n = ↧A

Every term of TauCeti.alternatingMulRightComplex a b is A.

theorem TauCeti.alternatingMulRightComplex_d {A : Type u} [Ring A] {a b : A} (hab : a * b = 0) (hba : b * a = 0) {i j : ℤ} (h : i + 1 = j) : (alternatingMulRightComplex a b hab hba).d i j = ModuleCat.ofHom (LinearMap.toSpanSingleton A A (if Even i then a else b))

The differential of TauCeti.alternatingMulRightComplex a b out of degree i is right multiplication by a for even i and by b for odd i.

@[simp]

theorem TauCeti.alternatingMulRightComplex_d_apply {A : Type u} [Ring A] {a b : A} (hab : a * b = 0) (hba : b * a = 0) {i j : ℤ} (h : i + 1 = j) (r : A) : (ModuleCat.Hom.hom ((alternatingMulRightComplex a b hab hba).d i j)) r = r * if Even i then a else b

theorem TauCeti.isTotallyAcyclic_alternatingMulRightComplex {A : Type u} [Ring A] {a b : A} {hab : a * b = 0} {hba : b * a = 0} (hla : ∀ (r : A), r * a = 0 ↔ ∃ (t : A), t * b = r) (hlb : ∀ (r : A), r * b = 0 ↔ ∃ (t : A), t * a = r) (hra : ∀ (s : A), a * s = 0 ↔ ∃ (t : A), b * t = s) (hrb : ∀ (s : A), b * s = 0 ↔ ∃ (t : A), a * t = s) : (alternatingMulRightComplex a b hab hba).IsTotallyAcyclic

Let a, b : A be an exact pair of zero-divisors: the left annihilator of a is A b, the left annihilator of b is A a, the right annihilator of a is b A and the right annihilator of b is a A. Then the two-periodic complex ⋯ → A --·a--> A --·b--> A → ⋯ is totally acyclic. For example, over k[x]/(xⁿ) the pair a = xⁱ, b = xⁿ⁻ⁱ with 0 < i < n is exact.

theorem TauCeti.isGorensteinProjective_span_singleton {A : Type u} [Ring A] {a b : A} (hla : ∀ (r : A), r * a = 0 ↔ ∃ (t : A), t * b = r) (hlb : ∀ (r : A), r * b = 0 ↔ ∃ (t : A), t * a = r) (hra : ∀ (s : A), a * s = 0 ↔ ∃ (t : A), b * t = s) (hrb : ∀ (s : A), b * s = 0 ↔ ∃ (t : A), a * t = s) : IsGorensteinProjective A ↧↥(A ∙ b)

For an exact pair of zero-divisors a, b : A, the left ideal A b is Gorenstein-projective, with complete resolution the two-periodic complex ⋯ → A --·a--> A --·b--> A → ⋯, whose degree-zero cycles are the left annihilator A b of a.