Loops on a projective stable category

For an exact structure with enough projectives, choose conflations ΩX ⟶ P(X) ⟶ X. Lifting a morphism X ⟶ Y to the projective middle terms induces a map ΩX ⟶ ΩY. Different lifts induce the same map modulo morphisms factoring through projectives. This constructs the additive loop endofunctor on the projective stable category.

Only enough projectives are needed for the construction. In a Frobenius exact category this is the loop functor used with suspension to construct the stable triangulation; the one statement about the chosen presentation that needs the Frobenius hypothesis, that its middle term is also relatively injective, is recorded at the end of the file. Neither a quasi-inverse comparison nor a triangulated structure is asserted in this file.

The API follows the suspension construction in TauCeti.CategoryTheory.Exact.Stable.Suspension, but works without the Frobenius hypothesis. It exposes the chosen presentation and its commuting squares for subsequent comparisons.

Main definitions

• TauCeti.ExactStructure.EnoughProjectives.loopObj: the kernel of the chosen presentation.
• TauCeti.ExactStructure.EnoughProjectives.loopMap: the induced map on kernels.
• TauCeti.ExactStructure.EnoughProjectives.stableLoop: the additive stable loop functor.
• TauCeti.ExactStructure.EnoughProjectives.stableLoopObjIso: the stable loop object is the kernel term of any relative projective presentation.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1.

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.EnoughProjectives.loopProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : C

The chosen projective middle term in the loop presentation of X.

Equations

• hE.loopProjective X = (hE.projectivePresentation X).P

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.EnoughProjectives.loopObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : C

The loop object ΩX, the kernel term of the chosen projective presentation.

Equations

• hE.loopObj X = (hE.projectivePresentation X).K

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.EnoughProjectives.loopInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : hE.loopObj X ⟶ hE.loopProjective X

The inflation ΩX ⟶ P(X) in the chosen loop presentation.

Equations

• hE.loopInflation X = (hE.projectivePresentation X).i

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.EnoughProjectives.loopDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : hE.loopProjective X ⟶ X

The deflation P(X) ⟶ X in the chosen loop presentation.

Equations

• hE.loopDeflation X = (hE.projectivePresentation X).p

theorem TauCeti.ExactStructure.EnoughProjectives.isProjective_loopProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : E.isProjective (hE.loopProjective X)

The middle term of the chosen loop presentation is projective relative to E.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopInflation_comp_loopDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : CategoryTheory.CategoryStruct.comp (hE.loopInflation X) (hE.loopDeflation X) = 0

The two maps in the chosen loop presentation compose to zero.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopInflation_comp_loopDeflation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.loopInflation X) (CategoryTheory.CategoryStruct.comp (hE.loopDeflation X) h) = CategoryTheory.CategoryStruct.comp 0 h

The two maps in the chosen loop presentation compose to zero.

theorem TauCeti.ExactStructure.EnoughProjectives.conflation_loopInflation_loopDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : E.Conflation { X₁ := hE.loopObj X, X₂ := hE.loopProjective X, X₃ := X, f := hE.loopInflation X, g := hE.loopDeflation X, zero := ⋯ }

The chosen loop presentation is a conflation of E.

noncomputable def TauCeti.ExactStructure.EnoughProjectives.loopMiddleMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) : hE.loopProjective X ⟶ hE.loopProjective Y

The chosen lift of f : X ⟶ Y between the projective middle terms.

Equations

• hE.loopMiddleMap f = (hE.projectivePresentation X).middleMap (hE.projectivePresentation Y) f

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopMiddleMap_comp_loopDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (hE.loopMiddleMap f) (hE.loopDeflation Y) = CategoryTheory.CategoryStruct.comp (hE.loopDeflation X) f

The middle map lifts f along the loop deflations.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopMiddleMap_comp_loopDeflation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.loopMiddleMap f) (CategoryTheory.CategoryStruct.comp (hE.loopDeflation Y) h) = CategoryTheory.CategoryStruct.comp (hE.loopDeflation X) (CategoryTheory.CategoryStruct.comp f h)

The middle map lifts f along the loop deflations.

noncomputable def TauCeti.ExactStructure.EnoughProjectives.loopMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) : hE.loopObj X ⟶ hE.loopObj Y

The induced map on loop objects. Its class modulo projectives is independent of the lift.

Equations

• hE.loopMap f = (hE.projectivePresentation X).kernelMap (hE.projectivePresentation Y) f

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopMap_comp_loopInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (hE.loopMap f) (hE.loopInflation Y) = CategoryTheory.CategoryStruct.comp (hE.loopInflation X) (hE.loopMiddleMap f)

The induced loop map makes the square on the inflations commute.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopMap_comp_loopInflation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) {Z : C} (h : hE.loopProjective Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (hE.loopMap f) (CategoryTheory.CategoryStruct.comp (hE.loopInflation Y) h) = CategoryTheory.CategoryStruct.comp (hE.loopInflation X) (CategoryTheory.CategoryStruct.comp (hE.loopMiddleMap f) h)

The induced loop map makes the square on the inflations commute.

theorem TauCeti.ExactStructure.EnoughProjectives.projectiveStableFunctor_map_loopMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) (a : hE.loopProjective X ⟶ hE.loopProjective Y) (g : hE.loopObj X ⟶ hE.loopObj Y) (ha : CategoryTheory.CategoryStruct.comp a (hE.loopDeflation Y) = CategoryTheory.CategoryStruct.comp (hE.loopDeflation X) f) (hg : CategoryTheory.CategoryStruct.comp g (hE.loopInflation Y) = CategoryTheory.CategoryStruct.comp (hE.loopInflation X) a) : E.projectiveStableFunctor.map (hE.loopMap f) = E.projectiveStableFunctor.map g

Any compatible maps between the chosen loop presentations inducing f give the same morphism as loopMap f in the projective stable quotient.

noncomputable def TauCeti.ExactStructure.EnoughProjectives.loopToStable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) : CategoryTheory.Functor C E.ProjectiveStableCategory

Loops from the exact category to its projective stable quotient.

Equations

• hE.loopToStable = E.loopToStableOfPresentations hE.projectivePresentation

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopToStable_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : hE.loopToStable.obj X = E.projectiveStableFunctor.obj (hE.loopObj X)

The object formula for loops to the projective stable category.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.loopToStable_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) : hE.loopToStable.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.loopMap f)) (CategoryTheory.eqToHom ⋯))

The morphism formula for loops to the projective stable category.

instance TauCeti.ExactStructure.EnoughProjectives.loopToStable_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) : hE.loopToStable.Additive

Loops to the stable quotient preserve addition of morphisms.

theorem TauCeti.ExactStructure.EnoughProjectives.isProjective_loopObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X : C} (hX : E.isProjective X) : E.isProjective (hE.loopObj X)

The loop object of a projective object is projective.

theorem TauCeti.ExactStructure.EnoughProjectives.loopToStable_kills_projectiveStableIdeal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) : E.projectiveStableIdeal ≤ hE.loopToStable.kerIdeal

Loops to the stable quotient kill every map factoring through a projective.

noncomputable def TauCeti.ExactStructure.EnoughProjectives.stableLoop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) : CategoryTheory.Functor E.ProjectiveStableCategory E.ProjectiveStableCategory

The additive loop endofunctor on the projective stable category.

Equations

• hE.stableLoop = E.projectiveStableIdeal.lift hE.loopToStable ⋯

instance TauCeti.ExactStructure.EnoughProjectives.stableLoop_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) : hE.stableLoop.Additive

Stable loops preserve addition of morphisms.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.stableLoop_obj_projectiveStableFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) (X : C) : hE.stableLoop.obj (E.projectiveStableFunctor.obj X) = E.projectiveStableFunctor.obj (hE.loopObj X)

On represented objects, the stable loop functor takes the chosen kernel.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.stableLoop_map_projectiveStableFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X Y : C} (f : X ⟶ Y) : hE.stableLoop.map (E.projectiveStableFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.loopMap f)) (CategoryTheory.eqToHom ⋯))

On represented morphisms, the stable loop functor applies the chosen kernel map.

noncomputable def TauCeti.ExactStructure.EnoughProjectives.stableLoopObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X : C} (P : E.ProjectivePresentation X) : hE.stableLoop.obj (E.projectiveStableFunctor.obj X) ≅ E.projectiveStableFunctor.obj P.K

The stable loop object of X is the kernel term of any relative projective presentation of X: the chosen presentation is compared with P by ProjectivePresentation.projectiveStableIso.

Equations

• hE.stableLoopObjIso P = CategoryTheory.eqToIso ⋯ ≪≫ (hE.projectivePresentation X).projectiveStableIso P

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.stableLoopObjIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X : C} (P : E.ProjectivePresentation X) : (hE.stableLoopObjIso P).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (E.projectiveStableFunctor.map ((hE.projectivePresentation X).kernelMap P (CategoryTheory.CategoryStruct.id X)))

The comparison with the stable loop object is induced by the identity of the presented object.

@[simp]

theorem TauCeti.ExactStructure.EnoughProjectives.stableLoopObjIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.EnoughProjectives) {X : C} (P : E.ProjectivePresentation X) : (hE.stableLoopObjIso P).inv = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.kernelMap (hE.projectivePresentation X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯)

The inverse comparison with the stable loop object is induced by the identity of the presented object.

Loop presentations of a Frobenius exact structure

theorem TauCeti.ExactStructure.IsFrobenius.isInjective_loopProjective {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 (⋯.loopProjective X)

The middle term of a chosen loop presentation is relatively injective.