Documentation

TauCeti.Algebra.Homology.TotallyAcyclic.Abelian.Frobenius

The Frobenius category of Gorenstein-projective objects #

Let C be an abelian category. Its Gorenstein-projective objects are closed under extensions (CategoryTheory.isGorensteinProjective_isExtensionClosed), so they inherit the exact structure of C. This exact structure is Frobenius: complete resolutions give conflations Z⁻¹ ↪ P⁻¹ ↠ Z⁰ and Z⁰ ↪ P⁰ ↠ Z¹ with projective middle terms, and both the relative projectives and the relative injectives are exactly the objects which are projective in C. Projectives of C are relatively injective because a Gorenstein-projective object has no extensions by them.

Hence the stable category of Gorenstein-projective objects, the quotient by the morphisms factoring through projectives, is triangulated by Happel's theorem (TauCeti.ExactStructure.IsFrobenius.stablePretriangulated and TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated). No hypothesis on C beyond being abelian is needed; in particular C need not have enough projectives.

Attribution #

The construction adapts the Frobenius exact structure on finitely generated Gorenstein-projective modules over a Noetherian ring in TauCeti/Algebra/Homology/GorensteinProjective/Frobenius.lean (TauCeti.GorensteinProjectiveModuleCat.exactStructure_isFrobenius): the full subcategory with its inherited exact structure, the conflations cut out of a complete resolution, and the identification of the relative projectives and injectives with the projective objects, here from totally acyclic complexes in an arbitrary abelian category.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev CategoryTheory.GorensteinProjective (C : Type u) [Category.{v, u} C] [Abelian C] :
Type u

The full subcategory of Gorenstein-projective objects of an abelian category.

Instances For
    source
    noncomputable def CategoryTheory.GorensteinProjective.exactStructure (C : Type u) [Category.{v, u} C] [Abelian C] :
    TauCeti.ExactStructure (GorensteinProjective C)

    The exact structure on Gorenstein-projective objects induced by the abelian exact structure of C.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.GorensteinProjective.exactStructure_conflation_iff {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex (GorensteinProjective C)) :
      (exactStructure C).Conflation S ↔ (S.map (isGorensteinProjective C).ι).ShortExact

      The conflations of Gorenstein-projective objects are the short exact sequences of C.

      source
      @[simp]
      theorem CategoryTheory.GorensteinProjective.exactStructure_isProjective_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : GorensteinProjective C) :
      (exactStructure C).isProjective X ↔ Projective X.obj

      The relative projectives among Gorenstein-projective objects are the projective objects of C.

      source
      @[simp]
      theorem CategoryTheory.GorensteinProjective.exactStructure_isInjective_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : GorensteinProjective C) :
      (exactStructure C).isInjective X ↔ Projective X.obj

      The relative injectives among Gorenstein-projective objects are also the projective objects of C, not the injective ones.

      source
      theorem CategoryTheory.GorensteinProjective.exactStructure_enoughProjectives {C : Type u} [Category.{v, u} C] [Abelian C] :
      (exactStructure C).EnoughProjectives

      Complete resolutions provide enough relative projectives.

      source
      theorem CategoryTheory.GorensteinProjective.exactStructure_enoughInjectives {C : Type u} [Category.{v, u} C] [Abelian C] :
      (exactStructure C).EnoughInjectives

      Complete resolutions provide enough relative injectives.

      source
      theorem CategoryTheory.GorensteinProjective.exactStructure_isFrobenius {C : Type u} [Category.{v, u} C] [Abelian C] :
      (exactStructure C).IsFrobenius

      Gorenstein-projective objects form a Frobenius exact category, whose projective-injective objects are the projective objects of C.

      source
      theorem CategoryTheory.GorensteinProjective.exactStructure_isProjective_factorsThrough_iff {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : GorensteinProjective C} (f : X ⟶ Y) :
      (exactStructure C).isProjective.FactorsThrough f ↔ (isProjective C).FactorsThrough f.hom

      A morphism of Gorenstein-projective objects factors through a relatively projective object exactly when it factors through a projective object of C.