Opposites of derived categories

For an abelian category C, using a derived contravariant functor with source (DerivedCategory C)ᵒᵖ requires comparing that category with DerivedCategory Cᵒᵖ. The pinned Mathlib supplies the corresponding opposite-category constructions on complexes and the localization machinery, but does not yet bundle this derived-category equivalence.

OppositeComparison records exactly that remaining comparison. It is generic categorical data: a later construction may provide it for any abelian category, while module and geometric duality consume the same root.

structure CategoryTheory.DerivedCategory.OppositeComparison (C : Type u) [Category.{v, u} C] [Abelian C] [Abelian Cᵒᵖ] [HasDerivedCategory C] [HasDerivedCategory Cᵒᵖ] : Type (max (max u v) w)

Explicit comparison between taking the opposite before and after forming a derived category.

• equivalence : (DerivedCategory C)ᵒᵖ ≌ DerivedCategory Cᵒᵖ

  The equivalence from the opposite derived category to the derived category of the opposite abelian category.