Hom comparison through t-structure truncations

A map from an object in the nonpositive aisle factors uniquely through its nonpositive truncation. When the two outer Hom groups of the next truncation triangle vanish, the map into the degree-zero truncation is an additive equivalence.

Main definitions

This file introduces no carrier, class, or instance.

Main results

• CategoryTheory.Triangulated.TStructure.homTruncLTAddEquiv identifies maps into an upper truncation from a source in the appropriate aisle.
• CategoryTheory.Triangulated.TStructure.homToDegreeZeroTruncAddEquiv identifies maps into a target with maps into its degree-zero truncation under explicit outer-Hom vanishing.

Implementation notes

The triangle factorization is private. Its injectivity and surjectivity use Mathlib's two coyoneda exactness lemmas, respectively. No t-structure vanishing is inferred from the generic statement's explicit hypotheses.

References

Mathlib's CategoryTheory.Triangulated.TStructure.liftTruncLT_ι, CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext, and CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ and CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃ at the pinned revision.

Tags

t-structure, truncation, additive Hom comparison

noncomputable def CategoryTheory.Triangulated.TStructure.homTruncLTAddEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (n : ℤ) [t.IsLE X n] : (X ⟶ (t.truncLT (n + 1)).obj Y) ≃+ (X ⟶ Y)

Maps from an object in the aisle ≤ n into a target factor uniquely and additively through its truncation τ_{<n+1}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.TStructure.homToDegreeZeroTruncAddEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X M : C} [t.IsLE X 0] (h₁ : ∀ (f : X ⟶ (t.truncLT 0).obj ((t.truncLT 1).obj M)), f = 0) (h₄ : ∀ (f : X ⟶ (shiftFunctor C 1).obj ((t.truncLT 0).obj ((t.truncLT 1).obj M))), f = 0) : (X ⟶ M) ≃+ (X ⟶ (t.truncGE 0).obj ((t.truncLT 1).obj M))

First lift through the nonpositive truncation using the source's aisle bound, then postcompose with its nonnegative truncation projection. The two outer-Hom vanishings give injectivity and surjectivity of the second step.

Equations

• t.homToDegreeZeroTruncAddEquiv h₁ h₄ = (t.homTruncLTAddEquiv 0).symm.trans (CategoryTheory.Triangulated.homMorTwoAddEquiv✝ ((t.triangleLTGE 0).obj ((t.truncLT 1).obj M)) ⋯ X h₁ h₄)