Thin interval categories and admissible subobjects

For a slicing s, s.IntervalCat C a b is the full subcategory of objects whose Harder--Narasimhan factors have phase in (a, b). An admissible subobject is one whose inclusion is the first map of a distinguished triangle whose quotient also lies in the same interval. This intrinsic triangulated description is independent of any retained quasi-abelian implementation.

def CategoryTheory.Triangulated.Slicing.intervalProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (a b : ℝ) : ObjectProperty C

The predicate defining the thin interval category P((a,b)).

Equations

• CategoryTheory.Triangulated.Slicing.intervalProp C s a b E = (CategoryTheory.Limits.IsZero E ∨ ∃ (F : CategoryTheory.Triangulated.HNFiltration C s.P E), ∀ (i : Fin F.n), a < F.φ i ∧ F.φ i < b)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.IntervalCat (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (a b : ℝ) : Type u

The thin interval category P((a,b)).

Equations

• CategoryTheory.Triangulated.Slicing.IntervalCat C s a b = (CategoryTheory.Triangulated.Slicing.intervalProp C s a b).FullSubcategory

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.IntervalCat.ι (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (a b : ℝ) : Functor (IntervalCat C s a b) C

The inclusion of a thin interval category into the ambient category.

Equations

• CategoryTheory.Triangulated.Slicing.IntervalCat.ι C s a b = (CategoryTheory.Triangulated.Slicing.intervalProp C s a b).ι

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_isZero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} (hE : Limits.IsZero E) (a b : ℝ) : intervalProp C s a b E

A zero object belongs to every thin interval.

instance CategoryTheory.Triangulated.Slicing.intervalProp_containsZero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (a b : ℝ) : (intervalProp C s a b).ContainsZero

def CategoryTheory.Triangulated.Slicing.IsAdmissibleSubobject (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} {E : IntervalCat C s a b} (A : Subobject E) : Prop

An admissible subobject in a thin interval is represented by a distinguished triangle whose third vertex also lies in that interval.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.AdmissibleSubobject (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} (E : IntervalCat C s a b) : Type (max 0 u v)

The ordered type of admissible subobjects of an interval object.

Equations

• CategoryTheory.Triangulated.Slicing.AdmissibleSubobject C s E = { A : CategoryTheory.Subobject E // CategoryTheory.Triangulated.Slicing.IsAdmissibleSubobject C s A }

def CategoryTheory.Triangulated.Slicing.IsAdmissiblyArtinian (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} (E : IntervalCat C s a b) : Prop

An interval object is admissibly Artinian if descending chains of admissible subobjects terminate.

Equations

• CategoryTheory.Triangulated.Slicing.IsAdmissiblyArtinian C s E = WellFoundedLT (CategoryTheory.Triangulated.Slicing.AdmissibleSubobject C s E)

def CategoryTheory.Triangulated.Slicing.IsAdmissiblyNoetherian (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} (E : IntervalCat C s a b) : Prop

An interval object is admissibly Noetherian if ascending chains of admissible subobjects terminate.

Equations

• CategoryTheory.Triangulated.Slicing.IsAdmissiblyNoetherian C s E = WellFoundedGT (CategoryTheory.Triangulated.Slicing.AdmissibleSubobject C s E)

def CategoryTheory.Triangulated.Slicing.IsFiniteLength (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} (E : IntervalCat C s a b) : Prop

Finite length in a thin interval, expressed intrinsically through admissible subobjects.

Equations

• CategoryTheory.Triangulated.Slicing.IsFiniteLength C s E = (CategoryTheory.Triangulated.Slicing.IsAdmissiblyArtinian C s E ∧ CategoryTheory.Triangulated.Slicing.IsAdmissiblyNoetherian C s E)

def CategoryTheory.Triangulated.admissibleSubobjectOrderIso {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (e x)) : { x : α // p x } ≃o { y : β // q y }

An order isomorphism restricts to an order isomorphism of subtypes when the two predicates correspond.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.admissibleSubobjectOrderIso_wellFoundedLT_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (e x)) : WellFoundedLT { x : α // p x } ↔ WellFoundedLT { y : β // q y }

theorem CategoryTheory.Triangulated.admissibleSubobjectOrderIso_wellFoundedGT_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (e x)) : WellFoundedGT { x : α // p x } ↔ WellFoundedGT { y : β // q y }