A Serre functor is unique up to natural isomorphism

Any two Serre functors on the same k-linear category are naturally isomorphic, and the isomorphism compatible with both duality isomorphisms is unique. The argument is Yoneda: S A represents B ↦ Dual (A ⟶ B), representing objects are unique up to unique isomorphism, and naturality in A promotes the pointwise isomorphisms to a natural isomorphism of functors.

The representability step has its own owner

isoOfLinearYonedaIso, its mapIso computation and hom_ext_of_linearYoneda are stated on linearYoneda alone and proved without reference to SerreFunctorData, because a downstream lane needs them on a functor that is not a Serre functor. They now live in CategoryTheory/Linear/Yoneda.lean, which this file imports; see that module for why the argument runs on linearYoneda rather than linearCoyoneda.

Trap: which variable the Yoneda argument runs in

Hom(A,B) is contravariant in A and covariant in B, and the dual flips both — so Dual (A ⟶ B) is covariant in A and contravariant in B, matching Hom(B, S A).

The Yoneda argument therefore runs in the B variable with A fixed. Naturality in A is a separate step, and it is what promotes the pointwise isomorphisms to a natural transformation.

Concretely: yonedaIso below is natural in B by naturality_right, and uniqueIso is natural in A by naturality_left. Two different fields of SerreFunctorData, for two different reasons.

No shift, no triangulation

Neither this file nor Basic mentions a shift or a distinguished triangle, which is why both live under CategoryTheory/Linear/. Ext profiles, shift relations, the Enriques refinement and every triangulated compatibility stay in CategoryTheory/Triangulated/SerreFunctor/, which imports this root.

Uniqueness of the Serre functor

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.compareEquiv {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (A B : C) : (B ⟶ D.S.obj A) ≃ₗ[k] B ⟶ D'.S.obj A

The comparison of the two duality isomorphisms at a fixed pair, as a linear equivalence (B ⟶ S A) ≃ₗ (B ⟶ S' A).

Equations

• D.compareEquiv D' A B = (D.eta A B).symm.trans (D'.eta A B)

theorem CategoryTheory.SerreFunctor.SerreFunctorData.compareEquiv_apply {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (A B : C) (psi : B ⟶ D.S.obj A) : (D.compareEquiv D' A B) psi = (D'.eta A B) ((D.eta A B).symm psi)

theorem CategoryTheory.SerreFunctor.SerreFunctorData.compareEquiv_naturality_right {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) {A B B' : C} (g : B' ⟶ B) (psi : B ⟶ D.S.obj A) : (D.compareEquiv D' A B') (CategoryStruct.comp g psi) = CategoryStruct.comp g ((D.compareEquiv D' A B) psi)

Naturality in B, from naturality_right. This is the step the Yoneda argument runs on.

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.yonedaIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (A : C) : (linearYoneda k C).obj (D.S.obj A) ≅ (linearYoneda k C).obj (D'.S.obj A)

The two representing objects have isomorphic linear Yoneda presheaves, at each A.

Equations

• D.yonedaIso D' A = CategoryTheory.NatIso.ofComponents (fun (B : Cᵒᵖ) => (D.compareEquiv D' A (Opposite.unop B)).toModuleIso) ⋯

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIsoApp {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (A : C) : D.S.obj A ≅ D'.S.obj A

The comparison isomorphism at an object.

Equations

• D.uniqueIsoApp D' A = CategoryTheory.SerreFunctor.isoOfLinearYonedaIso k C (D.yonedaIso D' A)

theorem CategoryTheory.SerreFunctor.SerreFunctorData.comp_uniqueIsoApp_hom {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) {A B : C} (psi : B ⟶ D.S.obj A) : CategoryStruct.comp psi (D.uniqueIsoApp D' A).hom = (D.compareEquiv D' A B) psi

The defining property of uniqueIsoApp: it is what the duality isomorphisms say it is.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIsoApp_hom_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (A : C) : (D.uniqueIsoApp D' A).hom = (D.compareEquiv D' A (D.S.obj A)) (CategoryStruct.id (D.S.obj A))

Evaluating the defining property at the identity.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIsoApp_naturality {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) {A A' : C} (f : A ⟶ A') : CategoryStruct.comp (D.S.map f) (D.uniqueIsoApp D' A').hom = CategoryStruct.comp (D.uniqueIsoApp D' A).hom (D'.S.map f)

Naturality in A, from naturality_left. This is the step that promotes the pointwise isomorphisms to a natural isomorphism of functors; see the module docstring on why it is a different field from the one yonedaIso uses.

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) : D.S ≅ D'.S

A Serre functor is unique up to natural isomorphism.

Equations

• D.uniqueIso D' = CategoryTheory.NatIso.ofComponents (fun (A : C) => D.uniqueIsoApp D' A) ⋯

@[simp]

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso_hom_app {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (A : C) : (D.uniqueIso D').hom.app A = (D.uniqueIsoApp D' A).hom

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso_compat {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) {A B : C} (phi : Module.Dual k (A ⟶ B)) : CategoryStruct.comp ((D.eta A B) phi) ((D.uniqueIso D').hom.app A) = (D'.eta A B) phi

The compatibility with the two duality isomorphisms, which is what characterises the comparison.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso_unique {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) (alpha : D.S ⟶ D'.S) (h : ∀ (A B : C) (phi : Module.Dual k (A ⟶ B)), CategoryStruct.comp ((D.eta A B) phi) (alpha.app A) = (D'.eta A B) phi) : alpha = (D.uniqueIso D').hom

Uniqueness of the comparison. Any natural transformation compatible with both duality isomorphisms is uniqueIso. This is the form a downstream coherence argument consumes, so it is not optional polish.

Coherence

So a downstream user can move a statement between two chosen Serre functors without re-deriving the comparison. Each is uniqueIso_unique applied to the obvious candidate.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso_refl {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) : D.uniqueIso D = Iso.refl D.S

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso_trans {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' D'' : SerreFunctorData k C) : CategoryStruct.comp (D.uniqueIso D').hom (D'.uniqueIso D'').hom = (D.uniqueIso D'').hom

theorem CategoryTheory.SerreFunctor.SerreFunctorData.uniqueIso_symm {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) : (D.uniqueIso D').symm = D'.uniqueIso D

theorem CategoryTheory.SerreFunctor.SerreFunctorData.exists_uniqueIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D D' : SerreFunctorData k C) : Nonempty (D.S ≅ D'.S)

HasSerreFunctor determines S up to natural isomorphism, so "the" Serre functor is a well-defined statement about C.