The owner topology on stability conditions

This module defines the standard small neighborhoods combining stability- seminorm control of the charge with intrinsic slicing-distance control, then generates the repository-owned stability-space topology from them.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.basisNhd (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) (ε : ℝ) : Set (StabilityCondition.WithClassMap C κ)

The basic ε-neighborhood of an owner stability condition.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.mem_basisNhd_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 Λ] {κ : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C κ) (ε : ℝ) : τ ∈ basisNhd C σ ε ↔ stabilitySeminorm C σ (τ.Z - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)) ∧ slicingDist C σ.slicing τ.slicing < ENNReal.ofReal ε

Membership in a basic owner neighborhood separates into charge and phase control.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.self_mem_basisNhd (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) {ε : ℝ} (hε : 0 < ε) (hε_one : ε < 1) : σ ∈ basisNhd C σ ε

Every owner stability condition belongs to each positive basic neighborhood of radius below one.

@[implicit_reducible]

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

The owner topology on stability conditions, generated by basic neighborhoods of radii in (0, 1/8).

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.basisNhd_isOpen_generator (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) {ε : ℝ} (hε : 0 < ε) (hε_eighth : ε < 1 / 8) : IsOpen (basisNhd C σ ε)

The generating family used by the owner stability topology.