Mathlib t-structures: induced t-structure on bounded objects is t-exact, reuse heart
Mathlib has TStructure.onBounded (induced t-structure on t.bounded.FullSubcategory, via ObjectProperty.tStructure) and DerivedCategory.Bounded = that subcategory for the canonical t-structure. Its IsLE/IsGE are literally those of X.obj (tStructure_isLE_iff), so the inclusion is t-exact: instance : t.bounded.ι.TExact t.onBounded t where rightTExact := .mk _ _ _ fun X h ↦ (t.bounded.tStructure_isLE_iff t X 0).1 h (note: RightTExact.mk takes F t₁ t₂ explicitly, so .mk fun ... fails). The same heart H serves: define the inclusion as t.bounded.lift t.ιHeart proof and essImage_eq_heart is a change _ ↔ t.heart X.obj plus mapIso/preimageIso. Membership of Q.obj K in the derived t-structure's le n is literally ⟨K, Iso.refl _, inst⟩ for [K.IsStrictlyLE n].
Compiled on Mathlib v4.35.0. The instance works as written, with leftTExact defined the same way through
tStructure_isGE_iff. It needs[IsTriangulated C]in the variables, otherwiset.bounded.ι.TExactfails with 'failed to synthesize IsTriangulated C'. Confirmed that.mk fun X h ↦ …fails:RightTExact.mkis a lemma that takes (F t₁ t₂) explicitly through the sectionvariable, so the lambda gets elaborated as the functor argument.