Documentation

Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Spectral objects attached to t-structures #

Let C be a triangulated category equipped with a t-structure t. We define a functor t.ω₁ : ComposableArrows EInt 1 ⥤ C ⥤ C which sends a map a ⟶ b in EInt (i.e. a ≤ b) to the functor t.eTruncLT.obj b ⋙ t.eTruncGE.obj a. (Roughly speaking, we "keep" the t-homology only in degree n such that a ≤ n < b.) When we have two composable morphisms f : a ⟶ b and g : b ⟶ c in EInt, we define a connecting homomorphism ω₁δ : t.ω₁.obj (mk₁ g) ⟶ t.ω₁.obj (mk₁ f) ⋙ shiftFunctor C (1 : ℤ), and this gives distinguished triangles that are functorial both in X : C and a ⟶ b ⟶ c in ComposableArrows EInt 2.

In other words, for each X : C, we define a spectral object t.spectralObject X : SpectralObject C EInt in the triangulated category C, and this extends to a functor t.spectralObjectFunctor : C ⥤ SpectralObject C EInt.

source
noncomputable def CategoryTheory.Triangulated.TStructure.ω₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) :
Functor (ComposableArrows EInt 1) (Functor C C)

Given a t-structure t on a triangulated category C, this is the functor ComposableArrows EInt 1 ⥤ C ⥤ C which sends an arrows a ⟶ b in EInt to the functor t.eTruncLT.obj b ⋙ t.eTruncGE.obj a.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Triangulated.TStructure.ω₁_obj {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (D : ComposableArrows EInt 1) :
    t.ω₁.obj D = (t.eTruncLT.obj (D.obj 1)).comp (t.eTruncGE.obj (D.obj 0))
    source
    @[simp]
    theorem CategoryTheory.Triangulated.TStructure.ω₁_map {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X✝ Y✝ : ComposableArrows EInt 1} (φ : X✝ ⟶ Y✝) :
    t.ω₁.map φ = t.eTruncLT.map (φ.app 1) ◫ t.eTruncGE.map (φ.app 0)
    source
    noncomputable def CategoryTheory.Triangulated.TStructure.ω₁δ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) :
    t.ω₁.obj (ComposableArrows.mk₁ (homOfLE hbc)) ⟶ (t.ω₁.obj (ComposableArrows.mk₁ (homOfLE hab))).comp (shiftFunctor C 1)

    The connecting homomorphism (as a natural transformation) for the spectral objects attached to the objects of a triangulated equipped with a t-structure.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Triangulated.TStructure.ω₁δ_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (X : C) :
      (t.ω₁δ a b c hab hbc).app X = CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj X))) (CategoryStruct.comp ((t.eTruncGEδLT.app b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))) (CategoryStruct.comp ((shiftFunctor C 1).map ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X))) ((shiftFunctor C 1).map ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app X))))))
      source
      theorem CategoryTheory.Triangulated.TStructure.ω₁δ_naturality {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (a' b' c' : EInt) (hab' : a' ≤ b') (hbc' : b' ≤ c') (φ : ComposableArrows.mk₂ (homOfLE hab) (homOfLE hbc) ⟶ ComposableArrows.mk₂ (homOfLE hab') (homOfLE hbc')) :
      CategoryStruct.comp (t.ω₁.map (ComposableArrows.homMk₁ (φ.app 1) (φ.app 2) ⋯)) (t.ω₁δ a' b' c' hab' hbc') = CategoryStruct.comp (t.ω₁δ a b c hab hbc) (Functor.whiskerRight (t.ω₁.map (ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C 1))
      source
      theorem CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (a' b' c' : EInt) (hab' : a' ≤ b') (hbc' : b' ≤ c') (φ : ComposableArrows.mk₂ (homOfLE hab) (homOfLE hbc) ⟶ ComposableArrows.mk₂ (homOfLE hab') (homOfLE hbc')) {Z : Functor C C} (h : (t.ω₁.obj (ComposableArrows.mk₁ (homOfLE hab'))).comp (shiftFunctor C 1) ⟶ Z) :
      CategoryStruct.comp (t.ω₁.map (ComposableArrows.homMk₁ (φ.app 1) (φ.app 2) ⋯)) (CategoryStruct.comp (t.ω₁δ a' b' c' hab' hbc') h) = CategoryStruct.comp (t.ω₁δ a b c hab hbc) (CategoryStruct.comp (Functor.whiskerRight (t.ω₁.map (ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C 1)) h)
      source
      noncomputable def CategoryTheory.Triangulated.TStructure.triangleω₁δ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) :
      Functor C (Pretriangulated.Triangle C)

      The functorial (distinguished) triangles that are part of the spectral object attached to objects in a triangulated category equipped with a t-structure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) :
        ((t.triangleω₁δ a b c hab hbc).obj j).obj₂ = (t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj j)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) :
        ((t.triangleω₁δ a b c hab hbc).map φ).hom₁ = (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map φ)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) :
        ((t.triangleω₁δ a b c hab hbc).map φ).hom₂ = (t.eTruncGE.obj a).map ((t.eTruncLT.obj c).map φ)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) :
        ((t.triangleω₁δ a b c hab hbc).obj j).obj₃ = (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj j)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) :
        ((t.triangleω₁δ a b c hab hbc).obj j).mor₂ = (t.eTruncGE.map (homOfLE hab)).app ((t.eTruncLT.obj c).obj j)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) :
        ((t.triangleω₁δ a b c hab hbc).obj j).mor₃ = CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj j))) (CategoryStruct.comp ((t.eTruncGEδLT.app b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj j))) (CategoryStruct.comp ((shiftFunctor C 1).map ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj j))) ((shiftFunctor C 1).map ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app j))))))
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) :
        ((t.triangleω₁δ a b c hab hbc).obj j).mor₁ = (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app j)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) :
        ((t.triangleω₁δ a b c hab hbc).map φ).hom₃ = (t.eTruncGE.obj b).map ((t.eTruncLT.obj c).map φ)
        source
        @[simp]
        theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) :
        ((t.triangleω₁δ a b c hab hbc).obj j).obj₁ = (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj j)
        source
        noncomputable def CategoryTheory.Triangulated.TStructure.triangleω₁δObjIso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (X : C) :
        (t.triangleω₁δ a b c hab hbc).obj X ≅ (t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (ComposableArrows.mk₁ (homOfLE ⋯))).obj X)

        The triangle (t.triangleω₁δ a b c hab hbc).obj X is isomorphic to the (distinguished) triangle obtained by applying the functor t.eTriangleLTGE.obj b to the object (t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem CategoryTheory.Triangulated.TStructure.triangleω₁δ_distinguished {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (X : C) :
          (t.triangleω₁δ a b c hab hbc).obj X ∈ Pretriangulated.distinguishedTriangles
          source
          noncomputable def CategoryTheory.Triangulated.TStructure.spectralObject {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) :
          SpectralObject C EInt

          The spectral object attached to an object X : C in a category equipped with a t-structure. It consists of all truncations of X.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Triangulated.TStructure.spectralObject_ω₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) :
            (t.spectralObject X).ω₁ = t.ω₁.comp ((evaluation C C).obj X)
            source
            @[simp]
            theorem CategoryTheory.Triangulated.TStructure.spectralObject_δ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) {a b c : EInt} (f : a ⟶ b) (g : b ⟶ c) :
            (t.spectralObject X).δ f g = (t.ω₁δ a b c ⋯ ⋯).app X
            source
            noncomputable def CategoryTheory.Triangulated.TStructure.spectralObjectFunctor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] :
            Functor C (SpectralObject C EInt)

            The spectral object attached to an object X : C in a category equipped with a t-structure, as a functor C ⥤ SpectralObject C EInt.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_obj {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) :
              t.spectralObjectFunctor.obj X = t.spectralObject X
              source
              @[simp]
              theorem CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_map_hom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) :
              (t.spectralObjectFunctor.map φ).hom = t.ω₁.whiskerLeft ((evaluation C C).map φ)