Mass--Hom bounds at finite stability distance #
A finite full stability distance compares all HN masses by a uniform exponential factor. Consequently the mass--Hom property is constant on every finite-distance class and hence on every connected component. The locus is open and closed in the existing Section 6 topology.
def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.finiteDistanceClass
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(σ : WithClassMap C v)
:
Set (WithClassMap C v)
The full-stability-distance class of σ.
Equations
Instances For
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.isClopen_finiteDistanceClass
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(σ : WithClassMap C v)
:
A finite-distance class is open and closed in the existing stability topology. The temporary pseudo-extended-metric instance has definitionally that topology.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.connectedComponent_subset_finiteDistanceClass
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(σ : WithClassMap C v)
:
Every connected component is contained in the finite-distance class of any one of its points.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.of_stabilityDist_lt
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
{σ τ : WithClassMap C v}
{T : ObjectProperty C}
(h : σ.HasMassHomBound T)
{ε : ℝ}
(hε : 0 < ε)
(hd : stabilityDist σ τ < ENNReal.ofReal ε)
:
τ.HasMassHomBound T
Transport a mass--Hom bound across a specified strict distance bound.
The bound constant is multiplied by exp ε.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.of_finiteDistance
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
{σ τ : WithClassMap C v}
{T : ObjectProperty C}
(h : σ.HasMassHomBound T)
(hd : stabilityDist σ τ < ⊤)
:
τ.HasMassHomBound T
A mass--Hom bound transports across any finite full stability distance.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.finiteDistance_iff
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
{σ τ : WithClassMap C v}
{T : ObjectProperty C}
(hd : stabilityDist σ τ < ⊤)
:
The mass--Hom property is invariant under finite full stability distance.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.of_mem_connectedComponent
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
{σ τ : WithClassMap C v}
{T : ObjectProperty C}
(h : σ.HasMassHomBound T)
(hτ : τ ∈ connectedComponent σ)
:
τ.HasMassHomBound T
The mass--Hom property is constant on connected components of the stability space.
def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.massHomLocus
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
(T : ObjectProperty C)
:
Set (WithClassMap C v)
The locus of stability conditions satisfying a mass--Hom bound for T.
Equations
Instances For
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.isOpen_massHomLocus
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
(T : ObjectProperty C)
:
IsOpen (massHomLocus T)
The mass--Hom locus is open.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.isClosed_massHomLocus
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
(T : ObjectProperty C)
:
IsClosed (massHomLocus T)
The mass--Hom locus is closed.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.isClopen_massHomLocus
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[SerreFunctor.HomFinite k C]
(T : ObjectProperty C)
:
IsClopen (massHomLocus T)
The mass--Hom locus is clopen.