Projective presentations in a projective stable category

Let E be an exact structure and let P and Q be relative projective presentations P.K ⟶ P.P ⟶ X and Q.K ⟶ Q.P ⟶ Y. A morphism f : X ⟶ Y lifts to the projective middle terms and hence induces ProjectivePresentation.kernelMap on the kernel terms. The lift is not unique, but the induced kernel map is unique in the projective stable quotient.

Consequently, the kernel terms of two projective presentations of the same object are canonically isomorphic in the stable category. A choice of projective presentation for every object produces an additive functor to the stable category, and any two choices produce canonically naturally isomorphic functors. For an exact structure with enough projectives, this is the loop construction before it is descended to an endofunctor of the stable category.

Main definitions

• TauCeti.ExactStructure.ProjectivePresentation.projectiveStableIso: the canonical isomorphism between the kernel terms of two relative projective presentations of the same object, in the projective stable category.
• TauCeti.ExactStructure.loopToStableOfPresentations: the functor to the projective stable category determined by a choice of relative projective presentation for every object.
• TauCeti.ExactStructure.loopToStableOfPresentationsIso: the canonical natural isomorphism comparing two choices.

Main results

• TauCeti.ExactStructure.projectiveStableFunctor_map_kernelMap_eq: any compatible maps between projective presentations inducing f give ProjectivePresentation.kernelMap in the projective stable category.

References

• TauCeti.CategoryTheory.Exact.Stable.Presentation, whose injective-presentation comparison API is the dual template for this projective-presentation construction.
• 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_kernelMap_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.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) (a : P.P ⟶ Q.P) (g : P.K ⟶ Q.K) (ha : CategoryTheory.CategoryStruct.comp a Q.p = CategoryTheory.CategoryStruct.comp P.p f) (hg : CategoryTheory.CategoryStruct.comp g Q.i = CategoryTheory.CategoryStruct.comp P.i a) : E.projectiveStableFunctor.map (P.kernelMap Q f) = E.projectiveStableFunctor.map g

Any compatible maps a and g between relative projective presentations P of X and Q of Y inducing f : X ⟶ Y give ProjectivePresentation.kernelMap on the kernel terms in the projective stable category.

@[simp]

theorem TauCeti.ExactStructure.projectiveStableFunctor_map_kernelMap_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.ProjectivePresentation X) : E.projectiveStableFunctor.map (P.kernelMap 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 kernel term of a relative projective presentation.

theorem TauCeti.ExactStructure.projectiveStableFunctor_map_kernelMap_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.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (R : E.ProjectivePresentation Z) (f : X ⟶ Y) (g : Y ⟶ Z) : E.projectiveStableFunctor.map (P.kernelMap R (CategoryTheory.CategoryStruct.comp f g)) = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.kernelMap Q f)) (E.projectiveStableFunctor.map (Q.kernelMap R g))

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

noncomputable def TauCeti.ExactStructure.ProjectivePresentation.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.ProjectivePresentation X) : E.projectiveStableFunctor.obj P.K ≅ E.projectiveStableFunctor.obj Q.K

The canonical isomorphism, in the projective stable category, between the kernel terms of two relative projective presentations of the same object.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.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.ProjectivePresentation X) : (P.projectiveStableIso Q).hom = E.projectiveStableFunctor.map (P.kernelMap Q (CategoryTheory.CategoryStruct.id X))

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

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.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.ProjectivePresentation X) : (P.projectiveStableIso Q).inv = E.projectiveStableFunctor.map (Q.kernelMap P (CategoryTheory.CategoryStruct.id X))

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

theorem TauCeti.ExactStructure.ProjectivePresentation.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.ProjectivePresentation X) (Q Q' : E.ProjectivePresentation Y) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (P.kernelMap Q f)) (Q.projectiveStableIso Q').hom = CategoryTheory.CategoryStruct.comp (P.projectiveStableIso P').hom (E.projectiveStableFunctor.map (P'.kernelMap Q' f))

The comparison isomorphisms between two choices of relative projective presentation are natural with respect to the induced maps on their kernel terms.

noncomputable def TauCeti.ExactStructure.loopToStableOfPresentations {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.ProjectivePresentation X) : CategoryTheory.Functor C E.ProjectiveStableCategory

The functor to the projective stable category sending an object to the kernel term of a chosen relative projective presentation and a morphism to the morphism it induces there.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.loopToStableOfPresentations_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.ProjectivePresentation X) (X : C) : (E.loopToStableOfPresentations P).obj X = E.projectiveStableFunctor.obj (P X).K

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

@[simp]

theorem TauCeti.ExactStructure.loopToStableOfPresentations_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.ProjectivePresentation X) {X Y : C} (f : X ⟶ Y) : (E.loopToStableOfPresentations P).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map ((P X).kernelMap (P Y) f)) (CategoryTheory.eqToHom ⋯))

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

instance TauCeti.ExactStructure.loopToStableOfPresentations_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.ProjectivePresentation X) : (E.loopToStableOfPresentations P).Additive

noncomputable def TauCeti.ExactStructure.loopToStableOfPresentationsIso {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.ProjectivePresentation X) : E.loopToStableOfPresentations P ≅ E.loopToStableOfPresentations Q

Two choices of relative projective presentations give canonically naturally isomorphic functors to the projective stable category.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.loopToStableOfPresentationsIso_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.ProjectivePresentation X) (X : C) : (E.loopToStableOfPresentationsIso P Q).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 projective presentations are the comparison isomorphisms of the two presentations of each object.

@[simp]

theorem TauCeti.ExactStructure.loopToStableOfPresentationsIso_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.ProjectivePresentation X) (X : C) : (E.loopToStableOfPresentationsIso P Q).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 projective presentations is the comparison taken in the other order.