Documentation

TauCeti.CategoryTheory.Exact.Stable.Connecting

The connecting morphism of a conflation in a Frobenius stable category #

Let E be a Frobenius exact structure and let X ⟶ Y ⟶ Z be a conflation. The inflation X ⟶ I(X) of the chosen suspension presentation extends along X ⟶ Y to a map Y ⟶ I(X), since I(X) is injective, and this extension induces a map Z ⟶ ΣX on cokernels. In the projective stable category the result does not depend on the chosen extension. This is the connecting morphism of Happel's standard triangle

X ⟶ Y ⟶ Z ⟶ ΣX.

This file constructs the connecting morphism, shows that it is independent of choices in the stable category, that the consecutive composites Y ⟶ Z ⟶ ΣX and Z ⟶ ΣX ⟶ ΣY vanish there, and that it is natural in morphisms of conflations. The last fact is packaged as a natural transformation between functors on the category of conflations. In the stable category, the connecting morphism of the chosen suspension presentation itself is the identity of ΣX, and that of a split conflation is zero.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ExactStructure.IsFrobenius.connectingMiddleMap {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) :
S.X₂ ⟶ hE.suspensionInjective S.X₁

A chosen extension Y ⟶ I(X) of the suspension inflation X ⟶ I(X) along the inflation X ⟶ Y of a conflation X ⟶ Y ⟶ Z.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.IsFrobenius.f_comp_connectingMiddleMap {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) :
    CategoryTheory.CategoryStruct.comp S.f (hE.connectingMiddleMap hS) = hE.suspensionInflation S.X₁

    The chosen middle map extends the suspension inflation along the inflation of S.

    source
    @[simp]
    theorem TauCeti.ExactStructure.IsFrobenius.f_comp_connectingMiddleMap_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.IsFrobenius) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) {Z : C} (h : hE.suspensionInjective S.X₁ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp S.f (CategoryTheory.CategoryStruct.comp (hE.connectingMiddleMap hS) h) = CategoryTheory.CategoryStruct.comp (hE.suspensionInflation S.X₁) h

    The chosen middle map extends the suspension inflation along the inflation of S.

    source
    noncomputable def TauCeti.ExactStructure.IsFrobenius.connectingMap {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) :
    S.X₃ ⟶ hE.suspensionObj S.X₁

    The connecting map Z ⟶ ΣX of a conflation X ⟶ Y ⟶ Z, induced on cokernels by the chosen extension Y ⟶ I(X). Its image in the stable category is independent of that choice.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ExactStructure.IsFrobenius.g_comp_connectingMap {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) :
      CategoryTheory.CategoryStruct.comp S.g (hE.connectingMap hS) = CategoryTheory.CategoryStruct.comp (hE.connectingMiddleMap hS) (hE.suspensionDeflation S.X₁)

      The connecting map makes the square on the two deflations commute.

      source
      @[simp]
      theorem TauCeti.ExactStructure.IsFrobenius.g_comp_connectingMap_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.IsFrobenius) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) {Z : C} (h : hE.suspensionObj S.X₁ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp S.g (CategoryTheory.CategoryStruct.comp (hE.connectingMap hS) h) = CategoryTheory.CategoryStruct.comp (hE.connectingMiddleMap hS) (CategoryTheory.CategoryStruct.comp (hE.suspensionDeflation S.X₁) h)

      The connecting map makes the square on the two deflations commute.

      source
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_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.IsFrobenius) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (a : S.X₂ ⟶ hE.suspensionInjective S.X₁) (δ : S.X₃ ⟶ hE.suspensionObj S.X₁) (ha : CategoryTheory.CategoryStruct.comp S.f a = hE.suspensionInflation S.X₁) (hδ : CategoryTheory.CategoryStruct.comp S.g δ = CategoryTheory.CategoryStruct.comp a (hE.suspensionDeflation S.X₁)) :
      E.projectiveStableFunctor.map (hE.connectingMap hS) = E.projectiveStableFunctor.map δ

      Any map Z ⟶ ΣX induced by some extension Y ⟶ I(X) of the suspension inflation agrees with connectingMap in the stable category.

      source
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_eq_connectingMap_comp {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (P : E.InjectivePresentation S.X₁) (a : S.X₂ ⟶ P.I) (δ : S.X₃ ⟶ P.K) (ha : CategoryTheory.CategoryStruct.comp S.f a = P.i) (hδ : CategoryTheory.CategoryStruct.comp S.g δ = CategoryTheory.CategoryStruct.comp a P.p) :
      E.projectiveStableFunctor.map δ = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hS)) (hE.projectiveStableIsoSuspensionObj P).inv

      The connecting map may be computed from any relative injective presentation X ⟶ P.I ⟶ P.K of the first term X of the conflation: a map δ : Z ⟶ P.K induced on cokernels by an extension Y ⟶ P.I of the inflation of P is the connecting map, followed by the comparison of the chosen suspension with P.K, in the stable category.

      source
      @[simp]
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_g_comp_connectingMap {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) :
      CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map S.g) (E.projectiveStableFunctor.map (hE.connectingMap hS)) = 0

      The composite Y ⟶ Z ⟶ ΣX of the standard triangle vanishes in the stable category: it factors through the injective I(X).

      source
      @[simp]
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_comp_cokernelMap {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) :
      CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hS)) (E.projectiveStableFunctor.map ((hE.suspensionPresentation S.X₁).cokernelMap (hE.suspensionPresentation S.X₂) S.f)) = 0

      The composite Z ⟶ ΣX ⟶ ΣY of the standard triangle vanishes in the stable category.

      source
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_naturality {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) {T : CategoryTheory.ShortComplex C} (hT : E.Conflation T) (φ : S ⟶ T) :
      E.projectiveStableFunctor.map (CategoryTheory.CategoryStruct.comp φ.τ₃ (hE.connectingMap hT)) = E.projectiveStableFunctor.map (CategoryTheory.CategoryStruct.comp (hE.connectingMap hS) ((hE.suspensionPresentation S.X₁).cokernelMap (hE.suspensionPresentation T.X₁) φ.τ₁))

      The connecting map is natural in morphisms of conflations, in the stable category: for φ : S ⟶ T, the square with φ.τ₃ and the suspension of φ.τ₁ commutes.

      source
      theorem TauCeti.ExactStructure.IsFrobenius.exists_stable_connecting_square {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) {S T : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (hT : E.Conflation T) (a : E.projectiveStableFunctor.obj S.X₁ ⟶ E.projectiveStableFunctor.obj T.X₁) (b : E.projectiveStableFunctor.obj S.X₂ ⟶ E.projectiveStableFunctor.obj T.X₂) (hab : CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map S.f) b = CategoryTheory.CategoryStruct.comp a (E.projectiveStableFunctor.map T.f)) :
      ∃ (c : E.projectiveStableFunctor.obj S.X₃ ⟶ E.projectiveStableFunctor.obj T.X₃), CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map S.g) c = CategoryTheory.CategoryStruct.comp b (E.projectiveStableFunctor.map T.g) ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hS)) (CategoryTheory.eqToHom ⋯)) (hE.stableSuspension.map a) = CategoryTheory.CategoryStruct.comp c (CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap hT)) (CategoryTheory.eqToHom ⋯))

      A stable commutative square between conflations extends across both the cokernel arrows and the connecting arrows.

      source
      @[simp]
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_suspensionPresentation {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.projectiveStableFunctor.map (hE.connectingMap ⋯) = CategoryTheory.CategoryStruct.id (E.projectiveStableFunctor.obj { X₁ := X, X₂ := (hE.suspensionPresentation X).I, X₃ := (hE.suspensionPresentation X).K, f := (hE.suspensionPresentation X).i, g := (hE.suspensionPresentation X).p, zero := ⋯ }.X₃)

      For the chosen suspension presentation X ⟶ I(X) ⟶ ΣX itself, the connecting map is the identity of ΣX in the stable category.

      source
      @[simp]
      theorem TauCeti.ExactStructure.IsFrobenius.projectiveStableFunctor_map_connectingMap_eq_zero_of_isSplitEpi {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) [CategoryTheory.IsSplitEpi S.g] :
      E.projectiveStableFunctor.map (hE.connectingMap hS) = 0

      The connecting map of a conflation whose deflation is a split epimorphism, in particular of a split conflation, is zero in the stable category.

      source
      noncomputable def TauCeti.ExactStructure.IsFrobenius.stableConnecting {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) :
      (ConflationClass.ConflationCategory.π₃ E.toConflationClass).comp E.projectiveStableFunctor ⟶ (ConflationClass.ConflationCategory.π₁ E.toConflationClass).comp hE.suspensionToStable

      The connecting maps of all conflations, as a natural transformation from the third term to the suspension of the first term, both taken in the stable category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.ExactStructure.IsFrobenius.stableConnecting_app {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) (S : E.ConflationCategory) :
        hE.stableConnecting.app S = CategoryTheory.CategoryStruct.comp (E.projectiveStableFunctor.map (hE.connectingMap ⋯)) (CategoryTheory.eqToHom ⋯)

        The component of stableConnecting at a conflation is its connecting map, read in the stable category.