Serre functors on linear categories

A Serre functor on a k-linear category is an endofunctor S together with natural linear equivalences

Dual k (A ⟶ B) ≃ₗ[k] (B ⟶ S.obj A).

The pointwise equivalences and their two naturality equations are the fields of SerreFunctorData. This is data by the mathematical nature of a Serre functor, not a ...Data wrapper meaning that an unproved theorem has silently been postulated. Geometric consumers may later supply such data explicitly.

Which notion this is: a right Serre functor

SerreFunctorData asks for the duality and its naturality and nothing else. It does not ask that S be an equivalence, so what it defines is Reiten--Van den Bergh's right Serre functor, not the Serre functor of Bondal--Kapranov and Huybrechts, who additionally require S to be a k-linear autoequivalence. That extra clause is SerreCategoryData.serreIsEquivalence below, and the geometric consumers take that stronger package.

The weaker notion is the useful one to state theorems from, and the split is deliberate: everything proved here holds for a right Serre functor, and a consumer that genuinely needs essential surjectivity asks for it by taking SerreCategoryData. The gap is real rather than cosmetic — a right Serre functor is fully faithful under Hom-finiteness but need not be essentially surjective — so HasRightSerreFunctor must not be read as "this category has a Serre functor" in the Bondal--Kapranov sense.

No shift or triangulation is needed for the definition. Hom-finiteness is a separate property and appears only where double-dual or dimension arguments actually spend it.

The naturality fields alone imply that the Serre endofunctor is additive; SerreFunctorData.additive provides this fact without a global instance.

The would-be functor-level packaging has variance C × Cᵒᵖ: dualising reverses the contravariance/covariance of Hom(A,B). It is deliberately not exported at these general universes. If k : Type w and morphisms live in Type v, then Dual k Hom(A,B) lives in Type (max w v) while Hom(B,S A) remains in Type v; without an equality or a systematic ULift, they are not objects of the same ModuleCat. The pointwise ≃ₗ has no such artificial restriction and every downstream theorem uses it directly.

class CategoryTheory.SerreFunctor.HomFinite (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] : Prop

Every Hom-space of a linear category is finite-dimensional.

• finite (A B : C) : Module.Finite k (A ⟶ B)

  The finite-dimensionality witness for each Hom-space.

structure CategoryTheory.SerreFunctor.SerreFunctorData (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] : Type (max (max u v) w)

A Serre functor with its natural duality equivalence.

The two equations are written pointwise to keep the variance explicit and to avoid hiding the load-bearing content inside a large functor expression.

• S : Functor C C

  The underlying endofunctor.

• eta (A B : C) : Module.Dual k (A ⟶ B) ≃ₗ[k] B ⟶ self.S.obj A

  Serre duality, pointwise.

• naturality_left {A A' B : C} (f : A ⟶ A') (phi : Module.Dual k (A ⟶ B)) : (self.eta A' B) (phi ∘ₗ Linear.leftComp k B f) = CategoryStruct.comp ((self.eta A B) phi) (self.S.map f)

  Naturality in the first, covariant variable.

• naturality_right {A B B' : C} (g : B' ⟶ B) (phi : Module.Dual k (A ⟶ B)) : (self.eta A B') (phi ∘ₗ Linear.rightComp k A g) = CategoryStruct.comp g ((self.eta A B) phi)

  Naturality in the second, contravariant variable.

@[reducible, inline]

abbrev CategoryTheory.SerreFunctor.HasRightSerreFunctor (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] : Prop

The property that a category admits some right Serre functor.

Named for the weaker notion on purpose; see the module docstring. For the Bondal--Kapranov notion, which additionally requires S to be an autoequivalence, use Nonempty (SerreCategoryData k C).

Equations

• CategoryTheory.SerreFunctor.HasRightSerreFunctor k C = Nonempty (CategoryTheory.SerreFunctor.SerreFunctorData k C)

structure CategoryTheory.SerreFunctor.SerreCategoryData (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] : Type (max (max u v) w)

A chosen Serre functor which is an autoequivalence.

This is the Bondal--Kapranov / Huybrechts notion: SerreFunctorData supplies the duality, and serreIsEquivalence supplies the clause that makes it a Serre functor rather than only a right one.

This is the common categorical package used by geometric residual categories. The stronger EnriquesCategoryData adds a specified relation between the square of the Serre functor and a shift.

• serre : SerreFunctorData k C

  The chosen Serre functor and duality.

• serreIsEquivalence : self.serre.S.IsEquivalence

  The Serre functor is an autoequivalence.

theorem CategoryTheory.SerreFunctor.SerreCategoryData.hasSerreEquivalence {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (A : SerreCategoryData k C) : A.serre.S.IsEquivalence

The chosen Serre functor can be used as an equivalence by a consumer without installing a global instance.

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

Naturality of Serre duality makes its endofunctor additive, without a Hom-finiteness or equivalence assumption.

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

The Serre pairing Hom(A,B) × Hom(B,S A) → k.

Equations

• D.pairing A B = { toFun := fun (f : A ⟶ B) => { toFun := fun (g : B ⟶ D.S.obj A) => ((D.eta A B).symm g) f, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

theorem CategoryTheory.SerreFunctor.SerreFunctorData.pairing_separating_left {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (A B : C) (f : A ⟶ B) (hf : ∀ (g : B ⟶ D.S.obj A), ((D.pairing A B) f) g = 0) : f = 0

The Serre pairing separates its first argument.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.pairing_separating_right {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (A B : C) (g : B ⟶ D.S.obj A) (hg : ∀ (f : A ⟶ B), ((D.pairing A B) f) g = 0) : g = 0

The Serre pairing separates its second argument.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.finrank_hom_eq {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) [HomFinite k C] (A B : C) : Module.finrank k (A ⟶ B) = Module.finrank k (B ⟶ D.S.obj A)

Serre duality identifies the dimensions of the two Hom-spaces.

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

The Serre trace on maps A ⟶ S A.

Equations

• D.trace A = { toFun := fun (f : A ⟶ D.S.obj A) => ((D.eta A A).symm f) (CategoryTheory.CategoryStruct.id A), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CategoryTheory.SerreFunctor.SerreFunctorData.trace_apply {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (A : C) (f : A ⟶ D.S.obj A) : (D.trace A) f = ((D.eta A A).symm f) (CategoryStruct.id A)

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

Cyclicity of the Serre trace, obtained from both naturality fields.