Local finiteness and stability conditions

This file adds the locally-finite refinement of the owner-controlled pre-stability API. The radius is normalized to be less than 1/2, so every window has width at most one.

structure CategoryTheory.Triangulated.Slicing.IsLocallyFinite (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) : Prop

A slicing is locally finite if one uniform thin window around every phase has finite length with respect to admissible subobjects.

• intervalFinite : ∃ (η : ℝ), 0 < η ∧ η < 1 / 2 ∧ ∀ (t : ℝ) (E : IntervalCat C s (t - η) (t + η)), IsFiniteLength C s E

  A uniform normalized radius with finite-length interval categories.

structure CategoryTheory.Triangulated.StabilityCondition.WithClassMap (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) extends CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v : Type (max u u')

A stability condition with a chosen class map.

• slicing : Slicing C
• Z : Λ →+ ℂ
• compat' (φ : ℝ) (E : C) : self.slicing.P φ E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), φ ≠ ↑n) → 0 < m) ∧ self.Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
• compatible (φ : ℝ) (E : C) : self.slicing.P φ E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 < m ∧ self.Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
• locallyFinite : Slicing.IsLocallyFinite C self.slicing

  The underlying slicing is locally finite.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} (hslicing : σ.slicing = τ.slicing) (hZ : σ.Z = τ.Z) : σ = τ

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} : σ = τ ↔ σ.slicing = τ.slicing ∧ σ.Z = τ.Z

@[reducible, inline]

abbrev CategoryTheory.Triangulated.StabilityCondition (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Type u

A stability condition with the identity class map.

Equations

• CategoryTheory.Triangulated.StabilityCondition C = CategoryTheory.Triangulated.StabilityCondition.WithClassMap C (AddMonoidHom.id (CategoryTheory.Triangulated.K₀ C))

theorem CategoryTheory.Triangulated.stabilityCondition_compat_apply (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (σ : StabilityCondition C) (φ : ℝ) (E : C) (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : ∃ (m : ℝ), 0 < m ∧ σ.Z (K₀.of C E) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)