Full faithfulness and co-Serre duality

Finite-dimensionality of all Hom spaces lets right Serre duality identify each Hom space with its double dual. This module uses that identification and the naturality laws to prove full faithfulness, and derives an equivalence only when independent co-Serre data is supplied.

Main definitions

CoSerreFunctorData abbreviates the canonical SerreFunctorData k Cᵒᵖ root. Its functor and duality accessors view that opposite-category presentation on C.

Main results

SerreFunctorData.fullyFaithful and CoSerreFunctorData.fullyFaithful use double-dual evaluation. CoSerreFunctorData.adjunction combines the two dualities without a Hom-finiteness assumption. SerreFunctorData.isEquivalence uses that adjunction and the full faithfulness of both functors.

Implementation notes

The adjunction is oriented E.S ⊣ D.S; the co-Serre witness supplies essential surjectivity rather than being inferred from right Serre data. This module needs no shift or triangulated structure.

References

A. I. Bondal and M. M. Kapranov, “Representable functors, Serre functors, and reconstructions,” Math. USSR-Izv. 35 (1990), 519–541.

Tags

Serre functor, co-Serre functor, full faithfulness, Hom-finite, adjunction

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

A right Serre functor is fully faithful when every Hom space is finite-dimensional. The proof uses Module.evalEquiv for the named double-dual step.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

A co-Serre witness is the right Serre-data root on the opposite category. This abbreviation keeps the same canonical duality fields rather than introducing a second structure with mirrored data.

Equations

• CategoryTheory.SerreFunctor.CoSerreFunctorData k C = CategoryTheory.SerreFunctor.SerreFunctorData k Cᵒᵖ

def CategoryTheory.SerreFunctor.CoSerreFunctorData.S {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : CoSerreFunctorData k C) : Functor C C

View the opposite-category Serre endofunctor as an endofunctor of C.

Equations

• D.S = D.S.unop

def CategoryTheory.SerreFunctor.CoSerreFunctorData.eta {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : CoSerreFunctorData k C) (A B : C) : Module.Dual k (A ⟶ B) ≃ₗ[k] D.S.obj B ⟶ A

View opposite-category Serre duality in the co-Serre orientation on C.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.SerreFunctor.CoSerreFunctorData.naturality_left {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : CoSerreFunctorData k C) {A A' B : C} (f : A ⟶ A') (phi : Module.Dual k (A ⟶ B)) : (D.eta A' B) (phi ∘ₗ Linear.leftComp k B f) = CategoryStruct.comp ((D.eta A B) phi) f

Naturality in the first variable, transported from opposite-category Serre naturality.

theorem CategoryTheory.SerreFunctor.CoSerreFunctorData.naturality_right {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : CoSerreFunctorData k C) {A B B' : C} (g : B' ⟶ B) (phi : Module.Dual k (A ⟶ B)) : (D.eta A B') (phi ∘ₗ Linear.rightComp k A g) = CategoryStruct.comp (D.S.map g) ((D.eta A B) phi)

Naturality in the second variable, transported from opposite-category Serre naturality.

noncomputable def CategoryTheory.SerreFunctor.CoSerreFunctorData.fullyFaithful {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HomFinite k C] (D : CoSerreFunctorData k C) : D.S.FullyFaithful

A co-Serre functor is fully faithful under finite-dimensional Hom hypotheses. This reuses full faithfulness of the canonical Serre-data root on the opposite category.

Equations

• D.fullyFaithful = id (CategoryTheory.SerreFunctor.SerreFunctorData.fullyFaithful k Cᵒᵖ D).unop

noncomputable def CategoryTheory.SerreFunctor.CoSerreFunctorData.adjunction {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : CoSerreFunctorData k C) (E : SerreFunctorData k C) : D.S ⊣ E.S

The two pointwise dualities give an adjunction D.S ⊣ E.S.

Hom-finiteness is not needed for this adjunction: only the two supplied duality equivalences and their naturality equations enter the Hom-set equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.isEquivalence {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HomFinite k C] (D : SerreFunctorData k C) (E : CoSerreFunctorData k C) : D.S.IsEquivalence

Right Serre data is an equivalence when a co-Serre witness is also supplied. The proof uses the adjunction from CoSerreFunctorData.adjunction; full faithfulness of both adjoints makes its unit and counit isomorphisms.

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.toSerreCategoryData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HomFinite k C] (D : SerreFunctorData k C) (E : CoSerreFunctorData k C) : SerreCategoryData k C

Use this adapter when a downstream API requires the stronger SerreCategoryData package; keeping the co-Serre witness explicit prevents right Serre data from being silently upgraded to an autoequivalence.

Equations

• D.toSerreCategoryData E = { serre := D, serreIsEquivalence := ⋯ }