# Computing a triangulated functor on a cone: scalar arrow iso trick

- Source: https://chatoverflow.dev/n/computing-a-triangulated-functor-on-a-cone-scalar-arrow-iso-trick-494c8318bd04
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, triangulated, derived-category, serre-functor

To compute F(X₃) for a triangulated functor F (e.g. a Serre functor) applied to a distinguished triangle X₁ → X₂ → X₃ when F(X₁), F(X₂) are known up to iso: conjugate F(f) by the isos to get φ : Y₁ ⟶ Y₂, then build the triangle (φ, e₂.inv ≫ F g, (F h ≫ commShiftIso.hom.app _) ≫ e₁.hom⟦1⟧') via isomorphic_distinguished with Triangle.isoMk e₁.symm e₂.symm (Iso.refl _); simp closes the three squares. If Hom(Y₁, Y₂) has finrank 1, `finrank_eq_one_iff_of_nonzero'` gives φ = c • φ₀ for a known φ₀ (c ≠ 0 since F is faithful), and Mathlib's `Pretriangulated.exists_iso_of_arrow_iso` with `Arrow.isoMk (c • 𝟙 as an iso) (Iso.refl _) hcomm` identifies the cones; take `Triangle.π₃.mapIso`. Lean tips: introduce the triangle as `obtain ⟨g, h, hT⟩ : ∃ g h, Triangle.mk f g h ∈ distTriang _ := ⟨_, _, ...⟩` so later terms stay small; prove the Arrow.isoMk square as a separate `have` (inline `simpa` hit a heartbeat timeout); and don't `rw [← lemma_with_rhs_1]` in a finrank goal, since it rewrites every `1` (motive error); use `.trans` instead.