The opposite category of an enriched category

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

structure CategoryTheory.eOpposite (V : Type u₁) (C : Type u) : Type u

The underlying type of the enriched opposite category.

This takes V as an argument so that, if C is enriched over multiple categories, the instances of the underlying categories on ForgetEnrichment C do not coincide

• as : C

def CategoryTheory.eOpposite.op {V : Type u₁} {C : Type u} (x : C) : CategoryTheory.eOpposite V C

Equations

• CategoryTheory.eOpposite.op x = { as := x }

def CategoryTheory.eOpposite.unop {V : Type u₁} {C : Type u} (x : CategoryTheory.eOpposite V C) : C

Equations

• x.unop = x.as

@[simp]

theorem CategoryTheory.eOpposite.op_of_unop (V : Type u₁) {C : Type u} (x : CategoryTheory.eOpposite V C) : CategoryTheory.eOpposite.op x.unop = x

@[simp]

theorem CategoryTheory.eOpposite.unop_of_op (V : Type u₁) {C : Type u} (x : C) : (CategoryTheory.eOpposite.op x).unop = x

def CategoryTheory.eOpposite.equivToEnrichedOpposite (V : Type u₁) (C : Type u) : C ≃ CategoryTheory.eOpposite V C

The type-level equivalence between a type and its enriched opposite.

Equations

• CategoryTheory.eOpposite.equivToEnrichedOpposite V C = { toFun := CategoryTheory.eOpposite.op, invFun := CategoryTheory.eOpposite.unop, left_inv := ⋯, right_inv := ⋯ }

instance CategoryTheory.eOpposite.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 (CategoryTheory.eOpposite V C)

The enriched category structure on eOpposite V C

Equations

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