The derived lift of exact linear duality

The exact linear-dual functor of Algebra/Category/ModuleCat/LinearDual.lean induces a functor on derived categories. To use this lift from the opposite of a derived category, a client supplies the generic CategoryTheory.DerivedCategory.OppositeComparison. The resulting derived linear-dual functors are categorical infrastructure; geometric Serre duality imports them as consumers.

noncomputable def ModuleCat.derivedLinearDualFunctor (k : Type u) [Field k] : CategoryTheory.Functor (DerivedCategory (ModuleCat k)ᵒᵖ) (DerivedCategory (ModuleCat k))

The derived functor induced by exact algebraic linear duality. Its source is the derived category of the opposite abelian category.

Equations

• ModuleCat.derivedLinearDualFunctor k = (ModuleCat.linearDualFunctor k).mapDerivedCategory

noncomputable def ModuleCat.derivedLinearDualFromOpposite (k : Type u) [Field k] (B : CategoryTheory.DerivedCategory.OppositeComparison (ModuleCat k)) : CategoryTheory.Functor (DerivedCategory (ModuleCat k))ᵒᵖ (DerivedCategory (ModuleCat k))

Algebraic derived linear duality as a functor from the opposite derived category, once the explicit opposite/derived comparison is supplied.

Equations

• ModuleCat.derivedLinearDualFromOpposite k B = B.equivalence.functor.comp (ModuleCat.derivedLinearDualFunctor k)

noncomputable def ModuleCat.derivedLinearDualShift (k : Type u) [Field k] (B : CategoryTheory.DerivedCategory.OppositeComparison (ModuleCat k)) (n : ℤ) : CategoryTheory.Functor (DerivedCategory (ModuleCat k))ᵒᵖ (DerivedCategory (ModuleCat k))

Derived linear duality followed by a cohomological shift.

Equations

• ModuleCat.derivedLinearDualShift k B n = (ModuleCat.derivedLinearDualFromOpposite k B).comp (CategoryTheory.shiftFunctor (DerivedCategory (ModuleCat k)) n)