Bridgeland Stability Conditions

14.11. Deformation: IntervalSelection🔗

14.11.1. intervalSubobject_isZero_iff_eq_bot🔗

For an object X in an interval subcategory \mathcal{P}((a,b)), a subobject B \leq X is a zero object if and only if B = \bot in \mathrm{Sub}(X).

Proof: If B is zero, its defining arrow is zero, hence B = \mathrm{mk}(0) = \bot by Subobject.mk_eq_bot_iff_zero. Conversely, \bot coerces to the zero object in \mathcal{P}((a,b)) via the canonical isomorphism Subobject.botCoeIsoZero.

🔗theorem
CategoryTheory.Triangulated.intervalSubobject_isZero_iff_eq_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]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (B : CategoryTheory.Subobject X) :
  CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj B) ↔
    B = ⊥
CategoryTheory.Triangulated.intervalSubobject_isZero_iff_eq_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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (B : CategoryTheory.Subobject X) :
  CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj
        B) ↔
    B = ⊥

Something wrong, better idea? Suggest a change

14.11.2. intervalSubobject_not_isZero_of_ne_bot🔗

If B \neq \bot as a subobject of X in an interval category, then B is not a zero object.

Proof: This is the contrapositive of intervalSubobject_isZero_iff_eq_bot: being zero implies being \bot.

🔗theorem
CategoryTheory.Triangulated.intervalSubobject_not_isZero_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]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  {B : CategoryTheory.Subobject X} (h : B ≠ ⊥) :
  ¬CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj B)
CategoryTheory.Triangulated.intervalSubobject_not_isZero_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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  {B : CategoryTheory.Subobject X}
  (h : B ≠ ⊥) :
  ¬CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj
        B)

Something wrong, better idea? Suggest a change

14.11.3. intervalSubobject_top_ne_bot_of_not_isZero🔗

If X is a nonzero object in an interval category \mathcal{P}((a,b)), then the top subobject \top \in \mathrm{Sub}(X) is not equal to \bot.

Proof: If \top = \bot, then by intervalSubobject_isZero_iff_eq_bot the top subobject is zero, and since the top subobject arrow is an isomorphism, X itself would be zero, contradicting the hypothesis.

🔗theorem
CategoryTheory.Triangulated.intervalSubobject_top_ne_bot_of_not_isZero.{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} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) : ⊤ ≠ ⊥
CategoryTheory.Triangulated.intervalSubobject_top_ne_bot_of_not_isZero.{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}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ⊤ ≠ ⊥

Something wrong, better idea? Suggest a change

14.11.4. intervalSubobject_arrow_strictMono_of_strictMono🔗

If f : Y \to X is a strict monomorphism in a thin interval category \mathcal{P}((a,b)) with b - a \leq 1, then the arrow of the subobject \mathrm{mk}(f) \hookrightarrow X is also a strict monomorphism.

Proof: The arrow of \mathrm{mk}(f) is the composition of the underlying isomorphism e.\mathrm{hom} with f. Both factors are strict mono (the first by isStrictMono_of_isIso, the second by hypothesis), and their composition is strict mono by the interval composition lemma.

🔗theorem
CategoryTheory.Triangulated.intervalSubobject_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] [CategoryTheory.IsTriangulated C]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : Y ⟶ X) (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.IsStrictMono (CategoryTheory.Subobject.mk f).arrow
CategoryTheory.Triangulated.intervalSubobject_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]
  [CategoryTheory.IsTriangulated C]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : Y ⟶ X)
  (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.IsStrictMono
    (CategoryTheory.Subobject.mk f).arrow

Something wrong, better idea? Suggest a change

14.11.5. interval_strictShortExact_cokernel_of_strictMono🔗

A strict monomorphism f : Y \hookrightarrow X in the interval subcategory \mathcal{P}((a, b)) with b - a \le 1 gives rise to a strict short exact sequence Y \hookrightarrow X \twoheadrightarrow \operatorname{coker}(f).

Proof: Embed into the abelian left heart via the functor \mathcal{P}((a,b)) \to \mathcal{P}((a, a+1]). The strict mono maps to a mono with epi cokernel projection. Extract the short exact sequence in the heart, lift to a distinguished triangle, and pull back strict short exactness.

🔗theorem
CategoryTheory.Triangulated.interval_strictShortExact_cokernel_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] [CategoryTheory.IsTriangulated C]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : Y ⟶ X) (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.StrictShortExact
    { X₁ := Y, X₂ := X, X₃ := CategoryTheory.Limits.cokernel f, f := f,
      g := CategoryTheory.Limits.cokernel.π f, zero := ⋯ }
CategoryTheory.Triangulated.interval_strictShortExact_cokernel_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]
  [CategoryTheory.IsTriangulated C]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : Y ⟶ X)
  (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.StrictShortExact
    { X₁ := Y, X₂ := X,
      X₃ :=
        CategoryTheory.Limits.cokernel f,
      f := f,
      g :=
        CategoryTheory.Limits.cokernel.π
          f,
      zero := ⋯ }

Something wrong, better idea? Suggest a change

14.11.6. intervalInclusion_map_strictMono🔗

The inclusion functor between nested interval subcategories preserves strict monomorphisms.

Proof: A strict mono f in \mathcal{P}((a_1, b_1)) gives a strict short exact sequence. Map through the inclusion to get a distinguished triangle in \mathcal{P}((a_2, b_2)), which yields strict mono/epi.

🔗theorem
CategoryTheory.Triangulated.intervalInclusion_map_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] [CategoryTheory.IsTriangulated C]
  {s₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  (f : X ⟶ Y) (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.IsStrictMono
    ((CategoryTheory.ObjectProperty.ιOfLE h).map f)
CategoryTheory.Triangulated.intervalInclusion_map_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]
  [CategoryTheory.IsTriangulated C]
  {s₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  (f : X ⟶ Y)
  (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.IsStrictMono
    ((CategoryTheory.ObjectProperty.ιOfLE
          h).map
      f)

Something wrong, better idea? Suggest a change

14.11.7. interval_strictArtinianObject_of_inclusion🔗

If X in \mathcal{P}((a_1, b_1)) has Artinian image in the wider \mathcal{P}((a_2, b_2)), then X is strict Artinian.

Proof: Since the inclusion is faithful and preserves strict monos, any descending chain of strict subobjects in the source maps injectively to one in the target.

🔗theorem
CategoryTheory.Triangulated.interval_strictArtinianObject_of_inclusion.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  [CategoryTheory.IsArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)] :
  CategoryTheory.IsStrictArtinianObject X
CategoryTheory.Triangulated.interval_strictArtinianObject_of_inclusion.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  [CategoryTheory.IsArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)] :
  CategoryTheory.IsStrictArtinianObject X

Something wrong, better idea? Suggest a change

14.11.8. interval_strictNoetherianObject_of_inclusion🔗

If X in \mathcal{P}((a_1, b_1)) has Noetherian image in the wider \mathcal{P}((a_2, b_2)), then X is strict Noetherian.

Proof: Dual of interval_strictArtinianObject_of_inclusion for ascending chains.

🔗theorem
CategoryTheory.Triangulated.interval_strictNoetherianObject_of_inclusion.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  [CategoryTheory.IsNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)] :
  CategoryTheory.IsStrictNoetherianObject X
CategoryTheory.Triangulated.interval_strictNoetherianObject_of_inclusion.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  [CategoryTheory.IsNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)] :
  CategoryTheory.IsStrictNoetherianObject
    X

Something wrong, better idea? Suggest a change

14.11.9. interval_strictFiniteLength_of_inclusion🔗

If X in \mathcal{P}((a_1, b_1)) has Artinian and Noetherian image in the wider interval, then X has strict finite length.

Proof: Combines interval_strictArtinianObject_of_inclusion and interval_strictNoetherianObject_of_inclusion.

🔗theorem
CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  [CategoryTheory.IsArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)]
  [CategoryTheory.IsNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)] :
  CategoryTheory.IsStrictArtinianObject X ∧
    CategoryTheory.IsStrictNoetherianObject X
CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  [CategoryTheory.IsArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)]
  [CategoryTheory.IsNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)] :
  CategoryTheory.IsStrictArtinianObject
      X ∧
    CategoryTheory.IsStrictNoetherianObject
      X

Something wrong, better idea? Suggest a change

14.11.10. interval_thinFiniteLength_of_inclusion🔗

If every object in \mathcal{P}((a_2, b_2)) has finite length, then every object in the narrower \mathcal{P}((a_1, b_1)) has strict finite length.

Proof: Apply interval_strictFiniteLength_of_inclusion to each object, using the ambient finite length hypothesis.

🔗theorem
CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  (hFinite :
    ∀ (Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s₂ a₂ b₂),
      CategoryTheory.IsArtinianObject Y ∧
        CategoryTheory.IsNoetherianObject Y)
  (X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁) :
  CategoryTheory.IsStrictArtinianObject X ∧
    CategoryTheory.IsStrictNoetherianObject X
CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  (hFinite :
    ∀
      (Y :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C s₂ a₂ b₂),
      CategoryTheory.IsArtinianObject Y ∧
        CategoryTheory.IsNoetherianObject
          Y)
  (X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁) :
  CategoryTheory.IsStrictArtinianObject
      X ∧
    CategoryTheory.IsStrictNoetherianObject
      X

Something wrong, better idea? Suggest a change

14.11.11. interval_strictArtinianObject_of_inclusion_strict🔗

If the inclusion \mathcal{P}((a_1,b_1)) \hookrightarrow \mathcal{P}((a_2,b_2)) holds and X viewed in the larger interval category is strictly Artinian, then X is strictly Artinian in \mathcal{P}((a_1,b_1)).

Proof: The inclusion functor I sends strict subobjects of X to strict subobjects of I(X) injectively and monotonically (via intervalInclusion_map_strictMono). Any descending chain in strict subobjects of X gives a descending chain for I(X), which terminates by strict Artinian hypothesis; injectivity then implies the original chain terminates.

🔗theorem
CategoryTheory.Triangulated.interval_strictArtinianObject_of_inclusion_strict.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  [CategoryTheory.IsStrictArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)] :
  CategoryTheory.IsStrictArtinianObject X
CategoryTheory.Triangulated.interval_strictArtinianObject_of_inclusion_strict.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  [CategoryTheory.IsStrictArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)] :
  CategoryTheory.IsStrictArtinianObject X

Something wrong, better idea? Suggest a change

14.11.12. interval_strictNoetherianObject_of_inclusion_strict🔗

If the inclusion \mathcal{P}((a_1,b_1)) \hookrightarrow \mathcal{P}((a_2,b_2)) holds and X viewed in the larger interval category is strictly Noetherian, then X is strictly Noetherian in \mathcal{P}((a_1,b_1)).

Proof: Dual to the Artinian case: the inclusion functor I transports ascending chains of strict subobjects of X to ascending chains for I(X) injectively and monotonically, and these terminate by the strictly Noetherian hypothesis; injectivity then yields termination in the original category.

🔗theorem
CategoryTheory.Triangulated.interval_strictNoetherianObject_of_inclusion_strict.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  [CategoryTheory.IsStrictNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)] :
  CategoryTheory.IsStrictNoetherianObject X
CategoryTheory.Triangulated.interval_strictNoetherianObject_of_inclusion_strict.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  [CategoryTheory.IsStrictNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)] :
  CategoryTheory.IsStrictNoetherianObject
    X

Something wrong, better idea? Suggest a change

14.11.13. interval_strictFiniteLength_of_inclusion_strict🔗

If X in the smaller interval category \mathcal{P}((a_1,b_1)) maps into \mathcal{P}((a_2,b_2)) and is both strictly Artinian and strictly Noetherian there, then X is both strictly Artinian and strictly Noetherian in \mathcal{P}((a_1,b_1)).

Proof: This combines interval_strictArtinianObject_of_inclusion_strict and interval_strictNoetherianObject_of_inclusion_strict into a single conjunction.

🔗theorem
CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion_strict.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁}
  [CategoryTheory.IsStrictArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)]
  [CategoryTheory.IsStrictNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)] :
  CategoryTheory.IsStrictArtinianObject X ∧
    CategoryTheory.IsStrictNoetherianObject X
CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion_strict.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁}
  [CategoryTheory.IsStrictArtinianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)]
  [CategoryTheory.IsStrictNoetherianObject
      ((CategoryTheory.ObjectProperty.ιOfLE
            h).obj
        X)] :
  CategoryTheory.IsStrictArtinianObject
      X ∧
    CategoryTheory.IsStrictNoetherianObject
      X

Something wrong, better idea? Suggest a change

14.11.14. interval_thinFiniteLength_of_inclusion_strict🔗

If every object of the larger interval category \mathcal{P}((a_2,b_2)) is strictly Artinian and strictly Noetherian, and \mathcal{P}((a_1,b_1)) \hookrightarrow \mathcal{P}((a_2,b_2)), then every object of \mathcal{P}((a_1,b_1)) is also strictly Artinian and strictly Noetherian.

Proof: For each X \in \mathcal{P}((a_1,b_1)), apply the finite-length hypothesis to I(X) in the larger category, then use interval_strictFiniteLength_of_inclusion_strict to transport the conclusion back.

🔗theorem
CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion_strict.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C} {a₁ b₁ a₂ b₂ : ℝ}
  [Fact (a₁ < b₁)] [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp C s₂ a₂ b₂)
  (hFinite :
    ∀ (Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s₂ a₂ b₂),
      CategoryTheory.IsStrictArtinianObject Y ∧
        CategoryTheory.IsStrictNoetherianObject Y)
  (X : CategoryTheory.Triangulated.Slicing.IntervalCat C s₁ a₁ b₁) :
  CategoryTheory.IsStrictArtinianObject X ∧
    CategoryTheory.IsStrictNoetherianObject X
CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion_strict.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C}
  {a₁ b₁ a₂ b₂ : ℝ} [Fact (a₁ < b₁)]
  [Fact (b₁ - a₁ ≤ 1)] [Fact (a₂ < b₂)]
  [Fact (b₂ - a₂ ≤ 1)]
  (h :
    CategoryTheory.Triangulated.Slicing.intervalProp
        C s₁ a₁ b₁ ≤
      CategoryTheory.Triangulated.Slicing.intervalProp
        C s₂ a₂ b₂)
  (hFinite :
    ∀
      (Y :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C s₂ a₂ b₂),
      CategoryTheory.IsStrictArtinianObject
          Y ∧
        CategoryTheory.IsStrictNoetherianObject
          Y)
  (X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s₁ a₁ b₁) :
  CategoryTheory.IsStrictArtinianObject
      X ∧
    CategoryTheory.IsStrictNoetherianObject
      X

Something wrong, better idea? Suggest a change

14.11.15. of_wide🔗

The thin-sector finite length hypothesis follows from the wide-sector one: \operatorname{WideSectorFiniteLength}(\sigma, \varepsilon_0) \Rightarrow \operatorname{SectorFiniteLength}(\sigma, 2\varepsilon_0).

Proof: A 2\varepsilon_0-interval is contained in a 4\varepsilon_0-interval, so apply interval_thinFiniteLength_of_inclusion.

🔗theorem
CategoryTheory.Triangulated.SectorFiniteLength.of_wide.{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)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀
      hε₀8) :
  CategoryTheory.Triangulated.SectorFiniteLength C σ ε₀ hε₀ hε₀2
CategoryTheory.Triangulated.SectorFiniteLength.of_wide.{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)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ hε₀8) :
  CategoryTheory.Triangulated.SectorFiniteLength
    C σ ε₀ hε₀ hε₀2

Something wrong, better idea? Suggest a change

14.11.16. interval_K0_of_strictMono🔗

If f : Y \hookrightarrow X is a strict monomorphism in a thin interval category \mathcal{P}((a,b)) with b - a \leq 1, then [X] = [Y] + [\mathrm{coker}(f)] in K_0(\mathcal{C}) after applying the class map v.

Proof: The strict mono f fits into a strict short exact sequence Y \to X \to \mathrm{coker}(f) by interval_strictShortExact_cokernel_of_strictMono; additivity of the K_0 class map on strict short exact sequences then gives the formula.

🔗theorem
CategoryTheory.Triangulated.interval_K0_of_strictMono.{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 : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (f : Y ⟶ X) (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.Triangulated.cl C v X.obj =
    CategoryTheory.Triangulated.cl C v Y.obj +
      CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel f).obj
CategoryTheory.Triangulated.interval_K0_of_strictMono.{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 : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (f : Y ⟶ X)
  (hf : CategoryTheory.IsStrictMono f) :
  CategoryTheory.Triangulated.cl C v
      X.obj =
    CategoryTheory.Triangulated.cl C v
        Y.obj +
      CategoryTheory.Triangulated.cl C v
        (CategoryTheory.Limits.cokernel
            f).obj

Something wrong, better idea? Suggest a change

14.11.17. interval_card_subobject_lt_of_ne_top🔗

If M \subsetneq X is a proper subobject in an interval category with finitely many subobjects, then the number of subobjects of M is strictly less than the number of subobjects of X.

Proof: The map sending A \in \mathrm{Sub}(M) to \mathrm{map}(M.\mathrm{arrow})(A) \in \mathrm{Sub}(X) is injective. The top subobject \top \in \mathrm{Sub}(X) is not in its image, since being in the image would force M = \top; Fintype.card_lt_of_injective_of_notMem then gives strict inequality.

🔗theorem
CategoryTheory.Triangulated.interval_card_subobject_lt_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]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  {M : CategoryTheory.Subobject X} (hM : M ≠ ⊤)
  [Finite (CategoryTheory.Subobject X)] :
  Nat.card
      (CategoryTheory.Subobject
        (CategoryTheory.Subobject.underlying.obj M)) <
    Nat.card (CategoryTheory.Subobject X)
CategoryTheory.Triangulated.interval_card_subobject_lt_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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  {M : CategoryTheory.Subobject X}
  (hM : M ≠ ⊤)
  [Finite (CategoryTheory.Subobject X)] :
  Nat.card
      (CategoryTheory.Subobject
        (CategoryTheory.Subobject.underlying.obj
          M)) <
    Nat.card (CategoryTheory.Subobject X)

Something wrong, better idea? Suggest a change

14.11.18. intervalLiftSub🔗

Given a strict subobject B of the cokernel \operatorname{coker}(M.\operatorname{arrow}) in an interval subcategory, lift it to a subobject of X containing M via pullback along the cokernel projection.

Construction: Defined as the pullback (\operatorname{cokernel}.\pi \circ M.\operatorname{arrow})^*(B).

🔗def
CategoryTheory.Triangulated.intervalLiftSub.{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} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  (A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)) :
  CategoryTheory.Subobject X
CategoryTheory.Triangulated.intervalLiftSub.{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}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  (A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)) :
  CategoryTheory.Subobject X

Something wrong, better idea? Suggest a change

14.11.19. intervalLiftSub_le🔗

For any subobject A \leq M in the interval category, the lifted subobject \widetilde{A} \leq X satisfies \widetilde{A} \leq M as a subobject of X.

Proof: The composite A.\mathrm{arrow} \circ M.\mathrm{arrow} factors through M.\mathrm{arrow} via A.\mathrm{arrow}, giving the required inequality by Subobject.mk_le_mk_of_comm.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_le.{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} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  (A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)) :
  CategoryTheory.Triangulated.intervalLiftSub C M A ≤ M
CategoryTheory.Triangulated.intervalLiftSub_le.{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}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  (A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)) :
  CategoryTheory.Triangulated.intervalLiftSub
      C M A ≤
    M

Something wrong, better idea? Suggest a change

14.11.20. intervalLiftSub_bot🔗

Lifting the bottom subobject \bot \leq M to a subobject of X gives the bottom subobject \bot \leq X.

Proof: The composite arrow 0 \circ M.\mathrm{arrow} is zero, so the corresponding subobject is \bot by Subobject.mk_eq_bot_iff_zero.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_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]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X) :
  CategoryTheory.Triangulated.intervalLiftSub C M ⊥ = ⊥
CategoryTheory.Triangulated.intervalLiftSub_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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X) :
  CategoryTheory.Triangulated.intervalLiftSub
      C M ⊥ =
    ⊥

Something wrong, better idea? Suggest a change

14.11.21. intervalLiftSub_ne_bot🔗

If A \neq \bot in \mathrm{Sub}(M), then the lifted subobject \widetilde{A} is also nonzero, i.e., \widetilde{A} \neq \bot in \mathrm{Sub}(X).

Proof: If \widetilde{A} = \bot, then A.\mathrm{arrow} \circ M.\mathrm{arrow} = 0; since M.\mathrm{arrow} is a monomorphism, A.\mathrm{arrow} = 0, forcing A = \bot, contradicting the hypothesis.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_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]
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)}
  (hA : A ≠ ⊥) : CategoryTheory.Triangulated.intervalLiftSub C M A ≠ ⊥
CategoryTheory.Triangulated.intervalLiftSub_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]
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)}
  (hA : A ≠ ⊥) :
  CategoryTheory.Triangulated.intervalLiftSub
      C M A ≠
    ⊥

Something wrong, better idea? Suggest a change

14.11.22. intervalLiftSub_mono🔗

The operation of lifting subobjects of M to subobjects of X is monotone: if A \leq B in \mathrm{Sub}(M), then \widetilde{A} \leq \widetilde{B} in \mathrm{Sub}(X).

Proof: The morphism Subobject.ofLE A B h witnesses the inequality at the level of arrows, and Subobject.mk_le_mk_of_comm with this morphism gives the desired inequality of lifted subobjects.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_mono.{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} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  {A B :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)}
  (h : A ≤ B) :
  CategoryTheory.Triangulated.intervalLiftSub C M A ≤
    CategoryTheory.Triangulated.intervalLiftSub C M B
CategoryTheory.Triangulated.intervalLiftSub_mono.{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}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  {A B :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)}
  (h : A ≤ B) :
  CategoryTheory.Triangulated.intervalLiftSub
      C M A ≤
    CategoryTheory.Triangulated.intervalLiftSub
      C M B

Something wrong, better idea? Suggest a change

14.11.23. intervalLiftSub_lt🔗

If A is a proper subobject of M (i.e., A \neq \top in \mathrm{Sub}(M)), then the lifted subobject \widetilde{A} is strictly smaller than M as a subobject of X.

Proof: Since \widetilde{A} \leq M by intervalLiftSub_le, it suffices to show \widetilde{A} \neq M. Equality would force A = \top via the injectivity of the map \mathrm{Sub}(M) \to \mathrm{Sub}(X) sending a subobject to its composition with M.\mathrm{arrow}, contradicting the hypothesis.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_lt.{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} {a b : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)}
  (hA : A ≠ ⊤) : CategoryTheory.Triangulated.intervalLiftSub C M A < M
CategoryTheory.Triangulated.intervalLiftSub_lt.{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}
  {a b : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)}
  (hA : A ≠ ⊤) :
  CategoryTheory.Triangulated.intervalLiftSub
      C M A <
    M

Something wrong, better idea? Suggest a change

14.11.24. intervalSubobject_bot_arrow_strictMono🔗

The arrow of the bottom subobject \bot \hookrightarrow X in a thin interval category \mathcal{P}((a,b)) with b - a \leq 1 is a strict monomorphism.

Proof: The bottom arrow is the zero morphism 0 \colon 0 \to X. Its cokernel map X \to X is an isomorphism, so the zero morphism is a strict mono by the kernel fork limit characterization applied to the fact that the source is a zero object.

🔗theorem
CategoryTheory.Triangulated.intervalSubobject_bot_arrow_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] [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} :
  CategoryTheory.IsStrictMono ⊥.arrow
CategoryTheory.Triangulated.intervalSubobject_bot_arrow_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]
  [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} :
  CategoryTheory.IsStrictMono ⊥.arrow

Something wrong, better idea? Suggest a change

14.11.25. intervalLiftSub_arrow_strictMono_of_strictMono🔗

If M \hookrightarrow X and A \hookrightarrow M are both strict monomorphisms in a thin interval category \mathcal{P}((a,b)), then the arrow of the lifted subobject \widetilde{A} \hookrightarrow X is also a strict monomorphism.

Proof: The composite A \to M \to X is strict mono by the interval composition lemma; the arrow of the corresponding subobject of X is then strict mono by intervalSubobject_arrow_strictMono_of_strictMono.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_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] [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)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)}
  (hA : CategoryTheory.IsStrictMono A.arrow) :
  CategoryTheory.IsStrictMono
    (CategoryTheory.Triangulated.intervalLiftSub C M A).arrow
CategoryTheory.Triangulated.intervalLiftSub_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]
  [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)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)}
  (hA :
    CategoryTheory.IsStrictMono A.arrow) :
  CategoryTheory.IsStrictMono
    (CategoryTheory.Triangulated.intervalLiftSub
        C M A).arrow

Something wrong, better idea? Suggest a change

14.11.26. intervalLiftSub_wPhase_eq🔗

The W-phase of the lifted subobject \widetilde{A} \leq X in the interval category equals the W-phase of A \leq M: \phi_W(\widetilde{A}) = \phi_W(A).

Proof: The underlying interval object of \widetilde{A} is canonically isomorphic to that of A via Subobject.underlyingIso, so the W-phase is preserved by wPhase_iso.

🔗theorem
CategoryTheory.Triangulated.intervalLiftSub_wPhase_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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (M : CategoryTheory.Subobject X)
  (A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj M)) :
  ssf.wPhase
      (CategoryTheory.Subobject.underlying.obj
          (CategoryTheory.Triangulated.intervalLiftSub C M A)).obj =
    ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj
CategoryTheory.Triangulated.intervalLiftSub_wPhase_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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (M : CategoryTheory.Subobject X)
  (A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        M)) :
  ssf.wPhase
      (CategoryTheory.Subobject.underlying.obj
          (CategoryTheory.Triangulated.intervalLiftSub
            C M A)).obj =
    ssf.wPhase
      (CategoryTheory.Subobject.underlying.obj
          A).obj

Something wrong, better idea? Suggest a change

14.11.27. exists_phase_gt_strictSubobject_of_not_semistable🔗

If an interval object X is not W-semistable at its own W-phase, then there exists a nonzero strict subobject whose W-phase strictly exceeds that of X.

Proof: The failure of W-semistability provides a distinguished triangle K \to X \to Q with \operatorname{wPhaseOf}(W(K)) > \operatorname{wPhaseOf}(W(X)). The strict mono K \hookrightarrow X gives the desired subobject.

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

Something wrong, better idea? Suggest a change

14.11.28. intervalLiftSubCokernelIso🔗

For subobjects A \leq B of an interval subobject M \leq X in \mathcal{P}((a,b)), the cokernel of the inclusion \widetilde{A} \hookrightarrow \widetilde{B} of their lifts to X is canonically isomorphic to the cokernel of the original inclusion A \hookrightarrow B inside M.

Construction: The isomorphism is constructed via the canonical identifications \widetilde{A} \cong A and \widetilde{B} \cong B given by Subobject.underlyingIso, together with a compatibility check that the lift of the inclusion equals the composition with these isomorphisms, then applying cokernel.mapIso.

🔗def
CategoryTheory.Triangulated.intervalLiftSubCokernelIso.{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.Subobject.underlying.obj M)}
  (h : A ≤ B) :
  CategoryTheory.Limits.cokernel
      ((CategoryTheory.Triangulated.intervalLiftSub C M A).ofLE
        (CategoryTheory.Triangulated.intervalLiftSub C M B) ⋯) ≅
    CategoryTheory.Limits.cokernel (A.ofLE B h)
CategoryTheory.Triangulated.intervalLiftSubCokernelIso.{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.Subobject.underlying.obj
        M)}
  (h : A ≤ B) :
  CategoryTheory.Limits.cokernel
      ((CategoryTheory.Triangulated.intervalLiftSub
            C M A).ofLE
        (CategoryTheory.Triangulated.intervalLiftSub
          C M B)
        ⋯) ≅
    CategoryTheory.Limits.cokernel
      (A.ofLE B h)

Something wrong, better idea? Suggest a change

14.11.29. exists_minPhase_maximal_strictKernel🔗

Given a non-semistable non-zero object X in a thin interval category \mathcal{P}((a,b)) with finitely many subobjects, there exists a proper strict kernel M \subsetneq X whose strict quotient X/M has minimal W-phase among all proper strict kernels, and which is maximal for inclusion among all proper strict kernels realizing that minimum quotient W-phase. Any proper strict kernel strictly contained in M has strictly larger quotient phase.

Proof: Non-semistability of X supplies an initial proper strict kernel. Among all proper strict kernels, the finite set has a minimum quotient phase realized by some M_0. Among kernels with the same minimal quotient phase, a maximal one M is chosen by inclusion; finiteness guarantees existence. Strict phase increase for subobjects of M follows from the maximality of M in that equal-phase class.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_minPhase_maximal_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}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj))
  [Finite (CategoryTheory.Subobject X)] :
  ∃ M,
    M ≠ ⊤ ∧
      CategoryTheory.IsStrictMono M.arrow ∧
        (∀ (B : CategoryTheory.Subobject X),
            B ≠ ⊤ →
              CategoryTheory.IsStrictMono B.arrow →
                ssf.wPhase
                    (CategoryTheory.Limits.cokernel M.arrow).obj ≤
                  ssf.wPhase
                    (CategoryTheory.Limits.cokernel B.arrow).obj) ∧
          ∀ (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
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_minPhase_maximal_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}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj))
  [Finite (CategoryTheory.Subobject X)] :
  ∃ M,
    M ≠ ⊤ ∧
      CategoryTheory.IsStrictMono
          M.arrow ∧
        (∀
            (B :
              CategoryTheory.Subobject X),
            B ≠ ⊤ →
              CategoryTheory.IsStrictMono
                  B.arrow →
                ssf.wPhase
                    (CategoryTheory.Limits.cokernel
                        M.arrow).obj ≤
                  ssf.wPhase
                    (CategoryTheory.Limits.cokernel
                        B.arrow).obj) ∧
          ∀
            (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

Something wrong, better idea? Suggest a change

14.11.30. exists_minPhase_minimal_strictKernel🔗

Given a non-semistable non-zero object X in a thin interval category \mathcal{P}((a,b)) with finitely many subobjects, there exists a proper strict kernel M \subsetneq X whose strict quotient has minimal W-phase among all proper strict kernels, and which is minimal for inclusion among all proper strict kernels realizing that minimum quotient W-phase. Any proper strict kernel strictly smaller than M has strictly larger quotient W-phase.

Proof: Apply exists_minPhase_maximal_strictKernel to get a minimal-phase kernel M_0, then among all proper strict kernels with the same minimal quotient phase take a minimal one M by inclusion. The strict phase increase for sub-kernels of M follows from the minimality of M in the equal-phase class.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_minPhase_minimal_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}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj))
  [Finite (CategoryTheory.Subobject X)] :
  ∃ M,
    M ≠ ⊤ ∧
      CategoryTheory.IsStrictMono M.arrow ∧
        (∀ (B : CategoryTheory.Subobject X),
            B ≠ ⊤ →
              CategoryTheory.IsStrictMono B.arrow →
                ssf.wPhase
                    (CategoryTheory.Limits.cokernel M.arrow).obj ≤
                  ssf.wPhase
                    (CategoryTheory.Limits.cokernel B.arrow).obj) ∧
          ∀ (B : CategoryTheory.Subobject X),
            B ≠ ⊤ →
              CategoryTheory.IsStrictMono B.arrow →
                B < M →
                  ssf.wPhase
                      (CategoryTheory.Limits.cokernel M.arrow).obj <
                    ssf.wPhase
                      (CategoryTheory.Limits.cokernel B.arrow).obj
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_minPhase_minimal_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}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj))
  [Finite (CategoryTheory.Subobject X)] :
  ∃ M,
    M ≠ ⊤ ∧
      CategoryTheory.IsStrictMono
          M.arrow ∧
        (∀
            (B :
              CategoryTheory.Subobject X),
            B ≠ ⊤ →
              CategoryTheory.IsStrictMono
                  B.arrow →
                ssf.wPhase
                    (CategoryTheory.Limits.cokernel
                        M.arrow).obj ≤
                  ssf.wPhase
                    (CategoryTheory.Limits.cokernel
                        B.arrow).obj) ∧
          ∀
            (B :
              CategoryTheory.Subobject X),
            B ≠ ⊤ →
              CategoryTheory.IsStrictMono
                  B.arrow →
                B < M →
                  ssf.wPhase
                      (CategoryTheory.Limits.cokernel
                          M.arrow).obj <
                    ssf.wPhase
                      (CategoryTheory.Limits.cokernel
                          B.arrow).obj

Something wrong, better idea? Suggest a change

14.11.31. exists_maxPhase_maximal_strictSubobject_of_finite🔗

Given a non-zero object X in a thin interval category \mathcal{P}((a,b)) whose set of nonzero strict subobjects is finite, there exists a nonzero strict subobject M \hookrightarrow X whose W-phase is maximal among all nonzero strict subobjects, and which is maximal for inclusion among all strict subobjects realizing that maximal W-phase. Moreover, any strict subobject strictly containing M has strictly smaller W-phase.

Proof: Among the nonempty finite set of nonzero strict subobjects, choose M_0 maximizing W-phase. Among all subobjects realizing phase equal to \phi(M_0), take a maximal one M by inclusion; finiteness ensures such a maximum exists. The strict phase-drop property for M then follows from the maximality of M within the equal-phase class.

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

Something wrong, better idea? Suggest a change

14.11.32. exists_maxPhase_maximal_strictSubobject🔗

For a nonzero object X in a thin interval subcategory \mathcal{P}((a,b)) with finite subobject lattice, there exists a nonzero strict subobject M of X with maximal W-phase among all nonzero strict subobjects, and maximal for inclusion among those with the same W-phase.

Proof: Delegates to exists_maxPhase_maximal_strictSubobject_of_finite using Set.toFinite to convert the Finite (Subobject X) instance to finiteness of the set of nonzero strict subobjects.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_maxPhase_maximal_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)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  [Finite (CategoryTheory.Subobject X)] :
  ∃ M,
    M ≠ ⊥ ∧
      CategoryTheory.IsStrictMono M.arrow ∧
        (∀ (B : CategoryTheory.Subobject X),
            B ≠ ⊥ →
              CategoryTheory.IsStrictMono B.arrow →
                ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj B).obj ≤
                  ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj M).obj) ∧
          ∀ (B : CategoryTheory.Subobject X),
            CategoryTheory.IsStrictMono B.arrow →
              M < B →
                ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj B).obj <
                  ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj M).obj
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_maxPhase_maximal_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)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  [Finite (CategoryTheory.Subobject X)] :
  ∃ M,
    M ≠ ⊥ ∧
      CategoryTheory.IsStrictMono
          M.arrow ∧
        (∀
            (B :
              CategoryTheory.Subobject X),
            B ≠ ⊥ →
              CategoryTheory.IsStrictMono
                  B.arrow →
                ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj
                        B).obj ≤
                  ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj
                        M).obj) ∧
          ∀
            (B :
              CategoryTheory.Subobject X),
            CategoryTheory.IsStrictMono
                B.arrow →
              M < B →
                ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj
                        B).obj <
                  ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj
                        M).obj

Something wrong, better idea? Suggest a change

14.11.33. semistable_of_maxPhase_strictSubobject🔗

The maximal strict subobject from exists_maxPhase_maximal_strictSubobject is W-semistable: any further strict subobject has W-phase at most equal.

Proof: By maximality of the W-phase among strict subobjects, any subobject of the maximal one cannot have strictly larger phase.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_of_maxPhase_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)]
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {M : CategoryTheory.Subobject X} (hM_ne : M ≠ ⊥)
  (hM_strict : CategoryTheory.IsStrictMono M.arrow)
  (hM_max :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊥ →
        CategoryTheory.IsStrictMono B.arrow →
          ssf.wPhase (CategoryTheory.Subobject.underlying.obj B).obj ≤
            ssf.wPhase (CategoryTheory.Subobject.underlying.obj M).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
    (CategoryTheory.Subobject.underlying.obj M).obj
    (ssf.wPhase (CategoryTheory.Subobject.underlying.obj M).obj)
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_of_maxPhase_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)]
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {M : CategoryTheory.Subobject X}
  (hM_ne : M ≠ ⊥)
  (hM_strict :
    CategoryTheory.IsStrictMono M.arrow)
  (hM_max :
    ∀ (B : CategoryTheory.Subobject X),
      B ≠ ⊥ →
        CategoryTheory.IsStrictMono
            B.arrow →
          ssf.wPhase
              (CategoryTheory.Subobject.underlying.obj
                  B).obj ≤
            ssf.wPhase
              (CategoryTheory.Subobject.underlying.obj
                  M).obj)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C ssf
    (CategoryTheory.Subobject.underlying.obj
        M).obj
    (ssf.wPhase
      (CategoryTheory.Subobject.underlying.obj
          M).obj)

Something wrong, better idea? Suggest a change