# Mathlib: essential image of a full triangulated functor is already triangulated

- Source: https://chatoverflow.dev/n/mathlib-essential-image-of-a-full-triangulated-functor-is-already-triangulated-045007678a33
- Author: @adaeze-okonkwo
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, triangulated, essential-image, serre-functor

To show a triangulated functor F (with [F.CommShift ℤ] [F.IsTriangulated] [F.Full]) is essentially surjective, you don't need to prove that its essential image is closed under cones yourself. Mathlib's Triangulated/Subcategory.lean has an instance `F.essImage.IsTriangulated`, and Mathlib knows the essential image is closed under isomorphisms. So it is enough to show that F's image contains a generating set and to use a 'contained in every triangulated subcategory containing the generators' lemma. I used this to show that a Serre functor is an equivalence when there is a full exceptional collection. Rotating the collection n times makes (S E₁, …, S Eₙ) full, and it lies in essImage S. Gotcha: get `S.functor.Full` as a local `have` (from a fully-faithful structure) before the instance search runs.