Serre duality and the Hom-built Euler form

For a Hom-finite category, Serre duality identifies each summand of χ(A, B) with the summand of χ(B, S A) in the opposite degree. Reindexing by negation proves the identity, even though finsum is junk-total without finite support. The bounded corollary supplies that support. This argument needs linearity of every shift functor, but does not require the Serre functor to be an equivalence or to commute with shifts.

Main results

SerreFunctorData.chiHom_eq_chiHom_swap_serre states the twisted identity under HomFinite. SerreFunctorData.chiHom_eq_chiHom_swap_serre_of_bounded supplies the version with HomFiniteBounded, ensuring the Euler sums have finite support. Shifting the second argument by n multiplies the Euler sum by (-1)^n.

• SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_of_serre_shift gives the pointwise formula for an arbitrary comparison object.
• SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_of_serre_shift_of_bounded makes it an equality of finite Euler sums.
• SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_twist specializes the comparison object to a functor's image of A.
• SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_twist_of_bounded gives that specialization with finite Hom support.
• SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_twist_of_natIso takes its pointwise comparison from a natural isomorphism.

Without HomFiniteBounded, the sums may still be junk-total.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_chiHom_swap_serre (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [HomFinite k C] (D : SerreFunctorData k C) (A B : C) : Triangulated.chiHom k C A B = Triangulated.chiHom k C B (D.S.obj A)

Serre duality gives χ(A, B) = χ(B, S A) for the Hom-built Euler form. The sum can be junk-total without a finite-support witness; use the bounded corollary for the mathematically meaningful Euler form.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_chiHom_swap_serre_of_bounded (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [Triangulated.HomFiniteBounded k C] (D : SerreFunctorData k C) (A B : C) : Triangulated.chiHom k C A B = Triangulated.chiHom k C B (D.S.obj A)

The twisted Euler identity with finite support of the Hom-built sums.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_of_serre_shift (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (D : SerreFunctorData k C) (A B X : C) (n : ℤ) [HomFinite k C] (e : D.S.obj A ≅ (shiftFunctor C n).obj X) : Triangulated.chiHom k C A B = ↑n.negOnePow * Triangulated.chiHom k C B X

A pointwise identification of the Serre image of A with X⟦n⟧ gives the signed Euler identity. Without bounded Hom support, the Euler sums may be junk-total.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_of_serre_shift_of_bounded (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (D : SerreFunctorData k C) (A B X : C) (n : ℤ) [Triangulated.HomFiniteBounded k C] (e : D.S.obj A ≅ (shiftFunctor C n).obj X) : Triangulated.chiHom k C A B = ↑n.negOnePow * Triangulated.chiHom k C B X

Bounded Hom support makes the signed pointwise identity an equality of actual finite Euler sums.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_twist (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (D : SerreFunctorData k C) (T : Functor C C) (A B : C) (n : ℤ) [HomFinite k C] (e : D.S.obj A ≅ (shiftFunctor C n).obj (T.obj A)) : Triangulated.chiHom k C A B = ↑n.negOnePow * Triangulated.chiHom k C B (T.obj A)

The pointwise signed Euler identity when the comparison object is the image of A under a fixed twist functor.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_twist_of_bounded (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (D : SerreFunctorData k C) (T : Functor C C) (A B : C) (n : ℤ) [Triangulated.HomFiniteBounded k C] (e : D.S.obj A ≅ (shiftFunctor C n).obj (T.obj A)) : Triangulated.chiHom k C A B = ↑n.negOnePow * Triangulated.chiHom k C B (T.obj A)

Bounded Hom support makes the twist formula an equality of finite Euler sums, instead of potentially junk-total sums.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.chiHom_eq_negOnePow_mul_chiHom_twist_of_natIso (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (D : SerreFunctorData k C) (T : Functor C C) (A B : C) (n : ℤ) [Triangulated.HomFiniteBounded k C] (e : D.S ≅ T.comp (shiftFunctor C n)) : Triangulated.chiHom k C A B = ↑n.negOnePow * Triangulated.chiHom k C B (T.obj A)

A natural identification S ≅ T ⋙ [n] supplies the objectwise comparison used in the bounded signed Euler identity.