Bridgeland Stability Conditions

14.22. Deformation: StrictShortExactSequence🔗

14.22.1. exists_first_strictShortExact_of_not_semistable_of_finite_leftHeartSubobjects🔗

If an interval object X is not W-semistable at its own W-phase and has finite subobject lattice in the left heart, then X admits Bridgeland's first strict short exact sequence: a proper strict subobject M with \operatorname{wPhaseOf}(W(M)) > \operatorname{wPhaseOf}(W(X)) that is itself W-semistable.

Proof: Finiteness of the left-heart subobject lattice implies finiteness of the strict subobject set. Apply exists_first_strictShortExact_of_not_semistable with this finite witness.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_first_strictShortExact_of_not_semistable_of_finite_leftHeartSubobjects.{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)
  (hX_left :
    Finite
      (CategoryTheory.Subobject
        ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart C
              σ.slicing a b ⋯).obj
          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_finite_leftHeartSubobjects.{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)
  (hX_left :
    Finite
      (CategoryTheory.Subobject
        ((CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart
              C σ.slicing a b ⋯).obj
          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.22.2. interval_pullback_cokernel_bot_eq🔗

The pullback of \bot along the cokernel projection \operatorname{coker}(M) \twoheadrightarrow \cdot recovers M itself.

Proof: The pullback of \bot is the kernel of the cokernel projection, which equals M by the universal property of strict monos.

🔗theorem
CategoryTheory.Triangulated.interval_pullback_cokernel_bot_eq.{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}
  (M : CategoryTheory.Subobject X)
  (hM : CategoryTheory.IsStrictMono M.arrow) :
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M.arrow)).obj
      ⊥ =
    M
CategoryTheory.Triangulated.interval_pullback_cokernel_bot_eq.{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}
  (M : CategoryTheory.Subobject X)
  (hM :
    CategoryTheory.IsStrictMono M.arrow) :
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M.arrow)).obj
      ⊥ =
    M

Something wrong, better idea? Suggest a change

14.22.3. interval_cokernel_nonzero_of_ne_top🔗

If M is a strict subobject of X in the thin interval category with M \ne \top (i.e., M is a proper strict subobject), then \mathrm{coker}(M \hookrightarrow X) is nonzero. Contrapositively, if the cokernel vanishes then the inclusion is an epimorphism, hence an isomorphism (since it is also a strict monomorphism), so M = \top.

Proof: If \mathrm{coker}(M) \cong 0, then M.\mathrm{arrow} is both a strict mono and (by Preadditive.epi_of_isZero_cokernel) an epi, so it is an isomorphism. Then Subobject.eq_top_of_isIso_arrow gives M = \top, contradicting M \ne \top.

🔗theorem
CategoryTheory.Triangulated.interval_cokernel_nonzero_of_ne_top.{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}
  {M : CategoryTheory.Subobject X} (hM : M ≠ ⊤)
  (hM_strict : CategoryTheory.IsStrictMono M.arrow) :
  ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel M.arrow)
CategoryTheory.Triangulated.interval_cokernel_nonzero_of_ne_top.{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}
  {M : CategoryTheory.Subobject X}
  (hM : M ≠ ⊤)
  (hM_strict :
    CategoryTheory.IsStrictMono M.arrow) :
  ¬CategoryTheory.Limits.IsZero
      (CategoryTheory.Limits.cokernel
        M.arrow)

Something wrong, better idea? Suggest a change

14.22.4. interval_pullback_ofLE_comm🔗

For subobjects A' \le B' of \mathrm{coker}(M), the pullbacks satisfy the naturality square: the canonical map \pi^*A' \to \pi^*B' followed by the pullback projection \pi^*B' \to B' equals the pullback projection \pi^*A' \to A' followed by the inclusion A' \le B'. In short, the pullback functor \pi^*(-) commutes with the ofLE inclusion morphisms.

Proof: The proof cancels the monomorphism B'.\mathrm{arrow} and then traces the square through the pullback equations and Subobject.ofLE_arrow, using the two pullback square commutativity identities (\pi^*B').\mathrm{arrow} \circ q = (\pi^*\pi_B) \circ B'.\mathrm{arrow} and analogously for A'.

🔗theorem
CategoryTheory.Triangulated.interval_pullback_ofLE_comm.{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}
  {M : CategoryTheory.Subobject X}
  {A' B' :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)}
  (h : A' ≤ B') :
  have q := CategoryTheory.Limits.cokernel.π M.arrow;
  let pbA := (CategoryTheory.Subobject.pullback q).obj A';
  let pbB := (CategoryTheory.Subobject.pullback q).obj B';
  have hpb := ⋯;
  CategoryTheory.CategoryStruct.comp (pbA.ofLE pbB hpb)
      (CategoryTheory.Subobject.pullbackπ q B') =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Subobject.pullbackπ q A') (A'.ofLE B' h)
CategoryTheory.Triangulated.interval_pullback_ofLE_comm.{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}
  {M : CategoryTheory.Subobject X}
  {A' B' :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)}
  (h : A' ≤ B') :
  have q :=
    CategoryTheory.Limits.cokernel.π
      M.arrow;
  let pbA :=
    (CategoryTheory.Subobject.pullback
          q).obj
      A';
  let pbB :=
    (CategoryTheory.Subobject.pullback
          q).obj
      B';
  have hpb := ⋯;
  CategoryTheory.CategoryStruct.comp
      (pbA.ofLE pbB hpb)
      (CategoryTheory.Subobject.pullbackπ
        q B') =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Subobject.pullbackπ
        q A')
      (A'.ofLE B' h)

Something wrong, better idea? Suggest a change

14.22.5. Wobj_pullback_eq_add🔗

For a strict monomorphism M \hookrightarrow X and a subobject B of \mathrm{coker}(M), the deformed charge of the pullback-cokernel subobject satisfies W([\pi^*B]) = W([M]) + W([B]). This is the W-additivity for the strict short exact sequence 0 \to M \to \pi^*B \to B \to 0 in the thin interval category.

Proof: The pair (M \le \pi^*B,\ \pi^*B \to B) from interval_le_pullback_cokernel and interval_ofLE_pullbackπ_eq_zero assembles into a strict short exact sequence via interval_strictShortExact_ofLE_pullbackπ_cokernel. Then W-additivity on strict short exact sequences (ssf.strict_additive) gives the formula.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.Wobj_pullback_eq_add.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  (hM : CategoryTheory.IsStrictMono M.arrow)
  (B :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)) :
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Subobject.underlying.obj
            ((CategoryTheory.Subobject.pullback
                  (CategoryTheory.Limits.cokernel.π M.arrow)).obj
              B)).obj) =
    ssf.W
        (CategoryTheory.Triangulated.cl C v
          (CategoryTheory.Subobject.underlying.obj M).obj) +
      ssf.W
        (CategoryTheory.Triangulated.cl C v
          (CategoryTheory.Subobject.underlying.obj B).obj)
CategoryTheory.Triangulated.SkewedStabilityFunction.Wobj_pullback_eq_add.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  (hM :
    CategoryTheory.IsStrictMono M.arrow)
  (B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)) :
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Subobject.underlying.obj
            ((CategoryTheory.Subobject.pullback
                  (CategoryTheory.Limits.cokernel.π
                    M.arrow)).obj
              B)).obj) =
    ssf.W
        (CategoryTheory.Triangulated.cl C
          v
          (CategoryTheory.Subobject.underlying.obj
              M).obj) +
      ssf.W
        (CategoryTheory.Triangulated.cl C
          v
          (CategoryTheory.Subobject.underlying.obj
              B).obj)

Something wrong, better idea? Suggest a change

14.22.6. interval_lt_pullback_cokernel_of_ne_bot🔗

If B \ne \bot is a nonzero subobject of \mathrm{coker}(M), then the pullback \pi^*B is strictly larger than M in the subobject lattice of X: M < \pi^*B. This is a strict version of interval_le_pullback_cokernel exploiting that a non-bottom subobject of the cokernel pulls back strictly above M.

Proof: Equality M = \pi^*B would force the pullback projection \pi^* B \to B to be zero (via interval_ofLE_pullbackπ_eq_zero and the iso-arrow), but the pullback projection is a strict epi (by interval_pullbackπ_strictEpi_of_strictEpi), hence an epi, and a zero epi forces B \cong 0, i.e., B = \bot, contradicting B \ne \bot.

🔗theorem
CategoryTheory.Triangulated.interval_lt_pullback_cokernel_of_ne_bot.{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}
  {M : CategoryTheory.Subobject X}
  {B :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)}
  (hB : B ≠ ⊥) :
  M <
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M.arrow)).obj
      B
CategoryTheory.Triangulated.interval_lt_pullback_cokernel_of_ne_bot.{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}
  {M : CategoryTheory.Subobject X}
  {B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)}
  (hB : B ≠ ⊥) :
  M <
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M.arrow)).obj
      B

Something wrong, better idea? Suggest a change

14.22.7. interval_pullback_cokernel_ne_top_of_ne_top🔗

If B is a proper strict subobject of \mathrm{coker}(M) (i.e., B \ne \top), then the pullback \pi^*B is a proper subobject of X: \pi^*B \ne \top. This is a contrapositive: if \pi^*B = \top, we can invert its arrow and factor the cokernel projection through B, forcing B.\mathrm{arrow} to be epi, hence (being a strict mono) an iso, giving B = \top.

Proof: If \pi^*B = \top, then \pi^*B.\mathrm{arrow} is an isomorphism. The retraction r = (\pi^*B.\mathrm{arrow})^{-1} \circ (\pi^*\pi)\colon X \to B satisfies r \circ B.\mathrm{arrow} = q (the cokernel projection), which forces B.\mathrm{arrow} to be epi. Since B.\mathrm{arrow} is also a strict mono, it is an isomorphism, so Subobject.eq_top_of_isIso_arrow gives B = \top.

🔗theorem
CategoryTheory.Triangulated.interval_pullback_cokernel_ne_top_of_ne_top.{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}
  {M : CategoryTheory.Subobject X}
  {B :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)}
  (hB : B ≠ ⊤) (hB_strict : CategoryTheory.IsStrictMono B.arrow) :
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M.arrow)).obj
      B ≠
    ⊤
CategoryTheory.Triangulated.interval_pullback_cokernel_ne_top_of_ne_top.{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}
  {M : CategoryTheory.Subobject X}
  {B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)}
  (hB : B ≠ ⊤)
  (hB_strict :
    CategoryTheory.IsStrictMono B.arrow) :
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M.arrow)).obj
      B ≠
    ⊤

Something wrong, better idea? Suggest a change

14.22.8. Wobj_cokernel_pullback_eq🔗

For a strict monomorphism M \hookrightarrow X and a strict monomorphism B \hookrightarrow \mathrm{coker}(M), the deformed charge of the cokernel of the pullback-cokernel subobject \pi^*B \hookrightarrow X equals the deformed charge of the cokernel of B: W([\mathrm{coker}(\pi^*B)]) = W([\mathrm{coker}(B)]). This reflects a K_0 cancellation in the diamond of subobjects.

Proof: Three instances of the strict short exact sequence K_0 identity interval_K0_of_strictMono give: W(X) = W(M) + W(\mathrm{coker}(M)), W(X) = W(\pi^*B) + W(\mathrm{coker}(\pi^*B)), and W(\mathrm{coker}(M)) = W(B) + W(\mathrm{coker}(B)). Combined with Wobj_pullback_eq_add giving W(\pi^*B) = W(M) + W(B), the four equations yield W(\mathrm{coker}(\pi^*B)) = W(\mathrm{coker}(B)) by cancellation.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.Wobj_cokernel_pullback_eq.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  (hM : CategoryTheory.IsStrictMono M.arrow)
  {B :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)}
  (hB : CategoryTheory.IsStrictMono B.arrow) :
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel
            ((CategoryTheory.Subobject.pullback
                    (CategoryTheory.Limits.cokernel.π M.arrow)).obj
                B).arrow).obj) =
    ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel B.arrow).obj)
CategoryTheory.Triangulated.SkewedStabilityFunction.Wobj_cokernel_pullback_eq.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  (hM :
    CategoryTheory.IsStrictMono M.arrow)
  {B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)}
  (hB :
    CategoryTheory.IsStrictMono B.arrow) :
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel
            ((CategoryTheory.Subobject.pullback
                    (CategoryTheory.Limits.cokernel.π
                      M.arrow)).obj
                B).arrow).obj) =
    ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel
            B.arrow).obj)

Something wrong, better idea? Suggest a change

14.22.9. Wobj_liftSub_cokernel_eq_add🔗

For strict monomorphisms A \hookrightarrow M \hookrightarrow X in the thin interval category, the deformed charge of the cokernel of the composed inclusion A \hookrightarrow X (the liftSub subobject) satisfies W([\mathrm{coker}(A \hookrightarrow X)]) = W([\mathrm{coker}(A \hookrightarrow M)]) + W([\mathrm{coker}(M \hookrightarrow X)]). This is the W-additivity for a three-term filtration step.

Proof: Three K_0 additivity identities from interval_K0_of_strictMono give W(X) = W(M) + W(\mathrm{coker}(M)), W(M) = W(A) + W(\mathrm{coker}(A \hookrightarrow M)), and W(X) = W(\mathrm{liftA}) + W(\mathrm{coker}(\mathrm{liftA})). Since \mathrm{liftA} is isomorphic to A (the underlying object is the same), we have W(\mathrm{liftA}) = W(A), and cancelling W(A) from both expansions of W(X) yields the result.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.Wobj_liftSub_cokernel_eq_add.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  (hM : CategoryTheory.IsStrictMono M.arrow)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)}
  (hA : CategoryTheory.IsStrictMono A.arrow) :
  have liftA := CategoryTheory.Triangulated.intervalLiftSub C M A;
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel liftA.arrow).obj) =
    ssf.W
        (CategoryTheory.Triangulated.cl C v
          (CategoryTheory.Limits.cokernel A.arrow).obj) +
      ssf.W
        (CategoryTheory.Triangulated.cl C v
          (CategoryTheory.Limits.cokernel M.arrow).obj)
CategoryTheory.Triangulated.SkewedStabilityFunction.Wobj_liftSub_cokernel_eq_add.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  (hM :
    CategoryTheory.IsStrictMono M.arrow)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)}
  (hA :
    CategoryTheory.IsStrictMono A.arrow) :
  have liftA :=
    CategoryTheory.Triangulated.intervalLiftSub
      C M A;
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel
            liftA.arrow).obj) =
    ssf.W
        (CategoryTheory.Triangulated.cl C
          v
          (CategoryTheory.Limits.cokernel
              A.arrow).obj) +
      ssf.W
        (CategoryTheory.Triangulated.cl C
          v
          (CategoryTheory.Limits.cokernel
              M.arrow).obj)

Something wrong, better idea? Suggest a change

14.22.10. semistable_cokernel_of_minPhase_strictKernel🔗

If M is a strict subobject of a W-semistable object X with \operatorname{wPhaseOf}(W(M)) > \psi, then the strict cokernel is W-semistable at phase \operatorname{wPhaseOf}(W(\operatorname{coker})).

Proof: The strict short exact sequence M \hookrightarrow X \twoheadrightarrow Q gives W(X) = W(M) + W(Q). The phase see-saw forces \operatorname{wPhaseOf}(W(Q)) < \psi. For any further subobject of Q, iterate the K_0 argument.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_cokernel_of_minPhase_strictKernel.{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}
  (hFinSub :
    ∀
      (Y :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a
          b),
      Finite (CategoryTheory.Subobject Y))
  (hM_ne_top : M ≠ ⊤) (hM_strict : CategoryTheory.IsStrictMono M.arrow)
  (hM_lt :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊤ →
        CategoryTheory.IsStrictMono B.arrow →
          M < B →
            ssf.wPhase (CategoryTheory.Limits.cokernel M.arrow).obj <
              ssf.wPhase (CategoryTheory.Limits.cokernel B.arrow).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
    (CategoryTheory.Limits.cokernel M.arrow).obj
    (ssf.wPhase (CategoryTheory.Limits.cokernel M.arrow).obj)
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_cokernel_of_minPhase_strictKernel.{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}
  (hFinSub :
    ∀
      (Y :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b),
      Finite (CategoryTheory.Subobject Y))
  (hM_ne_top : M ≠ ⊤)
  (hM_strict :
    CategoryTheory.IsStrictMono M.arrow)
  (hM_lt :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊤ →
        CategoryTheory.IsStrictMono
            B.arrow →
          M < B →
            ssf.wPhase
                (CategoryTheory.Limits.cokernel
                    M.arrow).obj <
              ssf.wPhase
                (CategoryTheory.Limits.cokernel
                    B.arrow).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C ssf
    (CategoryTheory.Limits.cokernel
        M.arrow).obj
    (ssf.wPhase
      (CategoryTheory.Limits.cokernel
          M.arrow).obj)

Something wrong, better idea? Suggest a change

14.22.11. semistable_of_lower_inclusion🔗

W-semistability is preserved under inclusion into a wider interval \mathcal{P}((a', b')) with a' \le a and b' \ge b, provided the wider interval still satisfies the thinness constraint.

Proof: The W-semistability data (interval membership, phase equality, and the subobject phase inequality) all transfer to the wider interval since distinguished triangles with vertices in the narrower interval remain in the wider one.

🔗theorem
CategoryTheory.Triangulated.semistable_of_lower_inclusion.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C] {a₁ a₂ b ψ ε₀ : ℝ} (ha₁ : a₁ < b)
  (ha₂ : a₂ < b) (ha : a₂ ≤ a₁) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW ha₁)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a₁ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀) (hthin₂ : b - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW ha₂)
    E ψ
CategoryTheory.Triangulated.semistable_of_lower_inclusion.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C]
  {a₁ a₂ b ψ ε₀ : ℝ} (ha₁ : a₁ < b)
  (ha₂ : a₂ < b) (ha : a₂ ≤ a₁) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW ha₁)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a₁ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀)
  (hthin₂ : b - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW ha₂)
    E ψ

Something wrong, better idea? Suggest a change

14.22.12. semistable_of_interval_inclusion🔗

W-semistability transfers across an arbitrary interval inclusion \mathcal{P}((a_1, b_1)) \hookrightarrow \mathcal{P}((a_2, b_2)) satisfying the thinness and enveloping constraints.

Proof: Compose semistable_of_lower_inclusion with interval monotonicity.

🔗theorem
CategoryTheory.Triangulated.semistable_of_interval_inclusion.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C] {a₁ a₂ b₁ b₂ ψ ε₀ : ℝ}
  (hab₁ : a₁ < b₁) (hab₂ : a₂ < b₂) (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂)
  {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₁)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a₁ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b₁ - ε₀) (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab₂)
    E ψ
CategoryTheory.Triangulated.semistable_of_interval_inclusion.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C]
  {a₁ a₂ b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a₁ < b₁)
  (hab₂ : a₂ < b₂) (ha : a₂ ≤ a₁)
  (hb : b₁ ≤ b₂) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₁)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a₁ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b₁ - ε₀)
  (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab₂)
    E ψ

Something wrong, better idea? Suggest a change

14.22.13. semistable_of_target_subinterval🔗

W-semistability transfers to a target subinterval: if E is W-semistable in \mathcal{P}((a, b)) and E \in \mathcal{P}((a', b')) with a \le a' and b' \le b, then E is W-semistable in \mathcal{P}((a', b')).

Proof: Subobject triangles with vertices in the narrower interval remain in the wider one, so the W-semistability condition is preserved.

🔗theorem
CategoryTheory.Triangulated.semistable_of_target_subinterval.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a₁ a₂ b₂ b₁ ψ ε₀ : ℝ} (hab₁ : a₁ < b₁) (hab₂ : a₂ < b₂)
  (ha : a₁ ≤ a₂) (hb : b₂ ≤ b₁) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₁)
      E ψ)
  (hI₂ :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂
      E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv₂_lo : a₂ + ε₀ ≤ ψ)
  (henv₂_hi : ψ ≤ b₂ - ε₀) (hthin₁ : b₁ - a₁ + 2 * ε₀ < 1)
  (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab₂)
    E ψ
CategoryTheory.Triangulated.semistable_of_target_subinterval.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a₁ a₂ b₂ b₁ ψ ε₀ : ℝ} (hab₁ : a₁ < b₁)
  (hab₂ : a₂ < b₂) (ha : a₁ ≤ a₂)
  (hb : b₂ ≤ b₁) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₁)
      E ψ)
  (hI₂ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a₂ b₂ E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv₂_lo : a₂ + ε₀ ≤ ψ)
  (henv₂_hi : ψ ≤ b₂ - ε₀)
  (hthin₁ : b₁ - a₁ + 2 * ε₀ < 1)
  (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab₂)
    E ψ

Something wrong, better idea? Suggest a change

14.22.14. semistable_of_target_envelope🔗

W-semistability transfers under the enveloping condition: if the W-phase \psi satisfies a' + \varepsilon_0 \le \psi \le b' - \varepsilon_0 for a new interval (a', b').

Proof: Combine the interval transfer lemmas with verification of the enveloping constraints.

🔗theorem
CategoryTheory.Triangulated.semistable_of_target_envelope.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C] {a₁ a₂ b₁ b₂ ψ ε₀ : ℝ}
  (hab₁ : a₁ < b₁) (hab₂ : a₂ < b₂) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₁)
      E ψ)
  (hI₂ :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b₂
      E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv₁_lo : a₁ + ε₀ ≤ ψ)
  (henv₁_hi : ψ ≤ b₁ - ε₀) (henv₂_lo : a₂ + ε₀ ≤ ψ)
  (henv₂_hi : ψ ≤ b₂ - ε₀) (hthin₁ : b₁ - a₁ + 2 * ε₀ < 1)
  (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab₂)
    E ψ
CategoryTheory.Triangulated.semistable_of_target_envelope.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C]
  {a₁ a₂ b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a₁ < b₁)
  (hab₂ : a₂ < b₂) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₁)
      E ψ)
  (hI₂ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a₂ b₂ E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv₁_lo : a₁ + ε₀ ≤ ψ)
  (henv₁_hi : ψ ≤ b₁ - ε₀)
  (henv₂_lo : a₂ + ε₀ ≤ ψ)
  (henv₂_hi : ψ ≤ b₂ - ε₀)
  (hthin₁ : b₁ - a₁ + 2 * ε₀ < 1)
  (hthin₂ : b₂ - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab₂)
    E ψ

Something wrong, better idea? Suggest a change

14.22.15. phase_le_of_strictQuotient_of_window🔗

A strict quotient of a W-semistable object in a windowed interval has W-phase at least \psi, with the stronger hypothesis that the window satisfies the enveloping condition.

Proof: Extract the distinguished triangle from the strict short exact sequence and apply phase_le_of_triangle_quotient.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_le_of_strictQuotient_of_window.{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 Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {ψ : ℝ}
  (hX :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      X.obj ψ)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) (p : X ⟶ Y) (hp : CategoryTheory.IsStrictEpi p)
  (hY : ¬CategoryTheory.Limits.IsZero Y.obj) : ψ ≤ ssf.wPhase Y.obj
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_le_of_strictQuotient_of_window.{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 Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {ψ : ℝ}
  (hX :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf X.obj ψ)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) (p : X ⟶ Y)
  (hp : CategoryTheory.IsStrictEpi p)
  (hY :
    ¬CategoryTheory.Limits.IsZero Y.obj) :
  ψ ≤ ssf.wPhase Y.obj

Something wrong, better idea? Suggest a change

14.22.16. phase_cokernel_lt_of_phase_gt_strictSubobject🔗

If M is a strict subobject of W-semistable X with \operatorname{wPhaseOf}(W(M)) > \psi, then the cokernel has \operatorname{wPhaseOf}(W(\operatorname{coker})) < \psi.

Proof: From W(X) = W(M) + W(\operatorname{coker}) and \operatorname{wPhaseOf}(W(X)) = \psi < \operatorname{wPhaseOf}(W(M)), the dual see-saw gives \operatorname{wPhaseOf}(W(\operatorname{coker})) < \psi.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_cokernel_lt_of_phase_gt_strictSubobject.{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)]
  {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {A : CategoryTheory.Subobject Y} (hA_ne_bot : A ≠ ⊥)
  (hA_ne_top : A ≠ ⊤) (hA_strict : CategoryTheory.IsStrictMono A.arrow)
  (hA_phase_gt :
    ssf.wPhase Y.obj <
      ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) :
  ssf.wPhase (CategoryTheory.Limits.cokernel A.arrow).obj <
    ssf.wPhase Y.obj
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_cokernel_lt_of_phase_gt_strictSubobject.{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)]
  {Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {A : CategoryTheory.Subobject Y}
  (hA_ne_bot : A ≠ ⊥) (hA_ne_top : A ≠ ⊤)
  (hA_strict :
    CategoryTheory.IsStrictMono A.arrow)
  (hA_phase_gt :
    ssf.wPhase Y.obj <
      ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) :
  ssf.wPhase
      (CategoryTheory.Limits.cokernel
          A.arrow).obj <
    ssf.wPhase Y.obj

Something wrong, better idea? Suggest a change