Phases and orders under preimage transfer #
Once a raw preimage collection has been proved to be a slicing, its HN filtrations map forward without changing their phases. If the functor also reflects zero objects, this identifies the intrinsic extreme phases, hence the strict and weak phase windows. This proves Lemmas 3.5 and 3.9 and the order clause of Remark 3.14(3) of arXiv:2607.28411v1 at the categorical level.
Reflection of zero objects is in fact a consequence of the lifting witness
itself (Slicing.PreimageData.reflectsZeroObjects), so the two-witness forms
of the order transfer (Slicing.Precedes.preimage_of_preimageData, Lemma 3.3
of arXiv:2601.22994) and the distance inequality of Lemmas 3.5(3) and 3.9(3)
(slicingDist_preimage_le) take no conservativity hypothesis at all.
A functor reflects zero objects. This is the object-level consequence of conservativity used by phase transfer.
Equations
- CategoryTheory.Triangulated.ReflectsZeroObjects F = ∀ (E : C), CategoryTheory.Limits.IsZero (F.obj E) → CategoryTheory.Limits.IsZero E
Instances For
A faithful additive functor reflects zero objects.
A conservative additive functor reflects zero objects. This is the exact object-level use of conservativity in the source phase identities.
The Hom-vanishing half of the slicing-lifting witness forces the detecting
functor to reflect zero objects, so the conservativity that Remarks 3.2 and
3.7 of arXiv:2607.28411v1 add by hand is a consequence rather than a
hypothesis. Take E with F.obj E zero; then E lies in the preimage
slices of phases 1 and 0 at once, and Hom-vanishing from the higher to the
lower phase forces 𝟙 E = 0.
The contrapositive of Slicing.PreimageData.reflectsZeroObjects, in the
shape every downstream caller needs: ¬IsZero is the hypothesis form taken by
Slicing.phiPlus, Slicing.phiMinus, the positivity field of a
pre-stability condition, and semistableClasses, so this is the form in
which conservativity is actually consumed, never ReflectsZeroObjects
itself.
An HN filtration for the preimage slicing maps to an HN filtration with the same phases in the target slicing.
Equations
- CategoryTheory.Triangulated.HNFiltration.mapPreimage s F h Fil = Fil.mapF F ⋯
Instances For
The highest HN phase is computed after applying the detecting functor.
The lowest HN phase is computed after applying the detecting functor.
Strict upper phase windows are reflected by a preimage slicing.
Weak upper phase windows are reflected by a preimage slicing.
Preimage transfer commutes with real phase translation. The HN proofs on the two sides may differ, but slicings are determined by their phase slices.
Canonical form of phase-shift compatibility, using the phase-shifted
lifting data derived from h.
A family of preimage constructions satisfying the lifting criterion gives the exact objectwise interface used by the slicing-order API.
Equations
- ⋯ = ⋯
Instances For
Genuine preimage transfer preserves the strict slicing order.
Genuine preimage transfer preserves the weak slicing order.
Order and distance from two lifting witnesses #
Slicing.Precedes.preimage asks for lifting data on every slicing of the
target. The paper's statements only ever involve the two slicings being
compared, so the two-witness forms below are the ones a geometric consumer
can discharge, and the reflection of zero objects they need is supplied by
the witnesses themselves.
Transfer preserves the strict slicing order, given lifting witnesses for
the two slicings involved. This is Lemma 3.3 of arXiv:2601.22994: an object
semistable for the transferred s maps to an object semistable for s, whose
HN phases for t are strictly below its phase, and those phases are the HN
phases for the transferred t.
The ≤ twin of Slicing.Precedes.preimage_of_preimageData, proved the
same way through preimage_leProp_iff instead of preimage_ltProp_iff; both
are the two-witness form of Lemma 3.3 of arXiv:2601.22994, which is what a
geometric consumer can discharge without the family-wide hypothesis of
Slicing.PrecedesWeak.preimage.
Transfer does not increase the generalized distance between slicings, Lemma 3.5(3) and Lemma 3.9(3) of arXiv:2607.28411v1. Every phase discrepancy on the source is a phase discrepancy on the target at the image object, so the source supremum runs over a subset of the target terms.