The support property under transfer

Remarks 3.2 and 3.7 of arXiv:2607.28411v1 observe that once the preimage collection is a slicing, the transported condition f^♯σ or f_♯σ satisfies the support property with respect to the same quadratic form as σ, on the class map v ∘ K₀(F). The last paragraph of the proof of Proposition 3.4 of arXiv:2601.22994 makes the same observation for the norm-bound formulation.

Main results

• PreStabilityCondition.WithClassMap.preimage_semistableClasses_subset: the semistable classes of the transported condition are semistable classes of the original one. This is the whole content: every nonzero semistable object of the transported condition maps to a nonzero semistable object of the same phase, and its transported class is the class of that image.
• PreStabilityCondition.WithClassMap.HasSupportProperty.preimage: the norm-bound support property transfers with the same real-linear charge and the same constant.
• PreStabilityCondition.WithClassMap.QuadraticSupportData.preimage: genuine quadratic support transfers with the same quadratic form, which is the form in which the paper states the support property (Definition 2.2).

Implementation notes

Both transfer theorems are monotonicity of the underlying numerical predicates in the selected locus, applied to the inclusion of semistable classes. Nothing about the functor beyond the lifting witness enters; in particular the negative-definiteness of the quadratic form on the kernel of the charge is a statement about Λ_ℝ and Z alone and is untouched.

References

• arXiv:2607.28411v1, Remarks 3.2 and 3.7.
• arXiv:2601.22994, Proposition 3.4.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.preimage_semistableClasses_subset {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {V : Type u_1} [NormedAddCommGroup V] {v : K₀ D →+ V} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) : (σ.preimage F h).semistableClasses ⊆ σ.semistableClasses

Every semistable class of the transported condition is a semistable class of the original condition: a nonzero object semistable of phase φ for the preimage slicing has a nonzero image semistable of phase φ, and the class map v ∘ K₀(F) evaluates to the class of that image.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.HasSupportProperty.preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ D →+ V} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) {Zlin : V →ₗ[ℝ] ℂ} (hσ : σ.HasSupportProperty Zlin) : (σ.preimage F h).HasSupportProperty Zlin

The norm-bound support property transfers along a phase-detecting functor, with the same real-linear charge and the same constant, since the transported semistable locus is contained in the original one.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.QuadraticSupportData.preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ D →+ V} (σ : WithClassMap D v) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) {Zlin : V →ₗ[ℝ] ℂ} (hσ : σ.QuadraticSupportData Zlin) : (σ.preimage F h).QuadraticSupportData Zlin

Genuine quadratic support transfers along a phase-detecting functor with the same quadratic form and the same charge: HasQuadraticSupportProperty.mono keeps the witness Q verbatim, since the transported semistable locus is a subset. This is the support half of Remarks 3.2 and 3.7 of arXiv:2607.28411v1; the local-finiteness half is Slicing.PreimageData.isLocallyFinite, and only the two together give a stability condition for (V, v ∘ K₀(F)).