Bridgeland Stability Conditions

14.20. Deformation: Pullback🔗

14.20.1. interval_pullbackπ_strictEpi_of_strictEpi🔗

Pullback of a strict epimorphism in a thin interval category is a strict epimorphism: if f : A \twoheadrightarrow B is strict epi and g : C \to B is any morphism, then \pi_1 : A \times_B C \to C is strict epi.

Proof: Strict epimorphisms in the thin interval category are detected by the left-heart functor. Pullbacks in the interval category map to pullbacks in the left heart (abelian), where the pullback of an epimorphism is epi. Transport back.

🔗theorem
CategoryTheory.Triangulated.interval_pullbackπ_strictEpi_of_strictEpi.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (p : X ⟶ Y) (hp : CategoryTheory.IsStrictEpi p)
  (B : CategoryTheory.Subobject Y) :
  CategoryTheory.IsStrictEpi (CategoryTheory.Subobject.pullbackπ p B)
CategoryTheory.Triangulated.interval_pullbackπ_strictEpi_of_strictEpi.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (p : X ⟶ Y)
  (hp : CategoryTheory.IsStrictEpi p)
  (B : CategoryTheory.Subobject Y) :
  CategoryTheory.IsStrictEpi
    (CategoryTheory.Subobject.pullbackπ p
      B)

Something wrong, better idea? Suggest a change

14.20.2. interval_pullback_arrow_strictMono_of_strictMono🔗

Pullback of a strict monomorphism along a morphism in a thin interval category preserves strict monicity: if B \hookrightarrow X is strict mono and f : Y \to X is any morphism, the pullback arrow is strict mono.

Proof: The pullback square in the interval category maps to a pullback square in the left heart (exact functor). Monomorphisms pull back in abelian categories. Transport the mono back to strict mono in the interval category.

🔗theorem
CategoryTheory.Triangulated.interval_pullback_arrow_strictMono_of_strictMono.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (p : X ⟶ Y) (B : CategoryTheory.Subobject Y)
  (hB : CategoryTheory.IsStrictMono B.arrow) :
  CategoryTheory.IsStrictMono
    ((CategoryTheory.Subobject.pullback p).obj B).arrow
CategoryTheory.Triangulated.interval_pullback_arrow_strictMono_of_strictMono.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (p : X ⟶ Y)
  (B : CategoryTheory.Subobject Y)
  (hB :
    CategoryTheory.IsStrictMono B.arrow) :
  CategoryTheory.IsStrictMono
    ((CategoryTheory.Subobject.pullback
            p).obj
        B).arrow

Something wrong, better idea? Suggest a change

14.20.3. interval_le_pullback_cokernel🔗

For any subobject M \hookrightarrow X in the thin interval category and any subobject B of \mathrm{coker}(M \hookrightarrow X), we have M \le (\pi^* B) in the subobject lattice of X, where \pi^* B denotes the pullback of B along the cokernel projection \pi\colon X \to \mathrm{coker}(M). This is the key inclusion placing M below the pullback-cokernel subobject.

Proof: The proof uses the universal property of the pullback: the map M \to \pi^*B is constructed by lifting (0, M.\mathrm{arrow}) through the pullback square. Concretely, Subobject.isPullback provides the lift, using the fact that M.\mathrm{arrow} \circ \pi = 0 (the cokernel condition).

🔗theorem
CategoryTheory.Triangulated.interval_le_pullback_cokernel.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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)) :
  M ≤
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M.arrow)).obj
      B
CategoryTheory.Triangulated.interval_le_pullback_cokernel.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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)) :
  M ≤
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M.arrow)).obj
      B

Something wrong, better idea? Suggest a change

14.20.4. interval_ofLE_pullbackπ_eq_zero🔗

The composite M \xrightarrow{\mathrm{ofLE}} \pi^*B \xrightarrow{\pi^*\pi} B is zero, where \pi^*\pi is the pullback projection from \pi^*B to B. This says the map M \to B induced by the inclusion M \le \pi^*B factors through zero — geometrically, M maps to zero in B because M.\mathrm{arrow} \circ \pi = 0.

Proof: The proof cancels the monomorphism B.\mathrm{arrow} and traces the chain of equalities through the pullback square: the composite M \to \pi^*B \to B equals M \to \pi^*B \to X \to \mathrm{coker}(M) = 0 \to B, using Subobject.ofLE_arrow and the cokernel condition.

🔗theorem
CategoryTheory.Triangulated.interval_ofLE_pullbackπ_eq_zero.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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)) :
  CategoryTheory.CategoryStruct.comp
      (M.ofLE
        ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π M.arrow)).obj
          B)
        ⋯)
      (CategoryTheory.Subobject.pullbackπ
        (CategoryTheory.Limits.cokernel.π M.arrow) B) =
    0
CategoryTheory.Triangulated.interval_ofLE_pullbackπ_eq_zero.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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)) :
  CategoryTheory.CategoryStruct.comp
      (M.ofLE
        ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π
                M.arrow)).obj
          B)
        ⋯)
      (CategoryTheory.Subobject.pullbackπ
        (CategoryTheory.Limits.cokernel.π
          M.arrow)
        B) =
    0

Something wrong, better idea? Suggest a change

14.20.5. interval_strictShortExact_of_kernel_strictEpi🔗

A short complex K \hookrightarrow X \twoheadrightarrow Q in a thin interval category is a strict short exact sequence when K = \ker(q) and q is strict epi.

Proof: The complex maps to a short exact sequence in the left heart: K maps to the kernel, q maps to an epimorphism. The left-heart short exact sequence gives the strict short exact sequence in the interval category.

🔗theorem
CategoryTheory.Triangulated.interval_strictShortExact_of_kernel_strictEpi.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b))
  (hKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
  (hg : CategoryTheory.IsStrictEpi S.g) :
  CategoryTheory.StrictShortExact S
CategoryTheory.Triangulated.interval_strictShortExact_of_kernel_strictEpi.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  (S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b))
  (hKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι
        S.f ⋯))
  (hg : CategoryTheory.IsStrictEpi S.g) :
  CategoryTheory.StrictShortExact S

Something wrong, better idea? Suggest a change

14.20.6. interval_strictShortExact_pullback_left🔗

Pullback of a strict short exact sequence along a morphism yields a strict short exact sequence on the left: given 0 \to A \to B \to C \to 0 and f : D \to B, the pullback gives 0 \to A \to D \times_B B \to D \times_B C \to 0.

Proof: Map to the left heart, apply the abelian pullback lemma, transport back.

🔗theorem
CategoryTheory.Triangulated.interval_strictShortExact_pullback_left.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {K E Q : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  {i : K ⟶ E} {q : E ⟶ Q}
  (hiq : CategoryTheory.CategoryStruct.comp i q = 0)
  (hKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι i hiq))
  (hq : CategoryTheory.IsStrictEpi q) (B : CategoryTheory.Subobject Q) :
  let pb := (CategoryTheory.Subobject.pullback q).obj B;
  let m :=
    have hiB := ⋯;
    pb.factorThru i ⋯;
  CategoryTheory.StrictShortExact
    { X₁ := K, X₂ := CategoryTheory.Subobject.underlying.obj pb,
      X₃ := CategoryTheory.Subobject.underlying.obj B, f := m,
      g := CategoryTheory.Subobject.pullbackπ q B, zero := ⋯ }
CategoryTheory.Triangulated.interval_strictShortExact_pullback_left.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {K E Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  {i : K ⟶ E} {q : E ⟶ Q}
  (hiq :
    CategoryTheory.CategoryStruct.comp i
        q =
      0)
  (hKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι
        i hiq))
  (hq : CategoryTheory.IsStrictEpi q)
  (B : CategoryTheory.Subobject Q) :
  let pb :=
    (CategoryTheory.Subobject.pullback
          q).obj
      B;
  let m :=
    have hiB := ⋯;
    pb.factorThru i ⋯;
  CategoryTheory.StrictShortExact
    { X₁ := K,
      X₂ :=
        CategoryTheory.Subobject.underlying.obj
          pb,
      X₃ :=
        CategoryTheory.Subobject.underlying.obj
          B,
      f := m,
      g :=
        CategoryTheory.Subobject.pullbackπ
          q B,
      zero := ⋯ }

Something wrong, better idea? Suggest a change

14.20.7. interval_strictShortExact_pullback_right🔗

Pullback of a strict short exact sequence along a morphism on the right: given 0 \to A \to B \to C \to 0 and g : D \to C, the pullback gives 0 \to A \to B \times_C D \to D \to 0.

Proof: Map to the left heart, apply the standard abelian pullback-along-epi lemma, transport back.

🔗theorem
CategoryTheory.Triangulated.interval_strictShortExact_pullback_right.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {E Q Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (q : E ⟶ Q) (hq : CategoryTheory.IsStrictEpi q)
  (B : CategoryTheory.Subobject Q) (g : Q ⟶ Y)
  (hBg : CategoryTheory.CategoryStruct.comp B.arrow g = 0)
  (hBKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι B.arrow hBg))
  (hg : CategoryTheory.IsStrictEpi g) :
  let pb := (CategoryTheory.Subobject.pullback q).obj B;
  let p := CategoryTheory.CategoryStruct.comp q g;
  CategoryTheory.StrictShortExact
    { X₁ := CategoryTheory.Subobject.underlying.obj pb, X₂ := E,
      X₃ := Y, f := pb.arrow, g := p, zero := ⋯ }
CategoryTheory.Triangulated.interval_strictShortExact_pullback_right.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {E Q Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (q : E ⟶ Q)
  (hq : CategoryTheory.IsStrictEpi q)
  (B : CategoryTheory.Subobject Q)
  (g : Q ⟶ Y)
  (hBg :
    CategoryTheory.CategoryStruct.comp
        B.arrow g =
      0)
  (hBKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι
        B.arrow hBg))
  (hg : CategoryTheory.IsStrictEpi g) :
  let pb :=
    (CategoryTheory.Subobject.pullback
          q).obj
      B;
  let p :=
    CategoryTheory.CategoryStruct.comp q
      g;
  CategoryTheory.StrictShortExact
    {
      X₁ :=
        CategoryTheory.Subobject.underlying.obj
          pb,
      X₂ := E, X₃ := Y, f := pb.arrow,
      g := p, zero := ⋯ }

Something wrong, better idea? Suggest a change

14.20.8. interval_strictShortExact_ofLE_pullbackπ_cokernel🔗

The pullback of a cokernel projection along a subobject inclusion gives a strict short exact sequence relating the subobject, its pullback, and the cokernel.

Proof: Combine interval_strictShortExact_pullback_right with the strict SES 0 \to M \to X \to \operatorname{coker}(M) \to 0.

🔗theorem
CategoryTheory.Triangulated.interval_strictShortExact_ofLE_pullbackπ_cokernel.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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)
  (B :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)) :
  let pbB :=
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M.arrow)).obj
      B;
  have hle := ⋯;
  CategoryTheory.StrictShortExact
    { X₁ := CategoryTheory.Subobject.underlying.obj M,
      X₂ := CategoryTheory.Subobject.underlying.obj pbB,
      X₃ := CategoryTheory.Subobject.underlying.obj B,
      f := M.ofLE pbB hle,
      g :=
        CategoryTheory.Subobject.pullbackπ
          (CategoryTheory.Limits.cokernel.π M.arrow) B,
      zero := ⋯ }
CategoryTheory.Triangulated.interval_strictShortExact_ofLE_pullbackπ_cokernel.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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)
  (B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)) :
  let pbB :=
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M.arrow)).obj
      B;
  have hle := ⋯;
  CategoryTheory.StrictShortExact
    {
      X₁ :=
        CategoryTheory.Subobject.underlying.obj
          M,
      X₂ :=
        CategoryTheory.Subobject.underlying.obj
          pbB,
      X₃ :=
        CategoryTheory.Subobject.underlying.obj
          B,
      f := M.ofLE pbB hle,
      g :=
        CategoryTheory.Subobject.pullbackπ
          (CategoryTheory.Limits.cokernel.π
            M.arrow)
          B,
      zero := ⋯ }

Something wrong, better idea? Suggest a change

14.20.9. interval_fIsKernel_of_strictShortExact🔗

In a strict short exact sequence 0 \to A \xrightarrow{f} B \xrightarrow{g} C \to 0 in a thin interval category, f is a kernel of g.

Construction: Constructs an IsLimit cone for the kernel fork of g at f, using the strict short exact sequence data. The lift is obtained from the left-heart factorization.

🔗def
CategoryTheory.Triangulated.interval_fIsKernel_of_strictShortExact.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C] {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)}
  (hS : CategoryTheory.StrictShortExact S) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)
CategoryTheory.Triangulated.interval_fIsKernel_of_strictShortExact.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated C]
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Triangulated.Slicing.IntervalCat
        C s a b)}
  (hS :
    CategoryTheory.StrictShortExact S) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.KernelFork.ofι
      S.f ⋯)

Something wrong, better idea? Suggest a change

14.20.10. interval_cokernel_pullbackTopIso🔗

The cokernel of the pullback of a subobject B \hookrightarrow \operatorname{coker}(M) along \operatorname{coker\_proj}(M) is isomorphic to \operatorname{coker}(B): \operatorname{coker}(\mathrm{pullback}) \cong \operatorname{coker}(B).

Construction: Constructs the canonical isomorphism using the nine-lemma / pullback-cokernel comparison in the interval category, detected via the left-heart functor.

🔗def
CategoryTheory.Triangulated.interval_cokernel_pullbackTopIso.{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]
  {s : CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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 : CategoryTheory.IsStrictMono B.arrow) :
  CategoryTheory.Limits.cokernel
      ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π M.arrow)).obj
          B).arrow ≅
    CategoryTheory.Limits.cokernel B.arrow
CategoryTheory.Triangulated.interval_cokernel_pullbackTopIso.{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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  [CategoryTheory.IsTriangulated 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 :
    CategoryTheory.IsStrictMono B.arrow) :
  CategoryTheory.Limits.cokernel
      ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π
                M.arrow)).obj
          B).arrow ≅
    CategoryTheory.Limits.cokernel B.arrow

Something wrong, better idea? Suggest a change

14.20.11. semistable_of_upper_inclusion🔗

Semistability transfers through upper interval inclusion: if E is \operatorname{ssf}-semistable in \mathcal{P}((a, b_1)) and b_1 \le b_2 with \mathcal{P}((a, b_1)) \subseteq \mathcal{P}((a, b_2)), then E is semistable in \mathcal{P}((a, b_2)) at the same phase.

Proof: Use semistable_of_target_envelope_triangleTest: the W-phase independence across branch cuts ensures the phase is unchanged, and the triangle test passes because the larger interval contains the smaller one.

🔗theorem
CategoryTheory.Triangulated.semistable_of_upper_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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a < b₁) (hab₂ : a < b₂) (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_upper_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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a < b₁)
  (hab₂ : a < b₂) (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