Bridgeland Stability Conditions

12.4. HeartEquivalence: Forward🔗

12.4.1. stabilityFunctionOnHeart🔗

Restrict a Bridgeland stability condition \sigma to the heart of its associated t-structure, producing the induced stability function on that abelian heart \mathcal{P}((0,1]).

Construction: The Z_{\mathrm{obj}} field sends E in the heart to \sigma.Z([E]) via the inclusion. Additivity follows from the K_0-relation for short exact sequences lifted from the heart to distinguished triangles. The upper half-plane condition uses the HN filtration: each HN factor lies in some \mathcal{P}(\varphi) with \varphi \in (0,1], so its central charge is in the upper half-plane; the sum of upper half-plane vectors remains in the upper half-plane.

🔗def
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart.{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]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) :
  CategoryTheory.StabilityFunction
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          σ.slicing).heart.FullSubcategory
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart.{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]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C) :
  CategoryTheory.StabilityFunction
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          σ.slicing).heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.4.2. stabilityFunctionOnHeart_phase_eq_of_mem_P_phi🔗

For E \in \mathcal{P}(\varphi) nonzero and \varphi \in (0,1], the heart stability-function phase of E equals \varphi.

Proof: The compatibility axiom gives Z(E) = m \, e^{i\pi\varphi} with m > 0. Dividing \arg(Z(E)) = \pi\varphi by \pi yields \varphi.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_phase_eq_of_mem_P_phi.{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]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1)
  (E :
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          σ.slicing).heart.FullSubcategory)
  (hP : σ.slicing.P φ E.obj) (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
          C σ).phase
      E =
    φ
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_phase_eq_of_mem_P_phi.{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]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1)
  (E :
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          σ.slicing).heart.FullSubcategory)
  (hP : σ.slicing.P φ E.obj)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
          C σ).phase
      E =
    φ

Something wrong, better idea? Suggest a change

12.4.3. stabilityFunctionOnHeart_phase_le_phiPlus🔗

For a nonzero heart object E, the heart stability-function phase is at most \varphi^+(E), the maximal HN phase.

Proof: Decomposes Z(E) as a sum over HN factors. Each factor's argument is at most \pi \varphi^+(E). The argument of a sum of upper half-plane vectors is at most the supremum of the individual arguments, so \arg(Z(E)) / \pi \le \varphi^+(E).

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_phase_le_phiPlus.{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]
  (σ : CategoryTheory.Triangulated.StabilityCondition C)
  (E :
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          σ.slicing).heart.FullSubcategory)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
          C σ).phase
      E ≤
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E.obj ⋯
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_phase_le_phiPlus.{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]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  (E :
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          σ.slicing).heart.FullSubcategory)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
          C σ).phase
      E ≤
    CategoryTheory.Triangulated.Slicing.phiPlus
      C σ.slicing E.obj ⋯

Something wrong, better idea? Suggest a change

12.4.4. stabilityFunctionOnHeart_isSemistable_of_mem_P_phi🔗

For \varphi \in (0,1], every nonzero E \in \mathcal{P}(\varphi) is semistable with respect to the heart stability function.

Proof: For any subobject B \hookrightarrow E in the heart, the Hom-vanishing property of the slicing forces \varphi^+(B) \le \varphi (otherwise a nonzero map from the top HN factor of B into E would exist, contradicting Hom vanishing from higher to lower phase). Since the heart phase of B is at most \varphi^+(B), we get \operatorname{phase}(B) \le \varphi = \operatorname{phase}(E).

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_isSemistable_of_mem_P_phi.{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]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1)
  (E :
    (CategoryTheory.Triangulated.Slicing.toTStructure C
          σ.slicing).heart.FullSubcategory)
  (hP : σ.slicing.P φ E.obj) (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
        C σ).IsSemistable
    E
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_isSemistable_of_mem_P_phi.{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]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1)
  (E :
    (CategoryTheory.Triangulated.Slicing.toTStructure
          C
          σ.slicing).heart.FullSubcategory)
  (hP : σ.slicing.P φ E.obj)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
        C σ).IsSemistable
    E

Something wrong, better idea? Suggest a change

12.4.5. phase_cokernel_ofLE_congr_local🔗

The phase of the cokernel of a subobject inclusion is invariant under propositionally equal subobjects.

Proof: Substitution on the subobject equalities.

🔗theorem
CategoryTheory.Triangulated.phase_cokernel_ofLE_congr_local.{u_1, u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} {A₁ A₂ B₁ B₂ : CategoryTheory.Subobject E} (hA : A₁ = A₂)
  (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} :
  Z.phase (CategoryTheory.Limits.cokernel (A₁.ofLE B₁ h₁)) =
    Z.phase (CategoryTheory.Limits.cokernel (A₂.ofLE B₂ h₂))
CategoryTheory.Triangulated.phase_cokernel_ofLE_congr_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  {A₁ A₂ B₁ B₂ :
    CategoryTheory.Subobject E}
  (hA : A₁ = A₂) (hB : B₁ = B₂)
  {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (A₁.ofLE B₁ h₁)) =
    Z.phase
      (CategoryTheory.Limits.cokernel
        (A₂.ofLE B₂ h₂))

Something wrong, better idea? Suggest a change

12.4.6. isSemistable_cokernel_ofLE_congr_local🔗

Semistability of the cokernel of a subobject inclusion is invariant under propositionally equal subobjects.

Proof: Substitution on the subobject equalities.

🔗theorem
CategoryTheory.Triangulated.isSemistable_cokernel_ofLE_congr_local.{u_1,
    u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} {A₁ A₂ B₁ B₂ : CategoryTheory.Subobject E} (hA : A₁ = A₂)
  (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂}
  (hs :
    Z.IsSemistable (CategoryTheory.Limits.cokernel (A₂.ofLE B₂ h₂))) :
  Z.IsSemistable (CategoryTheory.Limits.cokernel (A₁.ofLE B₁ h₁))
CategoryTheory.Triangulated.isSemistable_cokernel_ofLE_congr_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  {A₁ A₂ B₁ B₂ :
    CategoryTheory.Subobject E}
  (hA : A₁ = A₂) (hB : B₁ = B₂)
  {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂}
  (hs :
    Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (A₂.ofLE B₂ h₂))) :
  Z.IsSemistable
    (CategoryTheory.Limits.cokernel
      (A₁.ofLE B₁ h₁))

Something wrong, better idea? Suggest a change

12.4.7. map_eq_mk_mono_local🔗

For a monomorphism f : X \to Y and a subobject S \le X, the image subobject f_*(S) equals \operatorname{mk}(S.\mathrm{arrow} \circ f).

Proof: Rewrites using \texttt{Subobject.mk\_arrow} and \texttt{Subobject.map\_mk}.

🔗theorem
CategoryTheory.Triangulated.Subobject.map_eq_mk_mono_local.{u_1, u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] {X Y : A}
  (f : X ⟶ Y) [CategoryTheory.Mono f] (S : CategoryTheory.Subobject X) :
  (CategoryTheory.Subobject.map f).obj S =
    CategoryTheory.Subobject.mk
      (CategoryTheory.CategoryStruct.comp S.arrow f)
CategoryTheory.Triangulated.Subobject.map_eq_mk_mono_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  (S : CategoryTheory.Subobject X) :
  (CategoryTheory.Subobject.map f).obj S =
    CategoryTheory.Subobject.mk
      (CategoryTheory.CategoryStruct.comp
        S.arrow f)

Something wrong, better idea? Suggest a change

12.4.8. mapMonoIso_local🔗

The image of a subobject along a monomorphism is canonically isomorphic to the original subobject (as objects in the ambient category).

Construction: Constructs the isomorphism using \texttt{Subobject.isoOfEqMk} from the identity \texttt{map\_eq\_mk\_mono}.

🔗def
CategoryTheory.Triangulated.Subobject.mapMonoIso_local.{u_1, u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] {X Y : A}
  (f : X ⟶ Y) [CategoryTheory.Mono f] (S : CategoryTheory.Subobject X) :
  CategoryTheory.Subobject.underlying.obj
      ((CategoryTheory.Subobject.map f).obj S) ≅
    CategoryTheory.Subobject.underlying.obj S
CategoryTheory.Triangulated.Subobject.mapMonoIso_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  (S : CategoryTheory.Subobject X) :
  CategoryTheory.Subobject.underlying.obj
      ((CategoryTheory.Subobject.map
            f).obj
        S) ≅
    CategoryTheory.Subobject.underlying.obj
      S

Something wrong, better idea? Suggest a change

12.4.9. ofLE_map_comp_mapMonoIso_hom_local🔗

The canonical comparison between the image of an inclusion S \le T under a monomorphism f and the image of T, composed with the \texttt{mapMonoIso} isomorphism, equals the composition of \texttt{mapMonoIso}(S) and the original inclusion.

Proof: Checks equality after composing with the arrow of T, using monicity of f and the definition of \texttt{mapMonoIso}.

🔗theorem
CategoryTheory.Triangulated.Subobject.ofLE_map_comp_mapMonoIso_hom_local.{u_1,
    u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] {X Y : A}
  (f : X ⟶ Y) [CategoryTheory.Mono f] {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Subobject.map f).obj S).ofLE
        ((CategoryTheory.Subobject.map f).obj T) ⋯)
      (CategoryTheory.Triangulated.Subobject.mapMonoIso_local f T).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.Subobject.mapMonoIso_local f S).hom
      (S.ofLE T h)
CategoryTheory.Triangulated.Subobject.ofLE_map_comp_mapMonoIso_hom_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Subobject.map
                f).obj
            S).ofLE
        ((CategoryTheory.Subobject.map
              f).obj
          T)
        ⋯)
      (CategoryTheory.Triangulated.Subobject.mapMonoIso_local
          f T).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.Subobject.mapMonoIso_local
          f S).hom
      (S.ofLE T h)

Something wrong, better idea? Suggest a change

12.4.10. cokernelMapMonoIso_local🔗

Taking cokernels after mapping a subobject inclusion along a monomorphism does not change the resulting quotient object.

Construction: Uses \texttt{cokernel.mapIso} with the two \texttt{mapMonoIso} isomorphisms.

🔗def
CategoryTheory.Triangulated.Subobject.cokernelMapMonoIso_local.{u_1,
    u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f] {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  CategoryTheory.Limits.cokernel
      (((CategoryTheory.Subobject.map f).obj S).ofLE
        ((CategoryTheory.Subobject.map f).obj T) ⋯) ≅
    CategoryTheory.Limits.cokernel (S.ofLE T h)
CategoryTheory.Triangulated.Subobject.cokernelMapMonoIso_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] {X Y : A}
  (f : X ⟶ Y) [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  CategoryTheory.Limits.cokernel
      (((CategoryTheory.Subobject.map
                f).obj
            S).ofLE
        ((CategoryTheory.Subobject.map
              f).obj
          T)
        ⋯) ≅
    CategoryTheory.Limits.cokernel
      (S.ofLE T h)

Something wrong, better idea? Suggest a change

12.4.11. phase_cokernel_mapMono_eq_local🔗

The stability phase of the cokernel of a subobject inclusion is preserved under pushing forward by a monomorphism.

Proof: Uses \texttt{phase\_eq\_of\_iso} applied to \texttt{cokernelMapMonoIso\_local}.

🔗theorem
CategoryTheory.Triangulated.phase_cokernel_mapMono_eq_local.{u_1, u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (f : X ⟶ Y) [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X} (h : S ≤ T) :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map f).obj S).ofLE
          ((CategoryTheory.Subobject.map f).obj T) ⋯)) =
    Z.phase (CategoryTheory.Limits.cokernel (S.ofLE T h))
CategoryTheory.Triangulated.phase_cokernel_mapMono_eq_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map
                  f).obj
              S).ofLE
          ((CategoryTheory.Subobject.map
                f).obj
            T)
          ⋯)) =
    Z.phase
      (CategoryTheory.Limits.cokernel
        (S.ofLE T h))

Something wrong, better idea? Suggest a change

12.4.12. isSemistable_cokernel_mapMono_iff_local🔗

Semistability of the cokernel of a subobject inclusion is preserved under pushing forward by a monomorphism: Z.\texttt{IsSemistable}(\operatorname{coker}(f_*(S) \to f_*(T))) iff Z.\texttt{IsSemistable}(\operatorname{coker}(S \to T)).

Proof: In both directions, uses \texttt{cokernelMapMonoIso\_local} (and its symmetric) to transfer semistability via \texttt{isSemistable\_of\_iso}.

🔗theorem
CategoryTheory.Triangulated.isSemistable_cokernel_mapMono_iff_local.{u_1,
    u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (f : X ⟶ Y) [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X} (h : S ≤ T) :
  Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map f).obj S).ofLE
          ((CategoryTheory.Subobject.map f).obj T) ⋯)) ↔
    Z.IsSemistable (CategoryTheory.Limits.cokernel (S.ofLE T h))
CategoryTheory.Triangulated.isSemistable_cokernel_mapMono_iff_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map
                  f).obj
              S).ofLE
          ((CategoryTheory.Subobject.map
                f).obj
            T)
          ⋯)) ↔
    Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (S.ofLE T h))

Something wrong, better idea? Suggest a change

12.4.13. exists_hn_with_last_phase_of_semistable_local🔗

A semistable object admits an HN filtration whose last phase equals the object's stability-function phase.

Proof: Delegates to the general existence result \texttt{exists\_hn\_with\_last\_phase\_of\_semistable}.

🔗theorem
CategoryTheory.Triangulated.StabilityFunction.exists_hn_with_last_phase_of_semistable_local.{u_1,
    u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hss : Z.IsSemistable E) : ∃ F, F.φ ⟨F.n - 1, ⋯⟩ = Z.phase E
CategoryTheory.Triangulated.StabilityFunction.exists_hn_with_last_phase_of_semistable_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hss : Z.IsSemistable E) :
  ∃ F, F.φ ⟨F.n - 1, ⋯⟩ = Z.phase E

Something wrong, better idea? Suggest a change

12.4.14. append_hn_filtration_of_mono_local🔗

Given a monomorphism i : X \hookrightarrow Y with semistable cokernel B of phase strictly less than the last HN phase of X, one can append B to obtain an HN filtration of Y.

Proof: Delegates to \texttt{append\_hn\_filtration\_of\_mono}.

🔗theorem
CategoryTheory.Triangulated.StabilityFunction.append_hn_filtration_of_mono_local.{u_1,
    u_2}
  {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {X Y B : A} (i : X ⟶ Y) [CategoryTheory.Mono i]
  (F : CategoryTheory.AbelianHNFiltration Z X)
  (eB : CategoryTheory.Limits.cokernel i ≅ B) (hB : Z.IsSemistable B)
  (hlast : Z.phase B < F.φ ⟨F.n - 1, ⋯⟩) :
  ∃ G, G.φ ⟨G.n - 1, ⋯⟩ = Z.phase B
CategoryTheory.Triangulated.StabilityFunction.append_hn_filtration_of_mono_local.{u_1,
    u_2}
  {A : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y B : A} (i : X ⟶ Y)
  [CategoryTheory.Mono i]
  (F :
    CategoryTheory.AbelianHNFiltration Z
      X)
  (eB :
    CategoryTheory.Limits.cokernel i ≅ B)
  (hB : Z.IsSemistable B)
  (hlast : Z.phase B < F.φ ⟨F.n - 1, ⋯⟩) :
  ∃ G, G.φ ⟨G.n - 1, ⋯⟩ = Z.phase B

Something wrong, better idea? Suggest a change