Frobenius exact categories

An exact structure has enough projectives when every object is the third term of a conflation whose middle term is relatively projective. Dually, it has enough injectives when every object is the first term of a conflation whose middle term is relatively injective. The projective and injective modules record these conditions using bundled presentations; this file defines a Frobenius exact structure by requiring both conditions and equality of the two relative object classes.

The definition is deliberately a property of a specified TauCeti.ExactStructure: an additive category can carry more than one exact structure, with different projective and injective objects. The split exact structure is the basic example, while the abelian comparison lemmas turn Mathlib's ordinary enough-projective and enough-injective hypotheses into presentations for the canonical abelian exact structure.

This is the input for the stable-category construction: choosing the presentations supplies the projective-injective middle terms used to define suspension and loop objects.

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.

structure TauCeti.ExactStructure.IsFrobenius {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : Prop

A Frobenius exact structure has enough relative projectives and injectives, and these two classes of objects coincide.

• enoughProjectives : E.EnoughProjectives

  Every object admits a relative projective presentation.

• enoughInjectives : E.EnoughInjectives

  Every object admits a relative injective presentation.

• projective_iff_injective (X : C) : E.isProjective X ↔ E.isInjective X

  The relatively projective objects are exactly the relatively injective objects.

@[simp]

theorem TauCeti.ExactStructure.IsFrobenius.injective_iff_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (X : C) : E.isInjective X ↔ E.isProjective X

In a Frobenius exact structure, relative injectivity is equivalent to relative projectivity.

theorem TauCeti.ExactStructure.IsFrobenius.isProjective_I {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) {X : C} (P : E.InjectivePresentation X) : E.isProjective P.I

In a Frobenius exact structure, the middle term of any relative injective presentation is relatively projective.

theorem TauCeti.ExactStructure.IsFrobenius.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) : E.op.IsFrobenius

The opposite of a Frobenius exact structure is Frobenius.

theorem TauCeti.ExactStructure.split_isFrobenius {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (split C).IsFrobenius

Every split exact structure is Frobenius: all objects are both relatively projective and relatively injective.