12. IntervalCategory.FiniteLength
Module BridgelandStability.IntervalCategory.FiniteLength — 1 declarations (Structure)
12.1. CategoryTheory.Triangulated.Slicing.IsLocallyFinite
Structure | BridgelandStability.IntervalCategory.FiniteLength | Source | Open Issue
/-- A slicing is locally finite if there exists `η > 0` with `η < 1/2` such that every
object in each thin interval category `P((t-η, t+η))` has finite length in the
quasi-abelian sense, i.e. ACC/DCC on strict subobjects.
The extra bound `η < 1/2` is a harmless normalization: any Bridgeland witness may be
shrunk to such an `η`, and then the width `2η` is at most `1`, so the thin interval
category carries the exact / quasi-abelian structure proved above. -/
@[informal "Definition 5.7" "per-object strict finite length is weaker than finite length of all chains (paper's assumption)"]
structure Slicing.IsLocallyFinite (s : Slicing C) : Prop where
intervalFinite : ∃ η : ℝ, ∃ hη : 0 < η, ∃ hη' : η < 1 / 2, ∀ t : ℝ,
let a := t - η
let b := t + η
letI : Fact (a < b) := ⟨C:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Ca✝:ℝb✝:ℝinst✝¹:Fact (a✝ < b✝)inst✝:Fact (b✝ - a✝ ≤ 1)s:Slicing Cη:ℝhη:0 < ηhη':η < 1 / 2t:ℝa:ℝ := t - ηb:ℝ := t + η⊢ a < b
C:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Ca✝:ℝb✝:ℝinst✝¹:Fact (a✝ < b✝)inst✝:Fact (b✝ - a✝ ≤ 1)s:Slicing Cη:ℝhη:0 < ηhη':η < 1 / 2t:ℝa:ℝ := t - ηb:ℝ := t + η⊢ t - η < t + η
All goals completed! 🐙⟩
letI : Fact (b - a ≤ 1) := ⟨C:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Ca✝:ℝb✝:ℝinst✝¹:Fact (a✝ < b✝)inst✝:Fact (b✝ - a✝ ≤ 1)s:Slicing Cη:ℝhη:0 < ηhη':η < 1 / 2t:ℝa:ℝ := t - ηb:ℝ := t + ηthis:Fact (a < b) := ···⊢ b - a ≤ 1
C:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Ca✝:ℝb✝:ℝinst✝¹:Fact (a✝ < b✝)inst✝:Fact (b✝ - a✝ ≤ 1)s:Slicing Cη:ℝhη:0 < ηhη':η < 1 / 2t:ℝa:ℝ := t - ηb:ℝ := t + ηthis:Fact (a < b) := ···⊢ t + η - (t - η) ≤ 1
All goals completed! 🐙⟩
∀ (E : s.IntervalCat C a b),
IsStrictArtinianObject E ∧ IsStrictNoetherianObject E