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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.EnrichedCategory V Cᵒᵖ

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

Equations

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

theorem CategoryTheory.eComp_op_eq (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ) : CategoryTheory.eComp V z y x = CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.EnrichedCategory.Hom (Opposite.unop y) (Opposite.unop z)) (CategoryTheory.EnrichedCategory.Hom (Opposite.unop x) (Opposite.unop y))).hom (CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ) {Z : V} (h : CategoryTheory.EnrichedCategory.Hom z x ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h = CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.EnrichedCategory.Hom (Opposite.unop y) (Opposite.unop z)) (CategoryTheory.EnrichedCategory.Hom (Opposite.unop x) (Opposite.unop y))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h)

theorem CategoryTheory.tensorHom_eComp_op_eq (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ CategoryTheory.EnrichedCategory.Hom z y) (g : w ⟶ CategoryTheory.EnrichedCategory.Hom y x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.eComp V z y x) = CategoryTheory.CategoryStruct.comp (β_ v w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ CategoryTheory.EnrichedCategory.Hom z y) (g : w ⟶ CategoryTheory.EnrichedCategory.Hom y x) {Z : V} (h : CategoryTheory.EnrichedCategory.Hom z x ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h) = CategoryTheory.CategoryStruct.comp (β_ v w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h))

def CategoryTheory.forgetEnrichmentOppositeEquivalence.functor (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V Cᵒᵖ) (CategoryTheory.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.

Equations

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

def CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V C)ᵒᵖ (CategoryTheory.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ᵒᵖ.

Equations

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

def CategoryTheory.forgetEnrichmentOppositeEquivalence (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.ForgetEnrichment V Cᵒᵖ ≌ (CategoryTheory.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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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