Serre functors and shifts

The shift comparison comes from conjugation by the shift equivalence and uniqueness of the Serre functor. Applying Serre uniqueness directly to S ⋙ [1] and [1] ⋙ S is invalid: either functor represents the dual of Hom(A, B⟦-1⟧), rather than the dual of Hom(A, B).

The displayed comparison is coherent in the shift index. The resulting CommShift ℤ does not itself establish preservation of distinguished triangles; that separate exactness argument must use the signed rotation convention.

Main definition

SerreFunctorData.commShiftIso n specializes linear conjugation transport to the equivalence given by the single shift n. SerreFunctorData.commShift assembles these comparisons into a coherent CommShift ℤ structure. SerreFunctorData.signedCommShift adjusts each component by (-1)^n for the rotation convention; signedCommShift_one_inv_app and trace_shift_one_signed state its degree-one consequences.

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.commShiftIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) (n : ℤ) [(shiftFunctor C n).Additive] [Functor.Linear k (shiftFunctor C n)] : D.S.comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp D.S

The Serre functor commutes with each shift, by conjugation with the corresponding shift equivalence. This is the orientation used in #898; Mathlib's CommShift stores the inverse orientation.

Equations

• D.commShiftIso n = (D.transportIso (CategoryTheory.shiftEquiv C n)).symm

@[implicit_reducible]

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.commShift {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] : D.S.CommShift ℤ

The conjugation transports give D.S a coherent commutation with integer shifts. Its component at n is (D.commShiftIso n).symm; the zero and addition laws follow from transport functoriality. Triangle preservation requires a separate signed comparison.

Equations

• D.commShift = { commShiftIso := fun (n : ℤ) => D.transportIso (CategoryTheory.shiftEquiv C n), commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

@[implicit_reducible]

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.signedCommShift {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] : D.S.CommShift ℤ

The sign-corrected shift commutation used by the triangulated rotation convention. It is derived from the coherent conjugation transport and is chosen explicitly by downstream exactness proofs.

Equations

• D.signedCommShift = CategoryTheory.SerreFunctor.SerreFunctorData.signedCommShiftOfCommShift✝ D.S

theorem CategoryTheory.SerreFunctor.SerreFunctorData.signedCommShift_one_inv_app {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (X : C) : (Functor.commShiftIso D.S 1).inv.app X = -(D.commShiftIso 1).hom.app X

At degree one, the inverse signed component is the negative of the pointwise Serre/shift comparison.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.trace_shift_one_signed {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (D : SerreFunctorData k C) [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (X : C) (x : X ⟶ D.S.obj X) : (D.trace ((shiftFunctor C 1).obj X)) (CategoryStruct.comp ((shiftFunctor C 1).map x) ((Functor.commShiftIso D.S 1).inv.app X)) = -(D.trace X) x

The signed degree-one transport reverses the Serre trace.