Slicing.Defs — BridgelandStability Comparator Manual

8. Slicing.Defs🔗

Module BridgelandStability.Slicing.Defs — 7 declarations (Structure, Definition, Theorem)

8.1. `CategoryTheory.Triangulated.HNFiltration`🔗

Structure | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- A Harder-Narasimhan (HN) filtration of an object `E` with respect to a phase
predicate `P`. This extends a `PostnikovTower` with phase data: each factor is
semistable with a given phase, and the phases are strictly decreasing. -/
@[informal "Definition 3.3" "axiom (c): HN decomposition data for triangulated categories"]
structure HNFiltration (P : ℝ → ObjectProperty C) (E : C) extends PostnikovTower C E where
  /-- The phases of the semistable factors, in strictly decreasing order. -/
  φ : Fin n → ℝ
  /-- The phases are strictly decreasing (higher phase factors appear first). -/
  hφ : StrictAnti φ
  /-- Each factor is semistable of the given phase. -/
  semistable : ∀ j, (P (φ j)) (toPostnikovTower.factor j)

8.2. `CategoryTheory.Triangulated.Slicing`🔗

Structure | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- A slicing of a pretriangulated category `C`, as defined in
Bridgeland (2007), Definition 5.1. A slicing assigns to each real number `φ`
a full subcategory of semistable objects `P(φ)` (as an `ObjectProperty`),
subject to shift, Hom-vanishing, and Harder-Narasimhan existence axioms.

Each `P(φ)` is an `ObjectProperty C`, enabling use of the `ObjectProperty` API
(e.g. `FullSubcategory`, shift stability, closure properties). -/
@[informal "Definition 3.3"]
structure Slicing where
  /-- For each phase `φ ∈ ℝ`, the property of semistable objects of phase `φ`. -/
  P : ℝ → ObjectProperty C
  /-- Each phase slice is closed under isomorphisms. -/
  closedUnderIso : ∀ (φ : ℝ), (P φ).IsClosedUnderIsomorphisms
  /-- The zero object satisfies every phase predicate. -/
  zero_mem : ∀ (φ : ℝ), (P φ) (0 : C)
  /-- Shifting by `[1]` increases the phase by 1, and conversely. -/
  shift_iff : ∀ (φ : ℝ) (X : C), (P φ) X ↔ (P (φ + 1)) (X⟦(1 : ℤ)⟧)
  /-- Morphisms from higher-phase to lower-phase nonzero semistable objects vanish. -/
  hom_vanishing : ∀ (φ₁ φ₂ : ℝ) (A B : C),
    φ₂ < φ₁ → (P φ₁) A → (P φ₂) B → ∀ (f : A ⟶ B), f = 0
  /-- Every object has a Harder-Narasimhan filtration. -/
  hn_exists : ∀ (E : C), Nonempty (HNFiltration C P E)

8.3. `CategoryTheory.Triangulated.Slicing.intervalProp`🔗

Definition | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- The interval subcategory predicate `P((a,b))`: an object `E` belongs to the
interval subcategory if it is zero or all phases in its HN filtration lie in `(a,b)`. -/
def Slicing.intervalProp (s : Slicing C) (a b : ℝ) : ObjectProperty C :=
  fun E ↦ IsZero E ∨ ∃ (F : HNFiltration C s.P E), ∀ i, a < F.φ i ∧ F.φ i < b

8.4. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first`🔗

Theorem | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- For any nonzero object, there exists an HN filtration with nonzero first factor.
Proved by repeatedly dropping zero first factors; terminates since `n` decreases
and some factor must be nonzero (by `exists_nonzero_factor`). -/
lemma HNFiltration.exists_nonzero_first (s : Slicing C) {E : C} (hE : ¬IsZero E) :
    ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃

Show proof

:= byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
  obtain ⟨F⟩ := s.hn_exists EC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
  suffices hmain : ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m →
      ∃ (H : HNFiltration C s.P E) (hn : 0 < H.n),
        ¬IsZero (H.triangle ⟨0, hn⟩).obj₃ from
    hmain F.n F le_rflC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
  intro mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕ⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
  induction m with
  | zero =>zeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ 0 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    intro G hGnzeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
    exact absurd (G.zero_isZero (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ G.n = 0 liaAll goals completed! 🐙)) hE
  | succ m ih =>succC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m + 1 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    intro G hGnsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
    have hGn0 : 0 < G.n := G.n_pos C hEsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.n⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    by_cases hfirst : IsZero (G.triangle ⟨0, hGn0⟩).obj₃posC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃negC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:¬IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    ·posC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃ -- First factor is zero; drop it and recurse
      have hn1 : 1 < G.n := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
        by_contra hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:¬1 < G.n⊢ False; push Not at hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1⊢ False
        have : ∀ (i : Fin G.n), IsZero (G.triangle i).obj₃ := fun i ↦ byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ IsZero (G.triangle i).obj₃
          have : i = ⟨0, hGn0⟩ := Fin.ext (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ ↑i = ↑⟨0, hGn0⟩ liaAll goals completed! 🐙)
          subst thisC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1⊢ IsZero (G.triangle ⟨0, hGn0⟩).obj₃; exact hfirstAll goals completed! 🐙
        exact absurd ((G.exists_nonzero_factor C hE).elim fun i hi ↦ absurd (this i) hi) idAll goals completed! 🐙
      have hdrop : (G.dropFirst C hn1 hfirst).n ≤ m := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
        change G.n - 1 ≤ mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃hn1:1 < G.n⊢ G.n - 1 ≤ m; liaAll goals completed! 🐙
      exact ih (G.dropFirst C hn1 hfirst) hdropAll goals completed! 🐙
    ·negC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:¬IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃ exact ⟨G, hGn0, hfirst⟩All goals completed! 🐙

8.5. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last`🔗

Theorem | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- For any nonzero object, there exists an HN filtration with nonzero last factor.
Proved by repeatedly dropping zero last factors. -/
lemma HNFiltration.exists_nonzero_last (s : Slicing C) {E : C} (hE : ¬IsZero E) :
    ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n),
      ¬IsZero (F.triangle ⟨F.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Ehn:0 < F.n⊢ F.n - 1 < F.n liaAll goals completed! 🐙⟩).obj₃

Show proof

:= byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
  obtain ⟨F⟩ := s.hn_exists EC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
  suffices hmain : ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m →
      ∃ (H : HNFiltration C s.P E) (hn : 0 < H.n),
        ¬IsZero (H.triangle ⟨H.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕG:HNFiltration C s.P EH:HNFiltration C s.P Ehn:0 < H.n⊢ H.n - 1 < H.n liaAll goals completed! 🐙⟩).obj₃ from
    hmain F.n F le_rfl
  intro mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕ⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
  induction m with
  | zero =>zeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ 0 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
    intro G hGnzeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
    exact absurd (G.zero_isZero (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ G.n = 0 liaAll goals completed! 🐙)) hE
  | succ m ih =>succC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m + 1 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
    intro G hGnsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
    have hGn0 : 0 < G.n := G.n_pos C hEsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.n⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
    by_cases hlast : IsZero (G.triangle ⟨G.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.n⊢ G.n - 1 < G.n liaAll goals completed! 🐙⟩).obj₃
    ·posC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃ have hn1 : 1 < G.n := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
        by_contra hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:¬1 < G.n⊢ False; push Not at hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1⊢ False
        have : ∀ (i : Fin G.n), IsZero (G.triangle i).obj₃ := fun i ↦ byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ IsZero (G.triangle i).obj₃
          have : i = ⟨G.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ G.n - 1 < G.n liaAll goals completed! 🐙⟩ := Fin.ext (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ ↑i = ↑⟨G.n - 1, ⋯⟩ liaAll goals completed! 🐙)
          subst thisC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1⊢ IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃; exact hlastAll goals completed! 🐙
        exact absurd ((G.exists_nonzero_factor C hE).elim fun i hi ↦ absurd (this i) hi) idAll goals completed! 🐙
      have hdrop : (G.dropLast C hn1 hlast).n ≤ m := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
        change G.n - 1 ≤ mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃hn1:1 < G.n⊢ G.n - 1 ≤ m; liaAll goals completed! 🐙
      exact ih (G.dropLast C hn1 hlast) hdropAll goals completed! 🐙
    ·negC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:¬IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃ exact ⟨G, hGn0, hlast⟩All goals completed! 🐙

8.6. `CategoryTheory.Triangulated.Slicing.phiPlus`🔗

Definition | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- The intrinsic highest phase of a nonzero object with respect to a slicing.
This is the phase of the first factor in any HN filtration with nonzero first factor.
Well-defined by `phiPlus_eq_of_nonzero_factors`. -/
noncomputable def Slicing.phiPlus (s : Slicing C) (E : C) (hE : ¬IsZero E) : ℝ :=
  let F := (HNFiltration.exists_nonzero_first C s hE).choose
  let hn := (HNFiltration.exists_nonzero_first C s hE).choose_spec.choose
  F.φ ⟨0, hn⟩

8.7. `CategoryTheory.Triangulated.Slicing.phiMinus`🔗

Definition | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- The intrinsic lowest phase of a nonzero object with respect to a slicing.
This is the phase of the last factor in any HN filtration with nonzero last factor.
Well-defined by `phiMinus_eq_of_nonzero_last_factors`. -/
noncomputable def Slicing.phiMinus (s : Slicing C) (E : C) (hE : ¬IsZero E) : ℝ :=
  let F := (HNFiltration.exists_nonzero_last C s hE).choose
  let hn : 0 < F.n := (HNFiltration.exists_nonzero_last C s hE).choose_spec.choose
  F.φ ⟨F.n - 1, Nat.sub_one_lt_of_le hn le_rfl⟩

8. Slicing.Defs🔗

8.1. CategoryTheory.Triangulated.HNFiltration🔗

8.2. CategoryTheory.Triangulated.Slicing🔗

8.3. CategoryTheory.Triangulated.Slicing.intervalProp🔗

8.4. CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first🔗

8.5. CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last🔗

8.6. CategoryTheory.Triangulated.Slicing.phiPlus🔗

8.7. CategoryTheory.Triangulated.Slicing.phiMinus🔗

8.1. `CategoryTheory.Triangulated.HNFiltration`🔗

8.2. `CategoryTheory.Triangulated.Slicing`🔗

8.3. `CategoryTheory.Triangulated.Slicing.intervalProp`🔗

8.4. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first`🔗

8.5. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last`🔗

8.6. `CategoryTheory.Triangulated.Slicing.phiPlus`🔗

8.7. `CategoryTheory.Triangulated.Slicing.phiMinus`🔗