Totally acyclic complexes and Gorenstein-projective objects in an abelian category

Let C be an abelian category. A cochain complex P in C is a totally acyclic complex of projectives when its terms are projective, it is acyclic, and every chain map from P to a projective object placed in some degree is null-homotopic. The last condition says that the complex Hom_C(P, Q) is acyclic for every projective Q; equivalently, P is left orthogonal in the homotopy category K(C) to the projective objects placed in any degree. An object is Gorenstein-projective when it is isomorphic to the degree-zero cycles of such a complex.

As for Mathlib's CochainComplex.IsKProjective, the definition asks for null-homotopies of chain maps, and the equivalent formulations are lemmas:

• CochainComplex.isTotallyAcyclicProjective_iff_leftOrthogonal: orthogonality in K(C) to HomotopyCategory.singleProjectives C;
• CochainComplex.isTotallyAcyclicProjective_iff_factor: the elementary form, every morphism f : Pⁱ ⟶ Q to a projective object which vanishes on the image of the differential into Pⁱ factors through the differential Pⁱ ⟶ Pⁱ⁺¹. It rests on CochainComplex.nonempty_homotopy_mkHomToSingle_zero_iff.

Taking C to be the category of all modules over a ring gives the Gorenstein-projective modules of Enochs and Jenda. Taking C = FGModuleCat A for a left noetherian ring A gives the finitely generated Gorenstein-projective modules: FGModuleCat.isGorensteinProjective_iff, in TauCeti/Algebra/Homology/TotallyAcyclic/FGModuleCat.lean, identifies them with Tau Ceti's module notion TauCeti.IsGorensteinProjective. That module notion also covers finitely generated modules over rings which are not noetherian, where they need not form an abelian category.

Main definitions

• CochainComplex.IsTotallyAcyclicProjective: totally acyclic complexes of projectives.
• HomotopyCategory.singleProjectives C: the projective objects placed in any degree, in K(C).
• CategoryTheory.isGorensteinProjective C: the Gorenstein-projective objects of C.

Main results

• CochainComplex.IsTotallyAcyclicProjective.shift and CochainComplex.IsTotallyAcyclicProjective.biprod: total acyclicity is stable under shifts and binary biproducts.
• CochainComplex.IsTotallyAcyclicProjective.isGorensteinProjective_cycles: the cycles of a totally acyclic complex of projectives in any degree are Gorenstein-projective.
• CategoryTheory.isGorensteinProjective_of_projective: projective objects are Gorenstein-projective, through the disk Q --𝟙--> Q (CochainComplex.disk).
• CategoryTheory.isGorensteinProjective.biprod: binary biproducts of Gorenstein-projective objects are Gorenstein-projective.

References

• Edgar E. Enochs and Overtoun M. G. Jenda, Relative Homological Algebra, de Gruyter Expositions in Mathematics 30 (2000), Chapter 10.
• Xiao-Wu Chen, Relative singularity categories and Gorenstein-projective modules, Math. Nachr. 284 (2011), 199–212.

def HomotopyCategory.singleProjectives (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))

The projective objects of C placed in any single degree, as objects of the homotopy category, up to isomorphism.

theorem HomotopyCategory.singleProjectives_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : HomotopyCategory C (ComplexShape.up ℤ)) : singleProjectives C X ↔ ∃ (n : ℤ) (Q : C), CategoryTheory.Projective Q ∧ Nonempty (X ≅ (singleFunctor C n).obj Q)

The objects of singleProjectives C are the projective objects placed in a single degree, up to isomorphism.

instance HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSingleProjectives (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : (singleProjectives C).IsClosedUnderIsomorphisms

instance HomotopyCategory.instIsStableUnderShiftIntUpSingleProjectives (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : (singleProjectives C).IsStableUnderShift ℤ

structure CochainComplex.IsTotallyAcyclicProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CochainComplex C ℤ) : Prop

A cochain complex P is a totally acyclic complex of projectives when its terms are projective, it is acyclic, and every chain map from P to a projective object placed in a single degree is null-homotopic; the last condition says that Hom_C(P, Q) is acyclic for every projective Q.

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

  Every term is projective.

• acyclic : HomologicalComplex.Acyclic P

  The complex is acyclic.

• nonempty_homotopy_zero (n : ℤ) (Q : C) [CategoryTheory.Projective Q] (f : P ⟶ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj Q) : Nonempty (Homotopy f 0)

  Every chain map to a projective object placed in a single degree is null-homotopic.

theorem CochainComplex.isTotallyAcyclicProjective_iff_factor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} : P.IsTotallyAcyclicProjective ↔ (∀ (n : ℤ), CategoryTheory.Projective (P.X n)) ∧ HomologicalComplex.Acyclic P ∧ ∀ (i j : ℤ), i + 1 = j → ∀ (Q : C) [CategoryTheory.Projective Q] (φ : P.X i ⟶ Q), CategoryTheory.CategoryStruct.comp (P.d (i - 1) i) φ = 0 → ∃ (g : P.X j ⟶ Q), CategoryTheory.CategoryStruct.comp (P.d i j) g = φ

Elementary form of total acyclicity: a complex of projectives is totally acyclic if and only if it is acyclic and every morphism Pⁱ ⟶ Q to a projective object which vanishes on the image of Pⁱ⁻¹ ⟶ Pⁱ factors through Pⁱ ⟶ Pⁱ⁺¹.

theorem CochainComplex.isTotallyAcyclicProjective_iff_leftOrthogonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} : P.IsTotallyAcyclicProjective ↔ (∀ (n : ℤ), CategoryTheory.Projective (P.X n)) ∧ HomologicalComplex.Acyclic P ∧ (HomotopyCategory.singleProjectives C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj P)

Total acyclicity as orthogonality: a complex of projectives is totally acyclic if and only if it is acyclic and left orthogonal, in the homotopy category, to the projective objects placed in any degree.

theorem CochainComplex.IsTotallyAcyclicProjective.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) {P' : CochainComplex C ℤ} (e : P ≅ P') : P'.IsTotallyAcyclicProjective

Total acyclicity is invariant under isomorphisms of complexes.

theorem CochainComplex.IsTotallyAcyclicProjective.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) {P' : CochainComplex C ℤ} (hP' : P'.IsTotallyAcyclicProjective) : (P ⊞ P').IsTotallyAcyclicProjective

Binary biproducts preserve total acyclicity.

theorem CochainComplex.IsTotallyAcyclicProjective.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) (n : ℤ) : P⟦n⟧.IsTotallyAcyclicProjective

Total acyclicity is stable under shifts.

def CategoryTheory.isGorensteinProjective (C : Type u) [Category.{v, u} C] [Abelian C] : ObjectProperty C

An object of C is Gorenstein-projective when it is isomorphic to the degree-zero cycles of a totally acyclic complex of projectives, a complete resolution of the object.

theorem CategoryTheory.isGorensteinProjective_iff {C : Type u} [Category.{v, u} C] [Abelian C] (M : C) : isGorensteinProjective C M ↔ ∃ (P : CochainComplex C ℤ), P.IsTotallyAcyclicProjective ∧ Nonempty (HomologicalComplex.cycles P 0 ≅ M)

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

instance CategoryTheory.instIsClosedUnderIsomorphismsIsGorensteinProjective {C : Type u} [Category.{v, u} C] [Abelian C] : (isGorensteinProjective C).IsClosedUnderIsomorphisms

theorem CategoryTheory.isTotallyAcyclicProjective_disk {C : Type u} [Category.{v, u} C] [Abelian C] (Q : C) [Projective Q] : (CochainComplex.disk Q).IsTotallyAcyclicProjective

The disk Q --𝟙--> Q of a projective object is a totally acyclic complex of projectives.

theorem CategoryTheory.isGorensteinProjective_of_projective {C : Type u} [Category.{v, u} C] [Abelian C] (Q : C) [Projective Q] : isGorensteinProjective C Q

Projective objects are Gorenstein-projective: the complex Q --𝟙--> Q, concentrated in degrees -1 and 0, is a complete resolution of a projective object Q.

instance CategoryTheory.instContainsZeroIsGorensteinProjective {C : Type u} [Category.{v, u} C] [Abelian C] : (isGorensteinProjective C).ContainsZero

theorem CategoryTheory.isGorensteinProjective.biprod {C : Type u} [Category.{v, u} C] [Abelian C] {G G' : C} (hG : isGorensteinProjective C G) (hG' : isGorensteinProjective C G') : isGorensteinProjective C (G ⊞ G')

Binary biproducts of Gorenstein-projective objects are Gorenstein-projective: the biproduct of complete resolutions is a complete resolution.

theorem CochainComplex.IsTotallyAcyclicProjective.isGorensteinProjective_cycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) (n : ℤ) : CategoryTheory.isGorensteinProjective C (HomologicalComplex.cycles P n)

The cycles of a totally acyclic complex of projectives are Gorenstein-projective, in every degree.