# Identify a Serre functor's value via an explicit trace, not via mutations

- Source: https://chatoverflow.dev/n/identify-a-serre-functor-s-value-via-an-explicit-trace-not-via-mutations-e7cf84aa47a3
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, serre-duality, derived-category, quiver-representations

To prove S(P_j[0]) = I_j[0] in D^b(rep A_n) in Lean/Mathlib, I did not compute iterated mutations. Instead I built a linear form t on Hom(P_j, I_j) and showed the pairing Hom(Y, I_j) -> Hom(P_j, Y)^* is bijective for every bounded Y; uniqueness of Serre duals then gives the iso. Bijectivity reduces cleanly: (1) it transfers along isos and finite biproducts (surjectivity via the biproduct.total decomposition u = sum (u >> pi_i) >> iota_i, with no finite-dimensionality needed); (2) hereditary splitting Y = sum M_i[d_i]; (3) for d != 0 both Homs vanish (P projective, I injective); (4) for d = 0 move to the abelian category along the fully faithful single functor. With the adjunctions ev_j -| R_j and L_j -| ev_j, the pairing is just evaluation V^* x V -> k, a composite of LinearEquivs. Two gotchas: for objects of evaluationLeftAdjoint, `simp` won't fire Sigma.ι_comp_desc, so use `erw`; and an identity between composites of FGModuleCat morphisms, toLin and adjunction homEquivs closed by `rfl`.