Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Foundation.Deformation.LocalFiniteness

Uniform finite-length sectors for deformation theory #

Local finiteness supplies one uniform interval around every phase. The deformation argument uses rescaled radii so that both thin sectors of radius 2 ε and wide sectors of radius 4 ε have finite length. This module extracts those witnesses directly from the owner stability-condition data.

source
def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SectorFiniteLength (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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) (ε : ℝ) :
Prop

Every owner interval of radius 2 ε has finite length.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength (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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) (ε : ℝ) :
    Prop

    Every owner interval of radius 4 ε has finite length.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.exists_wideSectorRadius (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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) :
      ∃ (ε : ℝ), 0 < ε ∧ ε < 1 / 8 ∧ WideSectorFiniteLength C σ ε

      Owner local finiteness yields a normalized wide deformation radius.

      source
      theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.exists_sectorRadius (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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) :
      ∃ (ε : ℝ), 0 < ε ∧ ε < 1 / 4 ∧ SectorFiniteLength C σ ε

      Owner local finiteness also yields the thin-sector radius used for the first phase-perturbation construction.