Stable functors commute with suspension #
An exact functor between Frobenius exact categories which preserves projective-injective objects descends to their stable categories. This file constructs the canonical comparison between that stable functor and suspension, and proves compatibility with the connecting maps of conflations.
Apply the original functor to a chosen injective presentation X ⟶ I(X) ⟶ ΣX. Its image
is an injective presentation of F(X), because the functor preserves conflations and
projective-injective objects. Independence of injective presentations then identifies F(ΣX)
with Σ(F(X)) in the target stable category. These identifications are natural and descend to
the source stable category.
Main definitions #
TauCeti.StableConflationExact.mapSuspensionPresentation: the image of the chosen suspension presentation under a stable conflation-exact functor.TauCeti.StableConflationExact.stableSuspensionCompStableFunctorIso: the natural isomorphism comparing suspension composed with the induced stable functor to the opposite composite.
References #
- Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
noncomputable def
TauCeti.StableConflationExact.mapSuspensionPresentation
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(X : C)
:
E'.InjectivePresentation (F.obj X)
Applying a stable conflation-exact functor to the chosen suspension presentation of X
gives an injective presentation of F.obj X in the target exact category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.StableConflationExact.mapSuspensionPresentation_I
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(X : C)
:
The middle term of the mapped suspension presentation is the image of the chosen middle term.
@[simp]
theorem
TauCeti.StableConflationExact.mapSuspensionPresentation_K
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(X : C)
:
The cokernel term of the mapped suspension presentation is the image of the chosen suspension object.
@[simp]
theorem
TauCeti.StableConflationExact.mapSuspensionPresentation_i
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(X : C)
:
The inflation in the mapped suspension presentation is the image of the chosen inflation.
@[simp]
theorem
TauCeti.StableConflationExact.mapSuspensionPresentation_p
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(X : C)
:
The deflation in the mapped suspension presentation is the image of the chosen deflation.
theorem
TauCeti.StableConflationExact.isProjective_I_mapSuspensionPresentation
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(X : C)
:
E'.isProjective (hF.mapSuspensionPresentation hE X).I
The middle term of the mapped suspension presentation remains projective.
@[simp]
theorem
TauCeti.StableConflationExact.map_connectingMap_comp_suspensionComparison
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
{S : CategoryTheory.ShortComplex C}
(hS : E.Conflation S)
:
CategoryTheory.CategoryStruct.comp (E'.projectiveStableFunctor.map (F.map (hE.connectingMap hS)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(E'.projectiveStableFunctor.map
((hF.mapSuspensionPresentation hE S.X₁).cokernelMap (hE'.suspensionPresentation (F.obj S.X₁))
(CategoryTheory.CategoryStruct.id (F.obj S.X₁))))) = E'.projectiveStableFunctor.map (hE'.connectingMap ⋯)
The image of a connecting map, followed by the comparison from the mapped suspension presentation to the chosen target presentation, is the connecting map of the image conflation in the target stable category.
@[simp]
theorem
TauCeti.StableConflationExact.map_connectingMap_comp_suspensionComparison_assoc
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
{S : CategoryTheory.ShortComplex C}
(hS : E.Conflation S)
{Z : E'.ProjectiveStableCategory}
(h : E'.projectiveStableFunctor.obj (hE'.suspensionPresentation (F.obj S.X₁)).K ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (E'.projectiveStableFunctor.map (F.map (hE.connectingMap hS)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp
(E'.projectiveStableFunctor.map
((hF.mapSuspensionPresentation hE S.X₁).cokernelMap (hE'.suspensionPresentation (F.obj S.X₁))
(CategoryTheory.CategoryStruct.id (F.obj S.X₁))))
h)) = CategoryTheory.CategoryStruct.comp (E'.projectiveStableFunctor.map (hE'.connectingMap ⋯)) h
The image of a connecting map, followed by the comparison from the mapped suspension presentation to the chosen target presentation, is the connecting map of the image conflation in the target stable category.
noncomputable def
TauCeti.StableConflationExact.stableSuspensionCompStableFunctorIso
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
:
The stable functor induced by a stable conflation-exact functor commutes with suspension.
Its component at X is the canonical comparison from the image of the chosen suspension
presentation of X to the chosen suspension presentation of F.obj X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.StableConflationExact.stableSuspensionCompStableFunctorIso_hom_app
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
(X : C)
:
(hF.stableSuspensionCompStableFunctorIso hE hE').hom.app (E.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp
(hE'.projectiveStableIsoSuspensionObj (hF.mapSuspensionPresentation hE X)).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)))))
On an object represented by X, the suspension comparison is the canonical comparison
between the mapped suspension presentation and the chosen presentation of F.obj X.
@[simp]
theorem
TauCeti.StableConflationExact.stableSuspensionCompStableFunctorIso_inv_app
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{E : ExactStructure C}
{E' : ExactStructure D}
{F : CategoryTheory.Functor C D}
[F.Additive]
(hF : StableConflationExact E E' F)
(hE : E.IsFrobenius)
(hE' : E'.IsFrobenius)
(X : C)
:
(hF.stableSuspensionCompStableFunctorIso hE hE').inv.app (E.projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (hE'.projectiveStableIsoSuspensionObj (hF.mapSuspensionPresentation hE X)).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)))))
On an object represented by X, the inverse suspension comparison is the inverse canonical
comparison, with the object-identification maps reversed.