Generator reduction for mass--Hom bounds

The test objects satisfying a mass--Hom bound form a thick subcategory: the property is invariant under shifts, closed under the middle term of a distinguished triangle, and inherited by retracts. The universal property of ObjectProperty.triangEnvelope therefore extends a bound from a classical generating collection to its thick envelope.

This is the generator half of Halpern--Leistner--Robotis, arXiv:2501.00710v2, Lemma 2.8. The stable-object half is kept in a separate leaf because it needs Jordan--Hölder input rather than thick closure.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.retract {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] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {A B : C} (hB : σ.HasMassHomBoundFor B) (r : Retract A B) : σ.HasMassHomBoundFor A

A retract of a test object inherits its mass--Hom bound.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.shift {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] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {A : C} (hA : σ.HasMassHomBoundFor A) (n : ℤ) : σ.HasMassHomBoundFor ((shiftFunctor C n).obj A)

Shifting a test object by any integer preserves its mass--Hom bound.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.of_isZero {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] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {A : C} (hA : Limits.IsZero A) : σ.HasMassHomBoundFor A

The zero object satisfies a mass--Hom bound with constant one.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.triangle_middle {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] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : σ.HasMassHomBoundFor T.obj₁) (h₃ : σ.HasMassHomBoundFor T.obj₃) : σ.HasMassHomBoundFor T.obj₂

In a distinguished triangle, bounds for the first and third test objects give a bound for the middle test object.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.massHomBoundedTests {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] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} (s : WithClassMap C v₀) : ObjectProperty C

The object property of tests which admit some mass--Hom constant.

Equations

• s.massHomBoundedTests A = s.HasMassHomBoundFor A

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.triangEnvelope {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] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} (G : ObjectProperty C) (hG : σ.HasMassHomBound G) : σ.HasMassHomBound G.triangEnvelope

A mass--Hom bound on a generating collection extends to its thick triangulated envelope.