Frobenius full subcategories and their stable inclusions #
An extension-closed full subcategory of a Frobenius exact category inherits a Frobenius
exact structure if it contains the ambient projective-injectives and is closed under kernels
and cokernels of conflations with projective-injective middle term. These are sufficient
closure conditions, recorded by ExactStructure.IsFrobeniusSubcategory; extension closure
alone does not guarantee enough projectives or injectives.
For the induced structure, relative projectivity and injectivity agree with their ambient
counterparts. The stable inclusion is fully faithful: every ambient projectively trivial
morphism between subcategory objects already factors through a projective of the subcategory.
It is a triangle functor by StableConflationExact.stableFunctorIsTriangulated, applied to
IsFrobeniusSubcategory.stableConflationExact_ι and .isFrobenius.
The shift comparisons and triangulated structures are the existing Happel constructions;
they are installed locally as in that theorem.
References #
- Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
- Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, https://arxiv.org/abs/0811.1480, Sections 11–13.
Sufficient closure conditions for a full subcategory of a Frobenius exact category to inherit its Frobenius structure and embed fully faithfully on stable categories.
The kernel and cokernel conditions apply to all conflations with projective-injective middle
term. In particular, the ambient projective and injective presentations remain inside P.
Containing all ambient projective-injectives also ensures that ambient stable factorizations
between objects of P can be carried out within the subcategory.
- extensionClosed : E.IsExtensionClosed P
Extensions of objects of the subcategory remain in it.
Every ambient projective-injective object belongs to the subcategory.
- kernel_mem {S : CategoryTheory.ShortComplex C} : E.Conflation S → E.projectiveInjective S.X₂ → P S.X₃ → P S.X₁
Kernels of deflations from projective-injectives to subcategory objects remain in it.
- cokernel_mem {S : CategoryTheory.ShortComplex C} : E.Conflation S → E.projectiveInjective S.X₂ → P S.X₁ → P S.X₃
Cokernels of inflations into projective-injectives from subcategory objects remain in it.
Instances For
Containing the ambient projective-injectives ensures that the subcategory contains zero.
Extension closure and the zero object imply closure under binary biproducts.
Relative projectivity in the induced structure is precisely ambient relative projectivity. The closure conditions guarantee a presentation inside the subcategory; a projective object is then a retract of its ambient projective middle term.
Relative injectivity in the induced structure is precisely ambient relative injectivity. An injective object is a retract of the ambient injective middle term of its presentation.
The exact structure induced on a subcategory satisfying the closure conditions is Frobenius. Both kinds of presentations are restrictions of ambient presentations.
The full-subcategory inclusion preserves conflations and projective-injectives, so its
stable functor is a triangle functor by StableConflationExact.stableFunctorIsTriangulated
with the Frobenius structures hP.isFrobenius hE and hE.
The projective stable ideal of the induced structure is exactly the inverse image of the ambient stable ideal. In particular, the stable inclusion reflects zero morphisms.
The stable inclusion of a full Frobenius subcategory satisfying the closure conditions is faithful: an ambient factorization through a projective can be made in the subcategory.