Bridgeland Stability Conditions

14.6. Deformation: FirstStrictSES🔗

14.6.1. semistable_of_iso🔗

If E is W-semistable of phase \psi and E \cong E', then E' is also W-semistable of phase \psi. Semistability is an isomorphism-invariant property: the interval membership, nonzero condition, K_0-class, and triangle inequality all transport across the isomorphism.

Proof: Each clause of the semistability predicate is transferred through the isomorphism: interval membership by prop_of_iso, nonzero by Iso.isZero_iff, W-phase equality by cl\_iso, and the triangle test by rotating the distinguished triangle through the isomorphism.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_of_iso.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  {E E' : C} (e : E ≅ E') {ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
    E' ψ
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_of_iso.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  {E E' : C} (e : E ≅ E') {ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C ssf E' ψ

Something wrong, better idea? Suggest a change

14.6.2. maxPhase_strictSubobject_ne_top_of_not_semistable🔗

In a non-W-semistable interval object X, a maximal-phase strict subobject M cannot be \top. If it were, then M \cong X via the subobject arrow, and the semistability of M (from maximal-phase selection) would transfer to X, contradicting the non-semistability assumption.

Proof: Assume M = \top. Then M \cong X via the subobject isomorphism, and semistable_of_iso transports the semistability of M (established by semistable_of_maxPhase_strictSubobject) to X, yielding a contradiction.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.maxPhase_strictSubobject_ne_top_of_not_semistable.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {M : CategoryTheory.Subobject X}
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj))
  (hM_ne : M ≠ ⊥) (hM_strict : CategoryTheory.IsStrictMono M.arrow)
  (hM_max :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊥ →
        CategoryTheory.IsStrictMono B.arrow →
          ssf.wPhase (CategoryTheory.Subobject.underlying.obj B).obj ≤
            ssf.wPhase (CategoryTheory.Subobject.underlying.obj M).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) :
  M ≠ ⊤
CategoryTheory.Triangulated.SkewedStabilityFunction.maxPhase_strictSubobject_ne_top_of_not_semistable.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {M : CategoryTheory.Subobject X}
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj))
  (hM_ne : M ≠ ⊥)
  (hM_strict :
    CategoryTheory.IsStrictMono M.arrow)
  (hM_max :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊥ →
        CategoryTheory.IsStrictMono
            B.arrow →
          ssf.wPhase
              (CategoryTheory.Subobject.underlying.obj
                  B).obj ≤
            ssf.wPhase
              (CategoryTheory.Subobject.underlying.obj
                  M).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F) :
  M ≠ ⊤

Something wrong, better idea? Suggest a change

14.6.3. phase_gt_of_maxPhase_strictSubobject_of_not_semistable🔗

In a non-W-semistable interval object X, a maximal-phase strict subobject M has W-phase strictly larger than that of X: \psi(X) < \psi(M). If not, the phase ordering on all strict subobjects combined with the semistable characterization would force X itself to be semistable.

Proof: By contradiction: if \psi(M) \le \psi(X), then every nonzero strict subobject K \hookrightarrow X (appearing in a distinguished triangle) has \psi(K) \le \psi(M) \le \psi(X), which is exactly the triangle inequality characterizing semistability of X.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_gt_of_maxPhase_strictSubobject_of_not_semistable.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {M : CategoryTheory.Subobject X}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj))
  (hM_max :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊥ →
        CategoryTheory.IsStrictMono B.arrow →
          ssf.wPhase (CategoryTheory.Subobject.underlying.obj B).obj ≤
            ssf.wPhase (CategoryTheory.Subobject.underlying.obj M).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) :
  ssf.wPhase X.obj <
    ssf.wPhase (CategoryTheory.Subobject.underlying.obj M).obj
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_gt_of_maxPhase_strictSubobject_of_not_semistable.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {M : CategoryTheory.Subobject X}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj))
  (hM_max :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊥ →
        CategoryTheory.IsStrictMono
            B.arrow →
          ssf.wPhase
              (CategoryTheory.Subobject.underlying.obj
                  B).obj ≤
            ssf.wPhase
              (CategoryTheory.Subobject.underlying.obj
                  M).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F) :
  ssf.wPhase X.obj <
    ssf.wPhase
      (CategoryTheory.Subobject.underlying.obj
          M).obj

Something wrong, better idea? Suggest a change

14.6.4. exists_first_strictShortExact_of_not_semistable_of_strictArtinian🔗

Strict-Artinian descent for the first strict short exact sequence (Bridgeland S7): given a non-W-semistable interval object X that is strict-Artinian, there exists a proper strict subobject M with M \ne \bot, M \ne \top, \psi(M) > \psi(X), M is W-semistable, and the inclusion M \hookrightarrow X gives a strict short exact sequence 0 \to M \to X \to X/M \to 0.

Proof: Well-founded induction on the strict-subobject lattice. At each step, find a strict subobject of larger phase than the current object. If it is semistable, stop; otherwise, descend to a smaller strict subobject via the existence of a phase-raising destabilizing strict subobject. The descent terminates by the well-foundedness of the strict-subobject partial order.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_first_strictShortExact_of_not_semistable_of_strictArtinian.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  [CategoryTheory.IsStrictArtinianObject X]
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) :
  ∃ M,
    M ≠ ⊥ ∧
      M ≠ ⊤ ∧
        CategoryTheory.IsStrictMono M.arrow ∧
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf (CategoryTheory.Subobject.underlying.obj M).obj
              (ssf.wPhase
                (CategoryTheory.Subobject.underlying.obj M).obj) ∧
            ssf.wPhase X.obj <
                ssf.wPhase
                  (CategoryTheory.Subobject.underlying.obj M).obj ∧
              CategoryTheory.StrictShortExact
                { X₁ := CategoryTheory.Subobject.underlying.obj M,
                  X₂ := X, X₃ := CategoryTheory.Limits.cokernel M.arrow,
                  f := M.arrow,
                  g := CategoryTheory.Limits.cokernel.π M.arrow,
                  zero := ⋯ }
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_first_strictShortExact_of_not_semistable_of_strictArtinian.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  [CategoryTheory.IsStrictArtinianObject
      X]
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F) :
  ∃ M,
    M ≠ ⊥ ∧
      M ≠ ⊤ ∧
        CategoryTheory.IsStrictMono
            M.arrow ∧
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf
              (CategoryTheory.Subobject.underlying.obj
                  M).obj
              (ssf.wPhase
                (CategoryTheory.Subobject.underlying.obj
                    M).obj) ∧
            ssf.wPhase X.obj <
                ssf.wPhase
                  (CategoryTheory.Subobject.underlying.obj
                      M).obj ∧
              CategoryTheory.StrictShortExact
                {
                  X₁ :=
                    CategoryTheory.Subobject.underlying.obj
                      M,
                  X₂ := X,
                  X₃ :=
                    CategoryTheory.Limits.cokernel
                      M.arrow,
                  f := M.arrow,
                  g :=
                    CategoryTheory.Limits.cokernel.π
                      M.arrow,
                  zero := ⋯ }

Something wrong, better idea? Suggest a change

14.6.5. finite_strictSubobjects_of_finite_leftHeartSubobjects🔗

Finiteness of subobjects in the left-heart image of an interval object implies finiteness of the set of nonzero strict subobjects in the thin interval category. This provides the local finite-length input for the first strict short exact sequence.

Proof: The functor to the left heart preserves strict monomorphisms as monomorphisms, so there is an injection from strict subobjects of X in the interval category to subobjects of FL(X) in the left heart. Finiteness of the target implies finiteness of the source.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.finite_strictSubobjects_of_finite_leftHeartSubobjects.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (hX :
    Finite
      (CategoryTheory.Subobject
        ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C
              s a b ⋯).obj
          X))) :
  Finite { B // B ≠ ⊥ ∧ CategoryTheory.IsStrictMono B.arrow }
CategoryTheory.Triangulated.Slicing.IntervalCat.finite_strictSubobjects_of_finite_leftHeartSubobjects.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (hX :
    Finite
      (CategoryTheory.Subobject
        ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
              C s a b ⋯).obj
          X))) :
  Finite
    { B //
      B ≠ ⊥ ∧
        CategoryTheory.IsStrictMono
          B.arrow }

Something wrong, better idea? Suggest a change

14.6.6. exists_first_strictShortExact_of_not_semistable🔗

Bridgeland's first strict short exact sequence in a thin category: if an interval object X is not W-semistable, there is a proper strict subobject M of maximal W-phase with M semistable, \psi(M) > \psi(X), and the inclusion gives a strict SES 0 \to M \to X \to X/M \to 0. The finite-length input is finiteness of the strict-subobject set, not an ambient \operatorname{Finite}(\operatorname{Subobject}(X)) statement.

Proof: Select a maximal-phase maximal strict subobject M from the finite set. Verify M \ne \top (by maxPhase_strictSubobject_ne_top_of_not_semistable), semistability (by semistable_of_maxPhase_strictSubobject), the phase gap (by phase_gt_of_maxPhase_strictSubobject_of_not_semistable), and the strict SES (by interval_strictShortExact_cokernel_of_strictMono).

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_first_strictShortExact_of_not_semistable.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hT_fin : {M | M ≠ ⊥ ∧ CategoryTheory.IsStrictMono M.arrow}.Finite)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) :
  ∃ M,
    M ≠ ⊥ ∧
      M ≠ ⊤ ∧
        CategoryTheory.IsStrictMono M.arrow ∧
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf (CategoryTheory.Subobject.underlying.obj M).obj
              (ssf.wPhase
                (CategoryTheory.Subobject.underlying.obj M).obj) ∧
            ssf.wPhase X.obj <
                ssf.wPhase
                  (CategoryTheory.Subobject.underlying.obj M).obj ∧
              CategoryTheory.StrictShortExact
                { X₁ := CategoryTheory.Subobject.underlying.obj M,
                  X₂ := X, X₃ := CategoryTheory.Limits.cokernel M.arrow,
                  f := M.arrow,
                  g := CategoryTheory.Limits.cokernel.π M.arrow,
                  zero := ⋯ }
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_first_strictShortExact_of_not_semistable.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hT_fin :
    {M |
        M ≠ ⊥ ∧
          CategoryTheory.IsStrictMono
            M.arrow}.Finite)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj))
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F) :
  ∃ M,
    M ≠ ⊥ ∧
      M ≠ ⊤ ∧
        CategoryTheory.IsStrictMono
            M.arrow ∧
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf
              (CategoryTheory.Subobject.underlying.obj
                  M).obj
              (ssf.wPhase
                (CategoryTheory.Subobject.underlying.obj
                    M).obj) ∧
            ssf.wPhase X.obj <
                ssf.wPhase
                  (CategoryTheory.Subobject.underlying.obj
                      M).obj ∧
              CategoryTheory.StrictShortExact
                {
                  X₁ :=
                    CategoryTheory.Subobject.underlying.obj
                      M,
                  X₂ := X,
                  X₃ :=
                    CategoryTheory.Limits.cokernel
                      M.arrow,
                  f := M.arrow,
                  g :=
                    CategoryTheory.Limits.cokernel.π
                      M.arrow,
                  zero := ⋯ }

Something wrong, better idea? Suggest a change