Injective presentations in a projective stable category

Let E be an exact structure and let P and Q be relative injective presentations X ⟶ P.I ⟶ P.K and Y ⟶ Q.I ⟶ Q.K. A morphism f : X ⟶ Y extends to the injective middle terms and hence induces InjectivePresentation.cokernelMap on the cokernel terms. That induced morphism depends on a choice, but once Q.I is relatively projective the choice disappears in the projective stable quotient: any two extensions of f induce the same morphism P.K ⟶ Q.K there.

This file records that independence and its consequences. The construction becomes functorial in the stable quotient, so two presentations of the same object have canonically isomorphic cokernel terms, and a choice of presentation with projective-injective middle term for every object produces a functor from C to the stable category which is independent, up to a canonical natural isomorphism, of that choice. For a Frobenius exact structure the middle terms are automatically projective and this functor is the suspension.

Main definitions

• TauCeti.ExactStructure.InjectivePresentation.projectiveStableIso: the canonical isomorphism between the cokernel terms of two relative injective presentations of the same object, in the projective stable category.
• TauCeti.ExactStructure.suspensionToStableOfPresentations: the functor to the projective stable category determined by a choice of relative injective presentations with relatively projective middle terms.
• TauCeti.ExactStructure.suspensionToStableOfPresentationsIso: the canonical natural isomorphism comparing two such choices.

Main results

• TauCeti.ExactStructure.projectiveStableFunctor_map_cokernelMap_eq: any extension of f to the injective middle terms induces the morphism InjectivePresentation.cokernelMap on cokernel terms, in the projective stable category.

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.

theorem TauCeti.ExactStructure.projectiveStableFunctor_map_cokernelMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X Y : C} (P : E.InjectivePresentation X) (Q : E.InjectivePresentation Y) (hQ : E.isProjective Q.I) (f : X ⟶ Y) (a : P.I ⟶ Q.I) (g : P.K ⟶ Q.K) (ha : CategoryTheory.CategoryStruct.comp P.i a = CategoryTheory.CategoryStruct.comp f Q.i) (hg : CategoryTheory.CategoryStruct.comp P.p g = CategoryTheory.CategoryStruct.comp a Q.p) : E.projectiveStableFunctor.map (P.cokernelMap Q f) = E.projectiveStableFunctor.map g

Any pair of morphisms a and g extending f : X ⟶ Y across relative injective presentations P of X and Q of Y induces InjectivePresentation.cokernelMap on the cokernel terms, once the middle term of Q is relatively projective.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableFunctor_map_cokernelMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X : C} (P : E.InjectivePresentation X) (hP : E.isProjective P.I) : E.projectiveStableFunctor.map (P.cokernelMap P (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj P.K)

In the projective stable category, the identity induces the identity of the cokernel term of a relative injective presentation.

theorem TauCeti.ExactStructure.projectiveStableFunctor_map_cokernelMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X Y Z : C} (P : E.InjectivePresentation X) (Q : E.InjectivePresentation Y) (R : E.InjectivePresentation Z) (hR : E.isProjective R.I) (f : X ⟶ Y) (g : Y ⟶ Z) : E.projectiveStableFunctor.map (P.cokernelMap R (CategoryTheory.CategoryStruct.comp f g)) = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.cokernelMap Q f)) (E.projectiveStableFunctor.map (Q.cokernelMap R g))

In the projective stable category, the morphisms induced on cokernel terms of relative injective presentations compose.

noncomputable def TauCeti.ExactStructure.InjectivePresentation.projectiveStableIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X : C} (P Q : E.InjectivePresentation X) (hP : E.isProjective P.I) (hQ : E.isProjective Q.I) : E.projectiveStableFunctor.obj P.K ≅ E.projectiveStableFunctor.obj Q.K

The canonical isomorphism, in the projective stable category, between the cokernel terms of two relative injective presentations of the same object with relatively projective middle terms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ExactStructure.InjectivePresentation.projectiveStableIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X : C} (P Q : E.InjectivePresentation X) (hP : E.isProjective P.I) (hQ : E.isProjective Q.I) : (P.projectiveStableIso Q hP hQ).hom = E.projectiveStableFunctor.map (P.cokernelMap Q (CategoryTheory.CategoryStruct.id X))

The comparison isomorphism is induced by the identity morphism of the presented object.

@[simp]

theorem TauCeti.ExactStructure.InjectivePresentation.projectiveStableIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X : C} (P Q : E.InjectivePresentation X) (hP : E.isProjective P.I) (hQ : E.isProjective Q.I) : (P.projectiveStableIso Q hP hQ).inv = E.projectiveStableFunctor.map (Q.cokernelMap P (CategoryTheory.CategoryStruct.id X))

The inverse comparison isomorphism is the one induced in the opposite direction.

theorem TauCeti.ExactStructure.projectiveStableIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X Y : C} (P P' : E.InjectivePresentation X) (Q Q' : E.InjectivePresentation Y) (hP : E.isProjective P.I) (hP' : E.isProjective P'.I) (hQ : E.isProjective Q.I) (hQ' : E.isProjective Q'.I) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.cokernelMap Q f)) (Q.projectiveStableIso Q' hQ hQ').hom = CategoryTheory.CategoryStruct.comp (P.projectiveStableIso P' hP hP').hom (E.projectiveStableFunctor.map (P'.cokernelMap Q' f))

The comparison isomorphisms between two choices of relative injective presentation are natural: they turn the morphism induced by f on one choice into the morphism induced by f on the other.

noncomputable def TauCeti.ExactStructure.suspensionToStableOfPresentations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) : CategoryTheory.Functor C E.ProjectiveStableCategory

The functor to the projective stable category sending an object to the cokernel term of a chosen relative injective presentation with relatively projective middle term, and a morphism to the morphism it induces there. For a Frobenius exact structure this is Happel's suspension, before it is descended to an endofunctor of the stable category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ExactStructure.suspensionToStableOfPresentations_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (P : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) (X : C) : (E.suspensionToStableOfPresentations P hP).obj X = E.projectiveStableFunctor.obj (P X).K

The object formula for the functor determined by a choice of relative injective presentations.

@[simp]

theorem TauCeti.ExactStructure.suspensionToStableOfPresentations_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (P : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) {X Y : C} (f : X ⟶ Y) : (E.suspensionToStableOfPresentations P hP).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((P X).cokernelMap (P Y) f)) (CategoryTheory.eqToHom ⋯))

The morphism formula for the functor determined by a choice of relative injective presentations.

instance TauCeti.ExactStructure.suspensionToStableOfPresentations_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (P : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) : (E.suspensionToStableOfPresentations P hP).Additive

noncomputable def TauCeti.ExactStructure.suspensionToStableOfPresentationsIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P Q : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) (hQ : ∀ (X : C), E.isProjective (Q X).I) : E.suspensionToStableOfPresentations P hP ≅ E.suspensionToStableOfPresentations Q hQ

Two choices of relative injective presentations with relatively projective middle terms give canonically naturally isomorphic functors to the projective stable category.

Equations

• E.suspensionToStableOfPresentationsIso P Q hP hQ = CategoryTheory.NatIso.ofComponents (fun (X : C) => (P X).projectiveStableIso (Q X) ⋯ ⋯) ⋯

@[simp]

theorem TauCeti.ExactStructure.suspensionToStableOfPresentationsIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (P Q : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) (hQ : ∀ (X : C), E.isProjective (Q X).I) (X : C) : (E.suspensionToStableOfPresentationsIso P Q hP hQ).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((P X).projectiveStableIso (Q X) ⋯ ⋯).hom (CategoryTheory.eqToHom ⋯))

The components of the comparison of two choices of relative injective presentations are the comparison isomorphisms of the two presentations of each object.

@[simp]

theorem TauCeti.ExactStructure.suspensionToStableOfPresentationsIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (P Q : (X : C) → E.InjectivePresentation X) (hP : ∀ (X : C), E.isProjective (P X).I) (hQ : ∀ (X : C), E.isProjective (Q X).I) (X : C) : (E.suspensionToStableOfPresentationsIso P Q hP hQ).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((P X).projectiveStableIso (Q X) ⋯ ⋯).inv (CategoryTheory.eqToHom ⋯))

The inverse of the comparison of two choices of relative injective presentations is the comparison taken in the other order.