Bridgeland Stability Conditions

6.1. TStructure: AbelianSubcategoryImageFactorisation🔗

6.1.1. exists_distinguished_triangle_of_image_factorisation🔗

Image factorisation triangle. Given a distinguished triangle \iota(X_1) \xrightarrow{\iota(f_1)} \iota(X_2) \xrightarrow{f_2} X_3 \xrightarrow{f_3} \iota(X_1)[1] with X_1, X_2 in the abelian subcategory, and a decomposition of X_3 as \iota(K)[1] \xrightarrow{\alpha} X_3 \xrightarrow{\beta} \iota(Q) \xrightarrow{\gamma} \iota(K)[1][1] (also distinguished), there exist: an object I in the subcategory, morphisms i \colon I \to X_2, \delta \colon \iota(Q) \to \iota(I)[1], m_1 \colon X_1 \to I, and m_3 \colon \iota(I) \to \iota(K)[1] such that (1) \iota(i), \iota(\pi_Q), \delta form a distinguished triangle, (2) \iota(\iota_K), \iota(m_1), -m_3 form a distinguished triangle, and (3) m_1 \circ i = f_1.

Proof: The proof applies the octahedral axiom to the factorisation f_2 \circ \beta = \iota(\pi_Q). The epi \pi_Q yields the first triangle via exists_distinguished_triangle_of_epi. The octahedron produces the second triangle and the factorisation m_1 \circ i = f_1. The key lifting steps use fullness of \iota \circ \operatorname{shift} to extract m_1 and m_3 as morphisms in the ambient category, and IsTriangulated to access the octahedral axiom.

🔗theorem
CategoryTheory.Triangulated.AbelianSubcategory.exists_distinguished_triangle_of_image_factorisation.{v_1,
    u_1, v_2, u_2}
  {C : Type u_1} {A : Type u_2} [CategoryTheory.Category.{v_1, u_1} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C]
  [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C}
  (hι :
    ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄
      (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)),
      n < 0 → f = 0)
  [CategoryTheory.Preadditive A] [ι.Full] [ι.Faithful] [ι.Additive]
  (hA :
    CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism
        ι =
      ⊤)
  [CategoryTheory.IsTriangulated C] {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C}
  (f₂ : ι.obj X₂ ⟶ X₃)
  (f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁))
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  {K Q : A} (α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃)
  (β : X₃ ⟶ ι.obj Q)
  {γ :
    ι.obj Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))}
  (hT' :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ∃ I i δ m₁ m₃,
    CategoryTheory.Pretriangulated.Triangle.mk (ι.map i)
          (ι.map
            (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β))
          δ ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Pretriangulated.Triangle.mk
            (ι.map
              (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α))
            (ι.map m₁) (-m₃) ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles ∧
        CategoryTheory.CategoryStruct.comp m₁ i = f₁
CategoryTheory.Triangulated.AbelianSubcategory.exists_distinguished_triangle_of_image_factorisation.{v_1,
    u_1, v_2, u_2}
  {C : Type u_1} {A : Type u_2}
  [CategoryTheory.Category.{v_1, u_1} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C}
  (hι :
    ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄
      (f :
        ι.obj X ⟶
          (CategoryTheory.shiftFunctor C
                n).obj
            (ι.obj Y)),
      n < 0 → f = 0)
  [CategoryTheory.Preadditive A] [ι.Full]
  [ι.Faithful] [ι.Additive]
  (hA :
    CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism
        ι =
      ⊤)
  [CategoryTheory.IsTriangulated C]
  {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C}
  (f₂ : ι.obj X₂ ⟶ X₃)
  (f₃ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        (ι.obj X₁))
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        (ι.map f₁) f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  {K Q : A}
  (α :
    (CategoryTheory.shiftFunctor C 1).obj
        (ι.obj K) ⟶
      X₃)
  (β : X₃ ⟶ ι.obj Q)
  {γ :
    ι.obj Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          (ι.obj K))}
  (hT' :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ∃ I i δ m₁ m₃,
    CategoryTheory.Pretriangulated.Triangle.mk
          (ι.map i)
          (ι.map
            (CategoryTheory.Triangulated.AbelianSubcategory.πQ
              f₂ β))
          δ ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Pretriangulated.Triangle.mk
            (ι.map
              (CategoryTheory.Triangulated.AbelianSubcategory.ιK
                f₃ α))
            (ι.map m₁) (-m₃) ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles ∧
        CategoryTheory.CategoryStruct.comp
            m₁ i =
          f₁

Something wrong, better idea? Suggest a change