Stable categories of finitely generated modules

For a right Noetherian ring A, this file defines the stable category of finitely generated right A-modules as the additive quotient by maps factoring through projective modules. When A is a finite-dimensional algebra over a field and is self-injective on both sides, the canonical exact structure on FGModuleCat Aᵐᵒᵖ is Frobenius. In that case this is the usual stable module category: projective and injective modules coincide, and precisely they become zero in the quotient.

The construction is stated first for a right Noetherian ring because the quotient itself does not use self-injectivity. The finite-dimensional self-injective hypotheses enter only in the results identifying the killed objects with injectives. This is the stmod-A carrier used by stable module and hypersurface comparison theorems.

Main definitions

• FGModuleCat.stableModuleCategory A is the stable category of finitely generated right A-modules.
• FGModuleCat.stableModuleFunctor A is the quotient functor.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
• Ragnar-Olaf Buchweitz, Maximal Cohen--Macaulay Modules and Tate Cohomology, Section 4.

@[reducible, inline]

noncomputable abbrev TauCeti.FGModuleCat.stableModuleCategory (A : Type u) [Ring A] [IsNoetherianRing Aᵐᵒᵖ] : Type (u + 1)

The stable module category of finitely generated right A-modules: maps factoring through a projective module are killed. For a finite-dimensional self-injective algebra, this is the usual category stmod-A.

Equations

• TauCeti.FGModuleCat.stableModuleCategory A = (TauCeti.ExactStructure.abelian (FGModuleCat Aᵐᵒᵖ)).ProjectiveStableCategory

@[reducible, inline]

noncomputable abbrev TauCeti.FGModuleCat.stableModuleFunctor (A : Type u) [Ring A] [IsNoetherianRing Aᵐᵒᵖ] : CategoryTheory.Functor (FGModuleCat Aᵐᵒᵖ) (stableModuleCategory A)

The quotient functor from finitely generated right A-modules to their stable category.

Equations

• TauCeti.FGModuleCat.stableModuleFunctor A = (TauCeti.ExactStructure.abelian (FGModuleCat Aᵐᵒᵖ)).projectiveStableFunctor

theorem FGModuleCat.isZero_stableModuleFunctor_obj_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (X : FGModuleCat Aᵐᵒᵖ) : CategoryTheory.Limits.IsZero ((TauCeti.FGModuleCat.stableModuleFunctor A).obj X) ↔ CategoryTheory.Projective X

A finitely generated module is zero in the stable module category exactly when it is projective.

theorem TauCeti.FGModuleCat.stableModuleFunctor_map_eq_zero_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FGModuleCat Aᵐᵒᵖ} (f : X ⟶ Y) : (stableModuleFunctor A).map f = 0 ↔ ∃ (P : FGModuleCat Aᵐᵒᵖ), CategoryTheory.Projective P ∧ ∃ (i : X ⟶ P) (p : P ⟶ Y), f = CategoryTheory.CategoryStruct.comp i p

A map of finitely generated modules vanishes in the stable module category exactly when it factors through a projective module.

theorem TauCeti.FGModuleCat.stableModuleFunctor_map_eq_zero_iff_exists_lift {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X Y P : FGModuleCat Aᵐᵒᵖ} [CategoryTheory.Projective P] (π : P ⟶ Y) [CategoryTheory.Epi π] (f : X ⟶ Y) : (stableModuleFunctor A).map f = 0 ↔ ∃ (g : X ⟶ P), CategoryTheory.CategoryStruct.comp g π = f

A map into Y vanishes in the stable module category exactly when it lifts along a given epimorphism π : P ⟶ Y from a projective module.

theorem TauCeti.FGModuleCat.stableModuleFunctor_map_eq_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FGModuleCat Aᵐᵒᵖ} (f g : X ⟶ Y) : (stableModuleFunctor A).map f = (stableModuleFunctor A).map g ↔ ∃ (P : FGModuleCat Aᵐᵒᵖ), CategoryTheory.Projective P ∧ ∃ (i : X ⟶ P) (p : P ⟶ Y), f - g = CategoryTheory.CategoryStruct.comp i p

Two maps of finitely generated modules are equal in the stable module category exactly when their difference factors through a projective module.

theorem FGModuleCat.isZero_stableModuleFunctor_obj_iff_injective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (k : Type w) [Field k] [Algebra k A] [FiniteDimensional k A] (hr : Module.Injective Aᵐᵒᵖ Aᵐᵒᵖ) (hl : Module.Injective Aᵐᵒᵖᵐᵒᵖ Aᵐᵒᵖ) (X : FGModuleCat Aᵐᵒᵖ) : CategoryTheory.Limits.IsZero ((TauCeti.FGModuleCat.stableModuleFunctor A).obj X) ↔ CategoryTheory.Injective X

For a finite-dimensional algebra self-injective on both sides, an object is zero in stmod-A exactly when it is injective.

theorem TauCeti.FGModuleCat.stableModuleFunctor_map_eq_zero_iff_injective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (k : Type w) [Field k] [Algebra k A] [FiniteDimensional k A] (hr : Module.Injective Aᵐᵒᵖ Aᵐᵒᵖ) (hl : Module.Injective Aᵐᵒᵖᵐᵒᵖ Aᵐᵒᵖ) {X Y : FGModuleCat Aᵐᵒᵖ} (f : X ⟶ Y) : (stableModuleFunctor A).map f = 0 ↔ ∃ (I : FGModuleCat Aᵐᵒᵖ), CategoryTheory.Injective I ∧ ∃ (i : X ⟶ I) (p : I ⟶ Y), f = CategoryTheory.CategoryStruct.comp i p

Under the self-injectivity hypotheses, a map is zero in stmod-A exactly when it factors through an injective module.