The adjoint transposition behind Proposition 3.8

Proposition 3.8 of arXiv:2607.28411v1 proves that f_♯𝒫 is a slicing under the hypothesis (3.2), f^* f_* 𝒫(φ) ⊆ 𝒫(≤ φ). Its proof has one categorical step and one appeal to Appendix A: the hypothesis of Corollary A.23 for Φ = f^* is f^* f_! 𝒫(φ) ⊆ 𝒫(≥ φ), and it is obtained from (3.2) by transposing twice along the adjunctions f_! ⊣ f^* ⊣ f_*:

Hom(f^* f_! E, G) ≅ Hom(f_! E, f_* G) ≅ Hom(E, f^* f_* G) = 0

for E ∈ 𝒫(φ) and G ∈ 𝒫(< φ). This file proves that step for an arbitrary functor F with a left adjoint L and a right adjoint R.

Main definitions

• Slicing.MapsSemistableLE: an endofunctor sends every semistable object of phase φ into 𝒫(≤ φ). At the comonad f^* f_* this is the paper's condition (3.2).
• Slicing.MapsSemistableGE: an endofunctor sends every semistable object of phase φ into 𝒫(≥ φ). At the monad f^* f_! this is the bounded form of the Corollary A.23 hypothesis.

Main results

• Slicing.MapsSemistableLE.leProp_of_leProp: the condition, stated on semistable objects, extends to every object with HN phases at most t, by applying the exact endofunctor to the HN filtration and using closure of the phase cut under towers.
• Slicing.MapsSemistableGE.of_mapsSemistableLE: the transposition itself.

Implementation notes

The two predicates are stated for an arbitrary endofunctor rather than for the comonad and monad of a pair of adjunctions, since neither statement uses the adjunction structure; the adjunctions enter only in the transposition. Theorem A.17 of the paper calls its hypothesis on Φ Φ_L the monad hypothesis; MapsSemistableGE is the bounded phase-cut form in which Corollary A.23 uses it.

The composite R ⋙ F must be exact, which is all the phase-cut half needs, and L and F need only preserve zero morphisms, for the two transpositions. The proofs never use exactness of R or F separately, so the hypothesis is stated on the composite, and the source category C needs no triangulated structure at all.

What this file does not do is verify (3.2) geometrically or feed the conclusion to the Appendix A machinery on Dqc; those are the remaining steps of Proposition 3.8 and stay explicit.

References

• arXiv:2607.28411v1, Proposition 3.8 and Corollary A.23.
• arXiv:2601.22994, Proposition 3.4, the smooth projective case over ℂ.

def CategoryTheory.Triangulated.Slicing.MapsSemistableLE {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (s : Slicing D) (G : Functor D D) : Prop

An endofunctor G sends every semistable object of phase φ into the upper phase cut 𝒫(≤ φ). For the comonad G = f^* f_* of the adjunction f^* ⊣ f_* this is condition (3.2) of arXiv:2607.28411v1.

Equations

• s.MapsSemistableLE G = ∀ (φ : ℝ) (E : D), s.P φ E → CategoryTheory.Triangulated.Slicing.leProp D s φ (G.obj E)

def CategoryTheory.Triangulated.Slicing.MapsSemistableGE {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (s : Slicing D) (G : Functor D D) : Prop

An endofunctor G sends every semistable object of phase φ into the lower phase cut 𝒫(≥ φ). For the monad G = f^* f_! of the adjunction f_! ⊣ f^* this is the bounded form of the hypothesis of Corollary A.23 of arXiv:2607.28411v1.

Equations

• s.MapsSemistableGE G = ∀ (φ : ℝ) (E : D), s.P φ E → CategoryTheory.Triangulated.Slicing.geProp D s φ (G.obj E)

theorem CategoryTheory.Triangulated.Slicing.MapsSemistableLE.leProp_of_leProp {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {G : Functor D D} [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] (h : s.MapsSemistableLE G) {t : ℝ} {E : D} (hE : leProp D s t E) : leProp D s t (G.obj E)

The condition extends from semistable objects to every object with HN phases at most t: the exact endofunctor carries the HN filtration to a Postnikov tower whose factors satisfy the cut by hypothesis, and Slicing.leProp_of_postnikovTower closes up.

theorem CategoryTheory.Triangulated.Slicing.MapsSemistableGE.of_mapsSemistableLE {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {L : Functor D C} {F : Functor C D} {R : Functor D C} [(R.comp F).Additive] [(R.comp F).CommShift ℤ] [(R.comp F).IsTriangulated] [L.PreservesZeroMorphisms] [F.PreservesZeroMorphisms] (adjL : L ⊣ F) (adjR : F ⊣ R) (h : s.MapsSemistableLE (R.comp F)) : s.MapsSemistableGE (L.comp F)

The adjoint transposition of Proposition 3.8. If the comonad R ⋙ F of F ⊣ R satisfies (3.2), then the monad L ⋙ F of L ⊣ F satisfies the Corollary A.23 hypothesis. For E ∈ 𝒫(φ) and G ∈ 𝒫(< φ), a morphism F L E ⟶ G transposes to E ⟶ F R G, whose target lies in 𝒫(< φ) by Slicing.MapsSemistableLE.leProp_of_leProp, so it vanishes; transposing back through the counits shows the original morphism vanishes, and Slicing.geProp_of_forall_hom_eq_zero concludes.