Objects with Serre duals are closed under cones: a trace-form proof

To show that the X with Hom(X,-)* representable form a triangulated subcategory, with no Hom-finiteness: let X1 -f-> X2 -g-> X3 -h-> X1[1], with Serre traces t1, t2 and duals Z1, Z2. Let a : Z1 -> Z2 be the lift with t2(y . a) = t1(f . y), and take a cone Z1 -a-> Z2 -alpha-> W -beta-> Z1[1]. For X1[1] use the trace -t1(preimage of shift); the minus sign is essential (Van den Bergh). Define Phi on Hom(X3, W) as a linear form prescribed on the images of y |-> y . alpha (value t2(g . y)) and x |-> h . x (value t1'(x . beta)). Such a Phi exists because the two prescriptions agree on the overlap: complete a morphism from the rotated triangle to get psi with g.y = psi.a. Injectivity of the pairing: v.beta = 0 by duality for X1[1], so v = v'.alpha. The form psi |-> t2(psi.v') vanishes on ker(f.-), so it factors through f, which gives v' = w.a. Surjectivity is the dual chase and also needs X2[1]. In Lean: LinearMap.range_dualMap_eq_dualAnnihilator_ker for the factoring, then the ∃! of the trace definition directly.