Transfer of mass--Hom bounds

Let G : C ⥤ D detect a preimage stability condition and let L ⊣ G be a linear adjunction. A mass--Hom bound for a test object A : D transfers to L.obj A: the adjunction identifies Hom(LA, F) with Hom(A, GF), while stabilityMass_preimage identifies the two masses.

Consequently, a bound on a target test class T transfers to the essential image T.map L and then, by thick closure, to every source test class contained in (T.map L).triangEnvelope. The generation comparison is deliberately an explicit hypothesis: the abstract theorem neither supplies a geometric generator nor assumes that L preserves one.

This is the categorical core of arXiv:2607.28411v1, Lemma 7.4. Its finite and faithfully-flat geometric realizations are separate consumers.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.preimage_obj {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] [SerreFunctor.HomFinite k C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Linear k D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] [SerreFunctor.HomFinite k D] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ D →+ Λ} {G : Functor C D} [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] {L : Functor D C} [L.Additive] [Functor.Linear k L] {σ : WithClassMap D v₀} {A : D} (hA : σ.HasMassHomBoundFor A) (adj : L ⊣ G) (hpre : σ.slicing.PreimageData G) : (σ.preimage G hpre).HasMassHomBoundFor (L.obj A)

An objectwise mass--Hom bound transfers across a linear left adjoint.

No conservativity hypothesis is needed here. The supplied PreimageData already says that the preimage slicing is a genuine slicing, and the proof uses only the adjunction on Hom spaces and the exact mass identity.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.preimage_map {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] [SerreFunctor.HomFinite k C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Linear k D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] [SerreFunctor.HomFinite k D] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ D →+ Λ} {G : Functor C D} [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] {L : Functor D C} [L.Additive] [Functor.Linear k L] {σ : WithClassMap D v₀} {T : ObjectProperty D} (h : σ.HasMassHomBound T) (adj : L ⊣ G) (hpre : σ.slicing.PreimageData G) : (σ.preimage G hpre).HasMassHomBound (T.map L)

A mass--Hom bound transfers to the essential image of the test class under the linear left adjoint.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.preimage {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] [SerreFunctor.HomFinite k C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Linear k D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] [SerreFunctor.HomFinite k D] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ D →+ Λ} {G : Functor C D} [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] {L : Functor D C} [L.Additive] [Functor.Linear k L] {σ : WithClassMap D v₀} {T : ObjectProperty D} {T' : ObjectProperty C} [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (h : σ.HasMassHomBound T) (adj : L ⊣ G) (hpre : σ.slicing.PreimageData G) (hgen : T' ≤ (T.map L).triangEnvelope) : (σ.preimage G hpre).HasMassHomBound T'

Transfer a mass--Hom bound to a source test class generated by the left-adjoint images of the bounded target tests.

The containment T' ≤ (T.map L).triangEnvelope is the exact generation input. Geometric applications may instantiate T and T' by perfect complexes, but that comparison is not asserted by this categorical theorem.