Bridgeland Stability Conditions

14.12. Deformation: MaximalDestabilizingQuotient🔗

14.12.1. ThinFiniteLengthInInterval🔗

The thin interval category \mathcal{P}((a,b)) has strict finite length when every interval object is both strict-Artinian and strict-Noetherian. This is the finite-length hypothesis used in the MDQ construction.

Construction: Defined as a universal quantification: for every Y in the interval category, Y is strict-Artinian and strict-Noetherian.

🔗def
CategoryTheory.Triangulated.ThinFiniteLengthInInterval.{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 : ℝ) [Fact (a < b)] [Fact (b - a ≤ 1)] : Prop
CategoryTheory.Triangulated.ThinFiniteLengthInInterval.{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 : ℝ) [Fact (a < b)]
  [Fact (b - a ≤ 1)] : Prop

Something wrong, better idea? Suggest a change

14.12.2. of_wide🔗

Derive thin finite length for \mathcal{P}((a,b)) from wide-sector finite length at center t with radius 4\varepsilon_0: if t - 4\varepsilon_0 \le a and b \le t + 4\varepsilon_0, then the interval inclusion monotonicity gives the result.

Proof: The interval (a,b) is contained in (t - 4\varepsilon_0, t + 4\varepsilon_0). Apply interval inclusion and transport the strict finite-length property from the wider interval.

🔗theorem
CategoryTheory.Triangulated.ThinFiniteLengthInInterval.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)
  {ε₀ t a b : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (hε₀ : 0 < ε₀)
  (hε₀8 : ε₀ < 1 / 8) (ha : t - 4 * ε₀ ≤ a) (hb : b ≤ t + 4 * ε₀)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀
      hε₀8) :
  CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b
CategoryTheory.Triangulated.ThinFiniteLengthInInterval.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)
  {ε₀ t a b : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] (hε₀ : 0 < ε₀)
  (hε₀8 : ε₀ < 1 / 8)
  (ha : t - 4 * ε₀ ≤ a)
  (hb : b ≤ t + 4 * ε₀)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ hε₀8) :
  CategoryTheory.Triangulated.ThinFiniteLengthInInterval
    C σ a b

Something wrong, better idea? Suggest a change

14.12.3. of_ambient🔗

Derive thin finite length for a sub-interval from artinian/noetherian data on an ambient interval via inclusion.

Proof: Immediate from interval_thinFiniteLength_of_inclusion applied to the inclusion of interval predicates.

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

Something wrong, better idea? Suggest a change

14.12.4. thinFiniteLength_of_node78_window🔗

The Node 7.8 window \mathcal{P}((t - 3\varepsilon_0, t + 5\varepsilon_0)) has thin finite length, derived from wide-sector finite length centered at t + \varepsilon_0.

Proof: Apply ThinFiniteLengthInInterval.of_wide with center t + \varepsilon_0 and verify the containment bounds.

🔗theorem
CategoryTheory.Triangulated.thinFiniteLength_of_node78_window.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε₀ t : ℝ} [Fact (t - 3 * ε₀ < t + 5 * ε₀)]
  [Fact (t + 5 * ε₀ - (t - 3 * ε₀) ≤ 1)] (hε₀ : 0 < ε₀)
  (hε₀8 : ε₀ < 1 / 8)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀
      hε₀8) :
  CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ
    (t - 3 * ε₀) (t + 5 * ε₀)
CategoryTheory.Triangulated.thinFiniteLength_of_node78_window.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε₀ t : ℝ}
  [Fact (t - 3 * ε₀ < t + 5 * ε₀)]
  [Fact (t + 5 * ε₀ - (t - 3 * ε₀) ≤ 1)]
  (hε₀ : 0 < ε₀) (hε₀8 : ε₀ < 1 / 8)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ hε₀8) :
  CategoryTheory.Triangulated.ThinFiniteLengthInInterval
    C σ (t - 3 * ε₀) (t + 5 * ε₀)

Something wrong, better idea? Suggest a change

14.12.5. exists_semistable_strictQuotient_le_phase_of_finiteLength🔗

Quotient selection for thin interval categories: every nonzero interval object X admits a proper strict kernel M whose cokernel is W-semistable with W-phase at most that of X. This is the strict-kernel analogue of Proposition 2.4's first quotient-selection step.

Proof: Noetherian induction on the strict-subobject poset. At each step, test whether the cokernel of the current kernel is semistable. If yes, stop. If not, find a destabilizing strict subobject of the cokernel, pull it back to get a strictly larger kernel, and note the phase decreases. Terminate by well-foundedness.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_semistable_strictQuotient_le_phase_of_finiteLength.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ∃ M,
    M ≠ ⊤ ∧
      CategoryTheory.IsStrictMono M.arrow ∧
        CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
            ssf (CategoryTheory.Limits.cokernel M.arrow).obj
            (ssf.wPhase (CategoryTheory.Limits.cokernel M.arrow).obj) ∧
          ssf.wPhase (CategoryTheory.Limits.cokernel M.arrow).obj ≤
            ssf.wPhase X.obj
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_semistable_strictQuotient_le_phase_of_finiteLength.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ∃ M,
    M ≠ ⊤ ∧
      CategoryTheory.IsStrictMono
          M.arrow ∧
        CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
            C ssf
            (CategoryTheory.Limits.cokernel
                M.arrow).obj
            (ssf.wPhase
              (CategoryTheory.Limits.cokernel
                  M.arrow).obj) ∧
          ssf.wPhase
              (CategoryTheory.Limits.cokernel
                  M.arrow).obj ≤
            ssf.wPhase X.obj

Something wrong, better idea? Suggest a change

14.12.6. IsStrictMDQ🔗

A strict maximally destabilizing quotient in a thin interval category: a morphism q : X \twoheadrightarrow B such that q is strict epi, B is nonzero and W-semistable, and q has minimal W-phase among all W-semistable strict quotients (with equality forcing factorization). This is the quasi-abelian analogue of StabilityFunction.IsMDQ.

Construction: A structure with four fields: strictEpi (the quotient map is a strict epimorphism), nonzero (B is nonzero), semistable (B is \operatorname{ssf}-semistable at its W-phase), and minimal (for any other semistable strict quotient B', \psi(B) \le \psi(B') with equality giving a factorization q' = q \circ t).

🔗structure
CategoryTheory.Triangulated.IsStrictMDQ.{v, u, u'} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b)
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (q : X ⟶ B) : Prop
CategoryTheory.Triangulated.IsStrictMDQ.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b)
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (q : X ⟶ B) : Prop

Constructor

CategoryTheory.Triangulated.IsStrictMDQ.mk.{v, u, u'}

Fields

strictEpi : CategoryTheory.IsStrictEpi q
nonzero : ¬CategoryTheory.Limits.IsZero B.obj
semistable : CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf B.obj (ssf.wPhase B.obj)
minimal : ∀ {B' : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b} (q' : X ⟶ B'),
  CategoryTheory.IsStrictEpi q' →
    ¬CategoryTheory.Limits.IsZero B'.obj →
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf B'.obj (ssf.wPhase B'.obj) →
        ssf.wPhase B.obj ≤ ssf.wPhase B'.obj ∧
          (ssf.wPhase B'.obj = ssf.wPhase B.obj → ∃ t, q' = CategoryTheory.CategoryStruct.comp q t)

Something wrong, better idea? Suggest a change

14.12.7. id_of_semistable🔗

A semistable interval object is its own strict MDQ: \operatorname{id}_X : X \to X is a strict MDQ when X is W-semistable.

Proof: The identity is trivially strict epi, X is nonzero and semistable by hypothesis, and minimality follows from phase_le_of_strictQuotient_of_window with factorization via q' = \operatorname{id} \circ q'.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.id_of_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)]
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      X.obj (ssf.wPhase X.obj)) :
  CategoryTheory.Triangulated.IsStrictMDQ C σ ssf
    (CategoryTheory.CategoryStruct.id X)
CategoryTheory.Triangulated.IsStrictMDQ.id_of_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)]
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf X.obj (ssf.wPhase X.obj)) :
  CategoryTheory.Triangulated.IsStrictMDQ
    C σ ssf
    (CategoryTheory.CategoryStruct.id X)

Something wrong, better idea? Suggest a change

14.12.8. precomposeIso🔗

Precomposing a strict MDQ with an isomorphism of sources preserves the strict MDQ property: if q : X \to B is a strict MDQ and e : X' \cong X, then e \circ q : X' \to B is a strict MDQ.

Proof: Strict epi is preserved by precomposing with an isomorphism. Minimality: given a competitor q' : X' \to B', compose with e^{-1} to get a competitor for q, apply the original minimality, then re-compose.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.precomposeIso.{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 X' B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  (e : X' ≅ X) :
  CategoryTheory.Triangulated.IsStrictMDQ C σ ssf
    (CategoryTheory.CategoryStruct.comp e.hom q)
CategoryTheory.Triangulated.IsStrictMDQ.precomposeIso.{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 X' B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  (e : X' ≅ X) :
  CategoryTheory.Triangulated.IsStrictMDQ
    C σ ssf
    (CategoryTheory.CategoryStruct.comp
      e.hom q)

Something wrong, better idea? Suggest a change

14.12.9. interval_strictEpi_of_strictEpi_comp🔗

If p \circ q is a strict epimorphism in a thin interval category, then q is a strict epimorphism.

Proof: Map to the left heart. The image of p \circ q is epi, so the image of q is epi. Transport back.

🔗theorem
CategoryTheory.Triangulated.interval_strictEpi_of_strictEpi_comp.{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 : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X Q B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (p : X ⟶ Q) (q : Q ⟶ B)
  (hpq :
    CategoryTheory.IsStrictEpi
      (CategoryTheory.CategoryStruct.comp p q)) :
  CategoryTheory.IsStrictEpi q
CategoryTheory.Triangulated.interval_strictEpi_of_strictEpi_comp.{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 : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)]
  {X Q B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (p : X ⟶ Q) (q : Q ⟶ B)
  (hpq :
    CategoryTheory.IsStrictEpi
      (CategoryTheory.CategoryStruct.comp
        p q)) :
  CategoryTheory.IsStrictEpi q

Something wrong, better idea? Suggest a change

14.12.10. of_strictEpi_factor🔗

If a strict MDQ q : X \twoheadrightarrow B factors as q = p \circ \pi_Q through a strict epi p : X \twoheadrightarrow Q, then \pi_Q : Q \to B is also a strict MDQ.

Proof: Strict epi property of \pi_Q follows from interval_strictEpi_of_strictEpi_comp. Minimality: for any competitor q' : Q \to B', the composite p \circ q' is a competitor for q, so the original minimality applies.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.of_strictEpi_factor.{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 Q B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  {p : X ⟶ Q} (hp : CategoryTheory.IsStrictEpi p) {πQ : Q ⟶ B}
  (hfac : CategoryTheory.CategoryStruct.comp p πQ = q) :
  CategoryTheory.Triangulated.IsStrictMDQ C σ ssf πQ
CategoryTheory.Triangulated.IsStrictMDQ.of_strictEpi_factor.{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 Q B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  {p : X ⟶ Q}
  (hp : CategoryTheory.IsStrictEpi p)
  {πQ : Q ⟶ B}
  (hfac :
    CategoryTheory.CategoryStruct.comp p
        πQ =
      q) :
  CategoryTheory.Triangulated.IsStrictMDQ
    C σ ssf πQ

Something wrong, better idea? Suggest a change

14.12.11. phase_le_of_strictQuotient🔗

The phase of a strict MDQ is bounded above by the phase of any nonzero strict quotient of its source: if q : X \twoheadrightarrow B is a strict MDQ and p : X \twoheadrightarrow Q is any strict epi with Q \ne 0, then \psi(B) \le \psi(Q).

Proof: Find a semistable strict quotient of Q with phase \le \psi(Q) (by exists_semistable_strictQuotient_le_phase_of_finiteLength), compose to get a semistable strict quotient of X, then apply the MDQ minimality.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.phase_le_of_strictQuotient.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  (p : X ⟶ Q) (hp : CategoryTheory.IsStrictEpi p)
  (hQ : ¬CategoryTheory.Limits.IsZero Q.obj) :
  ssf.wPhase B.obj ≤ ssf.wPhase Q.obj
CategoryTheory.Triangulated.IsStrictMDQ.phase_le_of_strictQuotient.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  (p : X ⟶ Q)
  (hp : CategoryTheory.IsStrictEpi p)
  (hQ :
    ¬CategoryTheory.Limits.IsZero Q.obj) :
  ssf.wPhase B.obj ≤ ssf.wPhase Q.obj

Something wrong, better idea? Suggest a change

14.12.12. isSemistable_of_strictQuotient_phase_eq🔗

If a nonzero strict quotient of the source has the same phase as a strict MDQ, then it is already semistable. Otherwise a destabilizing strict subobject would produce a smaller-phase strict quotient, contradicting MDQ minimality.

Proof: By contradiction: if the quotient is not semistable, the first strict SES (strict-Artinian descent) produces a proper subobject of larger phase. The composition through the cokernel gives a strict quotient of X with phase < \psi(B), which is then below the MDQ quotient with phase equal to \psi(B), contradicting minimality.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.isSemistable_of_strictQuotient_phase_eq.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  (p : X ⟶ Q) (hp : CategoryTheory.IsStrictEpi p)
  (hQ : ¬CategoryTheory.Limits.IsZero Q.obj)
  (hEq : ssf.wPhase Q.obj = ssf.wPhase B.obj) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
    Q.obj (ssf.wPhase Q.obj)
CategoryTheory.Triangulated.IsStrictMDQ.isSemistable_of_strictQuotient_phase_eq.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  (p : X ⟶ Q)
  (hp : CategoryTheory.IsStrictEpi p)
  (hQ :
    ¬CategoryTheory.Limits.IsZero Q.obj)
  (hEq :
    ssf.wPhase Q.obj = ssf.wPhase B.obj) :
  CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
    C ssf Q.obj (ssf.wPhase Q.obj)

Something wrong, better idea? Suggest a change

14.12.13. factor_of_phase_eq_of_strictQuotient🔗

If a nonzero strict quotient Q of the MDQ source has the same W-phase as the MDQ target B, then the MDQ factors through Q: there exists t : B \to Q with q' = q \circ t.

Proof: By isSemistable_of_strictQuotient_phase_eq, Q is semistable at the common phase. The MDQ minimality then yields the factorization.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.factor_of_phase_eq_of_strictQuotient.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  (p : X ⟶ Q) (hp : CategoryTheory.IsStrictEpi p)
  (hQ : ¬CategoryTheory.Limits.IsZero Q.obj)
  (hEq : ssf.wPhase Q.obj = ssf.wPhase B.obj) :
  ∃ t, p = CategoryTheory.CategoryStruct.comp q t
CategoryTheory.Triangulated.IsStrictMDQ.factor_of_phase_eq_of_strictQuotient.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B Q :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  (p : X ⟶ Q)
  (hp : CategoryTheory.IsStrictEpi p)
  (hQ :
    ¬CategoryTheory.Limits.IsZero Q.obj)
  (hEq :
    ssf.wPhase Q.obj = ssf.wPhase B.obj) :
  ∃ t,
    p =
      CategoryTheory.CategoryStruct.comp q
        t

Something wrong, better idea? Suggest a change

14.12.14. comp_of_destabilizing_semistable_subobject🔗

If A \hookrightarrow X is a destabilizing W-semistable strict subobject with \psi(A) > \psi(X) and A \ne \top, and q : \operatorname{coker}(A) \to B is a strict MDQ on the cokernel, then \operatorname{coker\_proj}(A) \circ q : X \to B is a strict MDQ on X.

Proof: Strict epi follows from composition. Minimality: for a competitor q' : X \to B' with \psi(B') \le \psi(B), the Hom vanishing \operatorname{Hom}(A, B') = 0 (from the phase gap) implies q' factors through \operatorname{coker}(A), reducing to the MDQ minimality on the cokernel.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.comp_of_destabilizing_semistable_subobject.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) {U_hom : ℝ}
  (hHom :
    ∀
      {E F :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a
          b},
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
          ssf E.obj (ssf.wPhase E.obj) →
        CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
            ssf F.obj (ssf.wPhase F.obj) →
          ssf.wPhase F.obj < ssf.wPhase E.obj →
            ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {A : CategoryTheory.Subobject X}
  (hA_ss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      (CategoryTheory.Subobject.underlying.obj A).obj
      (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj))
  (hA_strict : CategoryTheory.IsStrictMono A.arrow)
  (hA_phase :
    ssf.wPhase X.obj <
      ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj)
  (hA_top : A ≠ ⊤)
  (hA_phase_upper :
    ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < U_hom)
  {B : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : CategoryTheory.Limits.cokernel A.arrow ⟶ B}
  (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q) :
  CategoryTheory.Triangulated.IsStrictMDQ C σ ssf
    (CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π A.arrow) q)
CategoryTheory.Triangulated.IsStrictMDQ.comp_of_destabilizing_semistable_subobject.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) {U_hom : ℝ}
  (hHom :
    ∀
      {E F :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b},
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
          C ssf E.obj (ssf.wPhase E.obj) →
        CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
            C ssf F.obj
            (ssf.wPhase F.obj) →
          ssf.wPhase F.obj <
              ssf.wPhase E.obj →
            ssf.wPhase E.obj < U_hom →
              ∀ (f : E ⟶ F), f = 0)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {A : CategoryTheory.Subobject X}
  (hA_ss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf
      (CategoryTheory.Subobject.underlying.obj
          A).obj
      (ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj))
  (hA_strict :
    CategoryTheory.IsStrictMono A.arrow)
  (hA_phase :
    ssf.wPhase X.obj <
      ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj)
  (hA_top : A ≠ ⊤)
  (hA_phase_upper :
    ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj <
      U_hom)
  {B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q :
    CategoryTheory.Limits.cokernel
        A.arrow ⟶
      B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q) :
  CategoryTheory.Triangulated.IsStrictMDQ
    C σ ssf
    (CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
        A.arrow)
      q)

Something wrong, better idea? Suggest a change

14.12.15. exists_strictMDQ_of_finiteLength🔗

MDQ existence in thin finite-length interval categories: every nonzero interval object admits a strict MDQ. This is the foundational MDQ existence theorem using the strict-Noetherian descent.

Proof: Noetherian induction. If the cokernel of the current kernel is semistable, its identity is an MDQ. Otherwise, find a destabilizing strict subobject, pull back to get a larger kernel, recurse on the cokernel, then compose via comp_of_destabilizing_semistable_subobject.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_strictMDQ_of_finiteLength.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) {U_hom : ℝ}
  (hHom :
    ∀
      {E F :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a
          b},
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
          ssf E.obj (ssf.wPhase E.obj) →
        CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
            ssf F.obj (ssf.wPhase F.obj) →
          ssf.wPhase F.obj < ssf.wPhase E.obj →
            ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0)
  (hDestabBound :
    ∀
      {Y :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a
          b},
      ¬CategoryTheory.Limits.IsZero Y →
        ∀ {A : CategoryTheory.Subobject Y},
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf (CategoryTheory.Subobject.underlying.obj A).obj
              (ssf.wPhase
                (CategoryTheory.Subobject.underlying.obj A).obj) →
            CategoryTheory.IsStrictMono A.arrow →
              ssf.wPhase Y.obj <
                  ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj A).obj →
                ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj A).obj <
                  U_hom)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ∃ B q, CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_strictMDQ_of_finiteLength.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) {U_hom : ℝ}
  (hHom :
    ∀
      {E F :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b},
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
          C ssf E.obj (ssf.wPhase E.obj) →
        CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
            C ssf F.obj
            (ssf.wPhase F.obj) →
          ssf.wPhase F.obj <
              ssf.wPhase E.obj →
            ssf.wPhase E.obj < U_hom →
              ∀ (f : E ⟶ F), f = 0)
  (hDestabBound :
    ∀
      {Y :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b},
      ¬CategoryTheory.Limits.IsZero Y →
        ∀
          {A :
            CategoryTheory.Subobject Y},
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf
              (CategoryTheory.Subobject.underlying.obj
                  A).obj
              (ssf.wPhase
                (CategoryTheory.Subobject.underlying.obj
                    A).obj) →
            CategoryTheory.IsStrictMono
                A.arrow →
              ssf.wPhase Y.obj <
                  ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj
                        A).obj →
                ssf.wPhase
                    (CategoryTheory.Subobject.underlying.obj
                        A).obj <
                  U_hom)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X) :
  ∃ B q,
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q

Something wrong, better idea? Suggest a change

14.12.16. interval_kernelSubobject_isLimitKernelFork🔗

For a morphism q : X \to Y in a thin interval category \mathcal{P}((a,b)) with b - a \leq 1, the canonical fork \ker(q) \hookrightarrow X \xrightarrow{q} Y with the kernel subobject arrow is a limit kernel fork.

Proof: Any morphism g : W \to X with g \circ q = 0 factors through \ker(q) via kernel.lift; composing with the isomorphism kernelSubobjectIso gives the unique factorization through the kernel subobject arrow.

🔗def
CategoryTheory.Triangulated.interval_kernelSubobject_isLimitKernelFork.{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}
  (q : X ⟶ Y) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.KernelFork.ofι
      (CategoryTheory.Limits.kernelSubobject q).arrow ⋯)
CategoryTheory.Triangulated.interval_kernelSubobject_isLimitKernelFork.{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}
  (q : X ⟶ Y) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.KernelFork.ofι
      (CategoryTheory.Limits.kernelSubobject
          q).arrow
      ⋯)

Something wrong, better idea? Suggest a change

14.12.17. interval_strictShortExact_of_kernelSubobject_strictEpi🔗

If q : X \twoheadrightarrow Y is a strict epimorphism in a thin interval category \mathcal{P}((a,b)) with b - a \leq 1, then the sequence \ker(q) \hookrightarrow X \twoheadrightarrow Y with the kernel subobject inclusion is a strict short exact sequence.

Proof: The kernel subobject arrow forms a limit kernel fork by interval_kernelSubobject_isLimitKernelFork; with the strict epi hypothesis on q, interval_strictShortExact_of_kernel_strictEpi then yields strict short exactness.

🔗theorem
CategoryTheory.Triangulated.interval_strictShortExact_of_kernelSubobject_strictEpi.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [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}
  (q : X ⟶ Y) (hq : CategoryTheory.IsStrictEpi q) :
  CategoryTheory.StrictShortExact
    {
      X₁ :=
        CategoryTheory.Subobject.underlying.obj
          (CategoryTheory.Limits.kernelSubobject q),
      X₂ := X, X₃ := Y,
      f := (CategoryTheory.Limits.kernelSubobject q).arrow, g := q,
      zero := ⋯ }
CategoryTheory.Triangulated.interval_strictShortExact_of_kernelSubobject_strictEpi.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [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}
  (q : X ⟶ Y)
  (hq : CategoryTheory.IsStrictEpi q) :
  CategoryTheory.StrictShortExact
    {
      X₁ :=
        CategoryTheory.Subobject.underlying.obj
          (CategoryTheory.Limits.kernelSubobject
            q),
      X₂ := X, X₃ := Y,
      f :=
        (CategoryTheory.Limits.kernelSubobject
            q).arrow,
      g := q, zero := ⋯ }

Something wrong, better idea? Suggest a change

14.12.18. map_eq_mk🔗

For a subobject K \leq E and a subobject S \leq K, the pushforward (\mathrm{map}(K.\mathrm{arrow}))(S) equals \mathrm{mk}(S.\mathrm{arrow} \circ K.\mathrm{arrow}) as a subobject of E.

Proof: Rewrite S as \mathrm{mk}(S.\mathrm{arrow}) and apply the functoriality formula Subobject.map_mk.

🔗theorem
CategoryTheory.Triangulated.Subobject.map_eq_mk.{u_1, u_2}
  {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {E : D}
  (K : CategoryTheory.Subobject E)
  (S :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj K)) :
  (CategoryTheory.Subobject.map K.arrow).obj S =
    CategoryTheory.Subobject.mk
      (CategoryTheory.CategoryStruct.comp S.arrow K.arrow)
CategoryTheory.Triangulated.Subobject.map_eq_mk.{u_1,
    u_2}
  {D : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} D]
  {E : D} (K : CategoryTheory.Subobject E)
  (S :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        K)) :
  (CategoryTheory.Subobject.map
          K.arrow).obj
      S =
    CategoryTheory.Subobject.mk
      (CategoryTheory.CategoryStruct.comp
        S.arrow K.arrow)

Something wrong, better idea? Suggest a change

14.12.19. mapSubIso🔗

For an object E, a subobject K \leq E, and a subobject S \leq K, there is a canonical isomorphism (\mathrm{map}(K.\mathrm{arrow})(S) : D) \cong (S : D) between the image of S under the pushforward along K.\mathrm{arrow} and S itself as objects of D.

Construction: Constructed as Subobject.isoOfEqMk applied to the equality Subobject.map_eq_mk K S, which identifies (Subobject.map K.arrow).obj S with Subobject.mk (S.arrow ≫ K.arrow), followed by the underlying isomorphism.

🔗def
CategoryTheory.Triangulated.Subobject.mapSubIso.{u_1, u_2}
  {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {E : D}
  (K : CategoryTheory.Subobject E)
  (S :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj K)) :
  CategoryTheory.Subobject.underlying.obj
      ((CategoryTheory.Subobject.map K.arrow).obj S) ≅
    CategoryTheory.Subobject.underlying.obj S
CategoryTheory.Triangulated.Subobject.mapSubIso.{u_1,
    u_2}
  {D : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} D]
  {E : D} (K : CategoryTheory.Subobject E)
  (S :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        K)) :
  CategoryTheory.Subobject.underlying.obj
      ((CategoryTheory.Subobject.map
            K.arrow).obj
        S) ≅
    CategoryTheory.Subobject.underlying.obj
      S

Something wrong, better idea? Suggest a change

14.12.20. interval_kernelSubobject_ne_top_of_strictEpi_nonzero🔗

The kernel subobject of a strict epi with nonzero target is not \top. If it were, the strict epi would factor through zero, contradicting the nonzero target.

Proof: If \ker(q) = \top then q factors through the zero object, but q is epi with nonzero target, contradiction.

🔗theorem
CategoryTheory.Triangulated.interval_kernelSubobject_ne_top_of_strictEpi_nonzero.{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}
  {q : X ⟶ Y} (hq : CategoryTheory.IsStrictEpi q)
  (hY : ¬CategoryTheory.Limits.IsZero Y.obj) :
  CategoryTheory.Limits.kernelSubobject q ≠ ⊤
CategoryTheory.Triangulated.interval_kernelSubobject_ne_top_of_strictEpi_nonzero.{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}
  {q : X ⟶ Y}
  (hq : CategoryTheory.IsStrictEpi q)
  (hY :
    ¬CategoryTheory.Limits.IsZero Y.obj) :
  CategoryTheory.Limits.kernelSubobject
      q ≠
    ⊤

Something wrong, better idea? Suggest a change

14.12.21. wPhaseOf_gt_of_strictQuotient_of_inner_strip🔗

For an object X in the inner strip \mathcal{P}((a + 2\varepsilon, b - 4\varepsilon)) of a thin interval \mathcal{P}((a,b)), every nonzero strict quotient has W-phase strictly greater than a + \varepsilon.

Proof: The inner strip containment gives tight phase bounds. The W-phase of any interval object is > a - \varepsilon by perturbation bounds, and a + \varepsilon is obtained by monotonicity from the tighter inner strip.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_gt_of_strictQuotient_of_inner_strip.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} [Fact (a < b)] [Fact (b - a ≤ 1)] (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {X B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX_inner :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (a + 2 * ε₀) (b - 4 * ε₀) X.obj)
  (q : X ⟶ B) (hq : CategoryTheory.IsStrictEpi q)
  (hBne : ¬CategoryTheory.Limits.IsZero B.obj) :
  a + ε₀ <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v B.obj)) ((a + b) / 2)
CategoryTheory.Triangulated.wPhaseOf_gt_of_strictQuotient_of_inner_strip.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ε₀ : ℝ} [Fact (a < b)]
  [Fact (b - a ≤ 1)] (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {X B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX_inner :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (a + 2 * ε₀)
      (b - 4 * ε₀) X.obj)
  (q : X ⟶ B)
  (hq : CategoryTheory.IsStrictEpi q)
  (hBne :
    ¬CategoryTheory.Limits.IsZero B.obj) :
  a + ε₀ <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v B.obj))
      ((a + b) / 2)

Something wrong, better idea? Suggest a change

14.12.22. kernelSubobject_ne_bot_of_not_semistable🔗

If X is not W-semistable and q : X \to B is a strict MDQ, then \ker(q) \ne \bot. If it were, q would be an isomorphism, forcing X \cong B to be semistable.

Proof: If \ker(q) = \bot then q is mono and epi, hence iso. But B is semistable, contradicting X not being semistable.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.kernelSubobject_ne_bot_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 B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
        ssf X.obj (ssf.wPhase X.obj)) :
  CategoryTheory.Limits.kernelSubobject q ≠ ⊥
CategoryTheory.Triangulated.IsStrictMDQ.kernelSubobject_ne_bot_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 B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  (hns :
    ¬CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
        C ssf X.obj (ssf.wPhase X.obj)) :
  CategoryTheory.Limits.kernelSubobject
      q ≠
    ⊥

Something wrong, better idea? Suggest a change

14.12.23. phase_lt_of_strictQuotient_of_kernel🔗

For a strict MDQ q : X \twoheadrightarrow B, every proper strict quotient of \ker(q) has W-phase strictly greater than \psi(B).

Proof: A strict quotient of \ker(q) gives a strictly larger kernel subobject of X. The cokernel of this larger kernel has phase < \psi(\operatorname{coker}(\ker(q))) = \psi(B) by the seesaw, but \psi(B) \le that phase by MDQ minimality. The resolution gives the strict inequality.

🔗theorem
CategoryTheory.Triangulated.IsStrictMDQ.phase_lt_of_strictQuotient_of_kernel.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : X ⟶ B} (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        (CategoryTheory.Limits.kernelSubobject q))}
  (hA_top : A ≠ ⊤) (hA_strict : CategoryTheory.IsStrictMono A.arrow) :
  ssf.wPhase B.obj <
    ssf.wPhase (CategoryTheory.Limits.cokernel A.arrow).obj
CategoryTheory.Triangulated.IsStrictMDQ.phase_lt_of_strictQuotient_of_kernel.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1)
  {X B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : X ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  {A :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        (CategoryTheory.Limits.kernelSubobject
          q))}
  (hA_top : A ≠ ⊤)
  (hA_strict :
    CategoryTheory.IsStrictMono A.arrow) :
  ssf.wPhase B.obj <
    ssf.wPhase
      (CategoryTheory.Limits.cokernel
          A.arrow).obj

Something wrong, better idea? Suggest a change