Opposite enriched functors

A functor between categories enriched in a braided monoidal category also acts on their opposites. Its map on the Hom object from op X to op Y is the original map from Y to X. Naturality of the braiding makes this map preserve opposite composition.

This applies in particular to differential graded functors: the braiding of cochain complexes supplies the Koszul sign in opposite composition, and the same chain maps define the opposite functor. The construction is useful when a left action is expressed as a right action of an opposite differential graded category.

References

• Mathlib.CategoryTheory.Enriched.Opposite, for the opposite enriched category.

def CategoryTheory.EnrichedFunctor.op {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u₂} {D : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] (F : EnrichedFunctor V C D) : EnrichedFunctor V Cᵒᵖ Dᵒᵖ

The opposite of an enriched functor, with the same map on each Hom object after reversing its source and target.

Equations

• F.op = { obj := fun (X : Cᵒᵖ) => Opposite.op (F.obj (Opposite.unop X)), map := fun (X Y : Cᵒᵖ) => F.map (Opposite.unop Y) (Opposite.unop X), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.EnrichedFunctor.op_obj {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u₂} {D : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : Cᵒᵖ) : F.op.obj X = Opposite.op (F.obj (Opposite.unop X))

The opposite functor acts on objects by applying the original functor.

@[simp]

theorem CategoryTheory.EnrichedFunctor.op_map {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u₂} {D : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X Y : Cᵒᵖ) : F.op.map X Y = F.map (Opposite.unop Y) (Opposite.unop X)

The opposite functor uses the original map on the reversed Hom object.

@[simp]

theorem CategoryTheory.EnrichedFunctor.op_id {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u₂} [EnrichedCategory V C] : (id V C).op = id V Cᵒᵖ

Taking opposites sends the identity enriched functor to the identity.

@[simp]

theorem CategoryTheory.EnrichedFunctor.op_comp {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u₂} {D : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] {E : Type u_1} [EnrichedCategory V E] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) : (comp V F G).op = comp V F.op G.op

Taking opposites preserves composition of enriched functors.