Involutive contravariant endofunctors #

A contravariant endofunctor F : Cᵒᵖ ⥤ C is involutive when double dualization is naturally isomorphic to the identity by an isomorphism satisfying the triangle identity CategoryTheory.Functor.IsInvolutiveDual, which is strictly stronger than the bare existence of such an isomorphism. The linear dual on finite-dimensional vector spaces and finite dualization of finite locally free Hopf algebras are the motivating examples.

Turning such an F into an equivalence Cᵒᵖ ≌ C by CategoryTheory.Functor.asEquivalence loses the involutivity: the inverse produced there is an abstract quasi-inverse, so no theorem identifies it with F again. CategoryTheory.Functor.dualityEquivalence instead takes the double-dual isomorphism as input and returns an equivalence whose inverse is F.rightOp, so both directions and both structural isomorphisms compute.

Main declarations #

CategoryTheory.Functor.IsInvolutiveDual: the triangle identity a double-dual isomorphism must satisfy.
CategoryTheory.Functor.dualityEquivalence: the anti-equivalence attached to an involutive contravariant endofunctor, together with the computations of its functor, inverse, unit and counit in both directions.

source

@[reducible, inline]

abbrev CategoryTheory.Functor.IsInvolutiveDual {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ C) (ev : Functor.id C ≅ F.rightOp.comp F) :

Prop

The triangle identity for a double-dual isomorphism ev : 𝟭 C ≅ F.rightOp ⋙ F: dualizing ev.inv at X and then applying ev.inv at the dual of X is the identity.

Equations

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

Instances For

source

def CategoryTheory.Functor.dualityEquivalence {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ C) (ev : Functor.id C ≅ F.rightOp.comp F) (triangle : F.IsInvolutiveDual ev) :

Cᵒᵖ ≌ C

An involutive contravariant endofunctor is an anti-equivalence.

The inverse of the double-dual isomorphism ev plays the role of the counit, and the opposite of that inverse plays the role of the unit, so unlike CategoryTheory.Functor.asEquivalence the inverse of the resulting equivalence is F.rightOp: dualizing back is the same operation as dualizing.

The body is exposed because the unit and counit computations below are not merely proved by rfl: their statements only typecheck once unitIso and counitIso reduce.

Equations