The opposite category of an enriched category

When a monoidal category V is braided, we may define the opposite V-category of a V-category. The symmetry map is required to define the composition morphism.

This file constructs the opposite V-category as an instance on the type Cᵒᵖ and constructs an equivalence between

• ForgetEnrichment V (Cᵒᵖ), the underlying category of the V-category Cᵒᵖ; and
• (ForgetEnrichment V C)ᵒᵖ, the opposite category of the underlying category of C. We also show that if C is an enriched ordinary category (i.e. a category enriched in V equipped with an identification (X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y))) then Cᵒᵖ is again an enriched ordinary category.

instance CategoryTheory.EnrichedCategory.opposite (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : EnrichedCategory V Cᵒᵖ

For a V-category C, construct the opposite V-category structure on the type Cᵒᵖ using the braiding in V.

theorem CategoryTheory.eComp_op_eq (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u} [EnrichedCategory V C] (x y z : Cᵒᵖ) : eComp V z y x = CategoryStruct.comp (β_ (EnrichedCategory.Hom (Opposite.unop y) (Opposite.unop z)) (EnrichedCategory.Hom (Opposite.unop x) (Opposite.unop y))).hom (eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z))

Unfold the definition of composition in the enriched opposite category.

theorem CategoryTheory.eComp_op_eq_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u} [EnrichedCategory V C] (x y z : Cᵒᵖ) {Z : V} (h : EnrichedCategory.Hom z x ⟶ Z) : CategoryStruct.comp (eComp V z y x) h = CategoryStruct.comp (β_ (EnrichedCategory.Hom (Opposite.unop y) (Opposite.unop z)) (EnrichedCategory.Hom (Opposite.unop x) (Opposite.unop y))).hom (CategoryStruct.comp (eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h)

theorem CategoryTheory.tensorHom_eComp_op_eq (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u} [EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ EnrichedCategory.Hom z y) (g : w ⟶ EnrichedCategory.Hom y x) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (eComp V z y x) = CategoryStruct.comp (β_ v w).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g f) (eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)))

When composing a tensor product of morphisms with the V-composition morphism in Cᵒᵖ, this re-writes the V-composition to be in C and moves the braiding to the left.

theorem CategoryTheory.tensorHom_eComp_op_eq_assoc (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {C : Type u} [EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ EnrichedCategory.Hom z y) (g : w ⟶ EnrichedCategory.Hom y x) {Z : V} (h : EnrichedCategory.Hom z x ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (CategoryStruct.comp (eComp V z y x) h) = CategoryStruct.comp (β_ v w).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g f) (CategoryStruct.comp (eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h))

def CategoryTheory.forgetEnrichmentOppositeEquivalence.functor (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : Functor (ForgetEnrichment V Cᵒᵖ) (ForgetEnrichment V C)ᵒᵖ

The functor going from the underlying category of the enriched category Cᵒᵖ to the opposite of the underlying category of the enriched category C.

def CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : Functor (ForgetEnrichment V C)ᵒᵖ (ForgetEnrichment V Cᵒᵖ)

The functor going from the opposite of the underlying category of the enriched category C to the underlying category of the enriched category Cᵒᵖ.

def CategoryTheory.forgetEnrichmentOppositeEquivalence (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : ForgetEnrichment V Cᵒᵖ ≌ (ForgetEnrichment V C)ᵒᵖ

The equivalence between the underlying category of the enriched category Cᵒᵖ and the opposite of the underlying category of the enriched category C.

@[simp]

theorem CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : (forgetEnrichmentOppositeEquivalence V C).counitIso = NatIso.ofComponents (fun (x : (ForgetEnrichment V C)ᵒᵖ) => Iso.refl (((forgetEnrichmentOppositeEquivalence.inverse V C).comp (forgetEnrichmentOppositeEquivalence.functor V C)).obj x)) ⋯

@[simp]

theorem CategoryTheory.forgetEnrichmentOppositeEquivalence_inverse (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : (forgetEnrichmentOppositeEquivalence V C).inverse = forgetEnrichmentOppositeEquivalence.inverse V C

@[simp]

theorem CategoryTheory.forgetEnrichmentOppositeEquivalence_functor (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : (forgetEnrichmentOppositeEquivalence V C).functor = forgetEnrichmentOppositeEquivalence.functor V C

@[simp]

theorem CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] (C : Type u) [EnrichedCategory V C] : (forgetEnrichmentOppositeEquivalence V C).unitIso = NatIso.ofComponents (fun (x : ForgetEnrichment V Cᵒᵖ) => Iso.refl ((Functor.id (ForgetEnrichment V Cᵒᵖ)).obj x)) ⋯

instance CategoryTheory.EnrichedOrdinaryCategory.opposite (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] [BraidedCategory V] {D : Type u} [Category.{v, u} D] [EnrichedOrdinaryCategory V D] : EnrichedOrdinaryCategory V Dᵒᵖ

If D is an enriched ordinary category then Dᵒᵖ is an enriched ordinary category.