doc-next-gen

Mathlib.CategoryTheory.Opposites

Module docstring

{"# Opposite categories

We provide a category instance on Cᵒᵖ. The morphisms X ⟶ Y are defined to be the morphisms unop Y ⟶ unop X in C.

Here Cᵒᵖ is an irreducible typeclass synonym for C (it is the same one used in the algebra library).

We also provide various mechanisms for constructing opposite morphisms, functors, and natural transformations.

Unfortunately, because we do not have a definitional equality op (op X) = X, there are quite a few variations that are needed in practice. "}

Quiver.Hom.op_inj theorem
{X Y : C} : Function.Injective (Quiver.Hom.op : (X ⟶ Y) → (Opposite.op Y ⟶ Opposite.op X))
Full source 
theorem Quiver.Hom.op_inj {X Y : C} :
    Function.Injective (Quiver.Hom.op : (X ⟶ Y) → (Opposite.opOpposite.op Y ⟶ Opposite.op X)) := fun _ _ H =>
  congr_arg Quiver.Hom.unop H
Injectivity of the Opposite Morphism Construction
Informal description
For any objects $X$ and $Y$ in a category $C$, the operation that takes a morphism $f : X \to Y$ to its opposite morphism $f^{\mathrm{op}} : Y^{\mathrm{op}} \to X^{\mathrm{op}}$ is injective. In other words, if $f^{\mathrm{op}} = g^{\mathrm{op}}$, then $f = g$.
Quiver.Hom.unop_inj theorem
{X Y : Cᵒᵖ} : Function.Injective (Quiver.Hom.unop : (X ⟶ Y) → (Opposite.unop Y ⟶ Opposite.unop X))
Full source 
theorem Quiver.Hom.unop_inj {X Y : Cᵒᵖ} :
    Function.Injective (Quiver.Hom.unop : (X ⟶ Y) → (Opposite.unopOpposite.unop Y ⟶ Opposite.unop X)) :=
  fun _ _ H => congr_arg Quiver.Hom.op H
Injectivity of Morphism Unop in Opposite Category
Informal description
For any objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$, the function that takes a morphism $f : X \to Y$ in $C^{\mathrm{op}}$ to its underlying morphism $\mathrm{unop}(f) : \mathrm{unop}(Y) \to \mathrm{unop}(X)$ in $C$ is injective.
Quiver.Hom.unop_op theorem
{X Y : C} (f : X ⟶ Y) : f.op.unop = f
Full source 
@[simp]
theorem Quiver.Hom.unop_op {X Y : C} (f : X ⟶ Y) : f.op.unop = f :=
  rfl
Opposite-Unopposite Morphism Identity: $(f^{\mathrm{op}})^{\mathrm{unop}} = f$
Informal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, the operation of first taking the opposite morphism $f^{\mathrm{op}}$ and then taking its unopposite $(f^{\mathrm{op}})^{\mathrm{unop}}$ returns the original morphism $f$.
Quiver.Hom.unop_op' theorem
{X Y : Cᵒᵖ} {x} : @Quiver.Hom.unop C _ X Y no_index (Opposite.op (unop := x)) = x
Full source 
@[simp]
theorem Quiver.Hom.unop_op' {X Y : Cᵒᵖ} {x} :
    @Quiver.Hom.unop C _ X Y no_index (Opposite.op (unop := x)) = x := rfl
Inverse property of opposite morphisms: $\mathrm{unop}(\mathrm{op}(x)) = x$
Informal description
For any objects $X, Y$ in the opposite category $C^{\mathrm{op}}$ and any morphism $x \colon \mathrm{unop}\, Y \to \mathrm{unop}\, X$ in $C$, we have $\mathrm{unop}(\mathrm{op}(x)) = x$.
Quiver.Hom.op_unop theorem
{X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f
Full source 
@[simp]
theorem Quiver.Hom.op_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f :=
  rfl
Opposite-unopposite roundtrip for morphisms
Informal description
For any morphism $f \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, the operation of first taking the underlying morphism in $C$ (via `unop`) and then taking its opposite (via `op`) returns the original morphism $f$.
Quiver.Hom.unop_mk theorem
{X Y : Cᵒᵖ} (f : X ⟶ Y) : Quiver.Hom.unop { unop := f } = f
Full source 
@[simp] theorem Quiver.Hom.unop_mk {X Y : Cᵒᵖ} (f : X ⟶ Y) : Quiver.Hom.unop {unop := f} = f := rfl
Unop construction preserves morphisms in opposite category
Informal description
For any morphism $f \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, the operation of taking the underlying morphism in $C$ (via `unop`) of the constructed morphism `{ unop := f }` returns the original morphism $f$.
CategoryTheory.Category.opposite instance
: Category.{v₁} Cᵒᵖ
Full source 
/-- The opposite category. -/
@[stacks 001M]
instance Category.opposite : Category.{v₁} Cᵒᵖ where
  comp f g := (g.unop ≫ f.unop).op
  id X := (𝟙 (unop X)).op
The Opposite Category Construction
Informal description
The opposite category $C^{\mathrm{op}}$ of a category $C$ is a category where the objects are the same as in $C$, and the morphisms $X \to Y$ in $C^{\mathrm{op}}$ are defined to be the morphisms $Y \to X$ in $C$. Composition of morphisms in $C^{\mathrm{op}}$ is given by reversing the order of composition in $C$.
CategoryTheory.op_comp theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).op = g.op ≫ f.op
Full source 
@[simp, reassoc]
theorem op_comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).op = g.op ≫ f.op :=
  rfl
Opposite of Composition in a Category Equals Reversed Composition of Opposites
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category $C$, the opposite of their composition $(f \circ g)^{\mathrm{op}}$ in the opposite category $C^{\mathrm{op}}$ is equal to the composition of their opposites in reversed order, i.e., $g^{\mathrm{op}} \circ f^{\mathrm{op}}$.
CategoryTheory.op_id theorem
{X : C} : (𝟙 X).op = 𝟙 (op X)
Full source 
@[simp]
theorem op_id {X : C} : (𝟙 X).op = 𝟙 (op X) :=
  rfl
Opposite of Identity Morphism Equals Identity on Opposite Object
Informal description
For any object $X$ in a category $C$, the opposite of the identity morphism on $X$ is equal to the identity morphism on the opposite object $\mathrm{op}(X)$, i.e., $(\mathrm{id}_X)^{\mathrm{op}} = \mathrm{id}_{\mathrm{op}(X)}$.
CategoryTheory.unop_comp theorem
{X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).unop = g.unop ≫ f.unop
Full source 
@[simp, reassoc]
theorem unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).unop = g.unop ≫ f.unop :=
  rfl
Composition in Opposite Category Unfolds to Reverse Composition in Original Category
Informal description
For any objects $X, Y, Z$ in the opposite category $C^{\mathrm{op}}$ and morphisms $f: X \to Y$ and $g: Y \to Z$ in $C^{\mathrm{op}}$, the unoperation of the composition $f \circ g$ equals the composition of the unoperations of $g$ and $f$ in the original category $C$, i.e., $(f \circ g)^{\mathrm{unop}} = g^{\mathrm{unop}} \circ f^{\mathrm{unop}}$.
CategoryTheory.unop_id theorem
{X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X)
Full source 
@[simp]
theorem unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) :=
  rfl
Identity Morphism Preservation under Unopposite
Informal description
For any object $X$ in the opposite category $C^{\mathrm{op}}$, the unopposite of the identity morphism on $X$ is equal to the identity morphism on the unopposite of $X$, i.e., $(𝟙_X)^{\mathrm{unop}} = 𝟙_{X^{\mathrm{unop}}}$.
CategoryTheory.unop_id_op theorem
{X : C} : (𝟙 (op X)).unop = 𝟙 X
Full source 
@[simp]
theorem unop_id_op {X : C} : (𝟙 (op X)).unop = 𝟙 X :=
  rfl
Identity Morphism Preservation under Opposite and Unopposite Operations
Informal description
For any object $X$ in a category $C$, the unopposite of the identity morphism on the opposite object $\mathrm{op}(X)$ is equal to the identity morphism on $X$, i.e., $\mathrm{unop}(1_{\mathrm{op}(X)}) = 1_X$.
CategoryTheory.op_id_unop theorem
{X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X
Full source 
@[simp]
theorem op_id_unop {X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X :=
  rfl
Opposite of Identity in Underlying Category Equals Identity in Opposite Category
Informal description
For any object $X$ in the opposite category $C^{\mathrm{op}}$, the opposite of the identity morphism on the underlying object $\mathrm{unop}\,X$ in $C$ is equal to the identity morphism on $X$ in $C^{\mathrm{op}}$. That is, $(𝟙 (\mathrm{unop}\,X))^{\mathrm{op}} = 𝟙 X$.
CategoryTheory.unopUnop definition
: Cᵒᵖᵒᵖ ⥤ C
Full source 
/-- The functor from the double-opposite of a category to the underlying category. -/
@[simps]
def unopUnop : CᵒᵖCᵒᵖᵒᵖCᵒᵖᵒᵖ ⥤ C where
  obj X := unop (unop X)
  map f := f.unop.unop
Double opposite category functor
Informal description
The functor from the double-opposite category $C^{\mathrm{op}\mathrm{op}}$ to the original category $C$ maps each object $X$ to $\mathrm{unop}(\mathrm{unop}(X))$ and each morphism $f$ to $\mathrm{unop}(\mathrm{unop}(f))$.
CategoryTheory.opOp definition
: C ⥤ Cᵒᵖᵒᵖ
Full source 
/-- The functor from a category to its double-opposite. -/
@[simps]
def opOp : C ⥤ Cᵒᵖᵒᵖ where
  obj X := op (op X)
  map f := f.op.op
Double opposite functor
Informal description
The functor from a category $C$ to its double opposite category $C^{\mathrm{op}\mathrm{op}}$, which maps each object $X$ to $\mathrm{op}(\mathrm{op}(X))$ and each morphism $f$ to $\mathrm{op}(\mathrm{op}(f))$.
CategoryTheory.opOpEquivalence definition
: Cᵒᵖᵒᵖ ≌ C
Full source 
/-- The double opposite category is equivalent to the original. -/
@[simps]
def opOpEquivalence : CᵒᵖCᵒᵖᵒᵖCᵒᵖᵒᵖ ≌ C where
  functor := unopUnop C
  inverse := opOp C
  unitIso := Iso.refl (𝟭 Cᵒᵖᵒᵖ)
  counitIso := Iso.refl (opOp C ⋙ unopUnop C)
Equivalence between a category and its double opposite
Informal description
The equivalence of categories between a category $C$ and its double opposite category $C^{\mathrm{op}\mathrm{op}}$, where: - The functor from $C^{\mathrm{op}\mathrm{op}}$ to $C$ is given by applying the `unop` operation twice, - The inverse functor from $C$ to $C^{\mathrm{op}\mathrm{op}}$ is given by applying the `op` operation twice, - The unit isomorphism is the identity natural isomorphism on the identity functor of $C^{\mathrm{op}\mathrm{op}}$, - The counit isomorphism is the identity natural isomorphism on the composition of the `opOp` and `unopUnop` functors.
CategoryTheory.instIsEquivalenceOppositeOpOp instance
: (opOp C).IsEquivalence
Full source 
instance : (opOp C).IsEquivalence :=
  (opOpEquivalence C).isEquivalence_inverse
Double Opposite Functor is an Equivalence
Informal description
The functor from a category $C$ to its double opposite category $C^{\mathrm{op}\mathrm{op}}$ is an equivalence of categories. This means that the double opposite construction preserves the essential structure of the original category, including objects, morphisms, and their compositions up to isomorphism.
CategoryTheory.instIsEquivalenceOppositeUnopUnop instance
: (unopUnop C).IsEquivalence
Full source 
instance : (unopUnop C).IsEquivalence :=
  (opOpEquivalence C).isEquivalence_functor
Double Opposite Functor is an Equivalence
Informal description
The functor from the double opposite category $C^{\mathrm{op}\mathrm{op}}$ to the original category $C$ is an equivalence of categories.
CategoryTheory.isIso_op instance
{X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso f.op
Full source 
/-- If `f` is an isomorphism, so is `f.op` -/
instance isIso_op {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso f.op :=
  ⟨⟨(inv f).op, ⟨Quiver.Hom.unop_inj (by simp), Quiver.Hom.unop_inj (by simp)⟩⟩⟩
Opposite of an Isomorphism is an Isomorphism
Informal description
For any morphism $f : X \to Y$ in a category $C$, if $f$ is an isomorphism, then its opposite morphism $f^{\mathrm{op}} : Y^{\mathrm{op}} \to X^{\mathrm{op}}$ in the opposite category $C^{\mathrm{op}}$ is also an isomorphism.
CategoryTheory.isIso_of_op theorem
{X Y : C} (f : X ⟶ Y) [IsIso f.op] : IsIso f
Full source 
/-- If `f.op` is an isomorphism `f` must be too.
(This cannot be an instance as it would immediately loop!)
-/
theorem isIso_of_op {X Y : C} (f : X ⟶ Y) [IsIso f.op] : IsIso f :=
  ⟨⟨(inv f.op).unop, ⟨Quiver.Hom.op_inj (by simp), Quiver.Hom.op_inj (by simp)⟩⟩⟩
Isomorphism in Original Category from Opposite Category Isomorphism
Informal description
For any morphism $f : X \to Y$ in a category $C$, if the opposite morphism $f^{\mathrm{op}} : Y^{\mathrm{op}} \to X^{\mathrm{op}}$ is an isomorphism in the opposite category $C^{\mathrm{op}}$, then $f$ is also an isomorphism in $C$.
CategoryTheory.isIso_op_iff theorem
{X Y : C} (f : X ⟶ Y) : IsIso f.op ↔ IsIso f
Full source 
theorem isIso_op_iff {X Y : C} (f : X ⟶ Y) : IsIsoIsIso f.op ↔ IsIso f :=
  ⟨fun _ => isIso_of_op _, fun _ => inferInstance⟩
Isomorphism Equivalence Between a Category and Its Opposite
Informal description
For any morphism $f : X \to Y$ in a category $C$, the opposite morphism $f^{\mathrm{op}} : Y^{\mathrm{op}} \to X^{\mathrm{op}}$ is an isomorphism in the opposite category $C^{\mathrm{op}}$ if and only if $f$ is an isomorphism in $C$.
CategoryTheory.isIso_unop_iff theorem
{X Y : Cᵒᵖ} (f : X ⟶ Y) : IsIso f.unop ↔ IsIso f
Full source 
theorem isIso_unop_iff {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsIsoIsIso f.unop ↔ IsIso f := by
  rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]
Isomorphism Equivalence Between Opposite and Original Categories: $f^{\mathrm{unop}}$ is iso iff $f$ is iso
Informal description
For any morphism $f \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, the underlying morphism $f^{\mathrm{unop}} \colon Y \to X$ in $C$ is an isomorphism if and only if $f$ is an isomorphism in $C^{\mathrm{op}}$.
CategoryTheory.isIso_unop instance
{X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : IsIso f.unop
Full source 
instance isIso_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : IsIso f.unop :=
  (isIso_unop_iff _).2 inferInstance
Isomorphism in Opposite Category Implies Isomorphism in Original Category
Informal description
For any morphism $f \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, if $f$ is an isomorphism in $C^{\mathrm{op}}$, then the underlying morphism $f^{\mathrm{unop}} \colon Y \to X$ in $C$ is also an isomorphism.
CategoryTheory.op_inv theorem
{X Y : C} (f : X ⟶ Y) [IsIso f] : (inv f).op = inv f.op
Full source 
@[simp]
theorem op_inv {X Y : C} (f : X ⟶ Y) [IsIso f] : (inv f).op = inv f.op := by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← op_comp, IsIso.inv_hom_id, op_id]
Opposite of Inverse Equals Inverse of Opposite: $(f^{-1})^{\mathrm{op}} = (f^{\mathrm{op}})^{-1}$
Informal description
For any isomorphism $f \colon X \to Y$ in a category $C$, the opposite of its inverse $(f^{-1})^{\mathrm{op}}$ is equal to the inverse of its opposite morphism $(f^{\mathrm{op}})^{-1}$ in the opposite category $C^{\mathrm{op}}$.
CategoryTheory.unop_inv theorem
{X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : (inv f).unop = inv f.unop
Full source 
@[simp]
theorem unop_inv {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : (inv f).unop = inv f.unop := by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← unop_comp, IsIso.inv_hom_id, unop_id]
Unopposite of Inverse Equals Inverse of Unopposite: $(f^{-1})^{\mathrm{unop}} = (f^{\mathrm{unop}})^{-1}$
Informal description
For any isomorphism $f \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, the unopposite of the inverse morphism $(f^{-1})^{\mathrm{unop}}$ is equal to the inverse of the unopposite morphism $(f^{\mathrm{unop}})^{-1}$ in the original category $C$.
CategoryTheory.Functor.op definition
(F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ
Full source 
/-- The opposite of a functor, i.e. considering a functor `F : C ⥤ D` as a functor `Cᵒᵖ ⥤ Dᵒᵖ`.
In informal mathematics no distinction is made between these. -/
@[simps]
protected def op (F : C ⥤ D) : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ where
  obj X := op (F.obj (unop X))
  map f := (F.map f.unop).op
Opposite functor
Informal description
The opposite functor of a given functor $F \colon C \to D$ is a functor $F^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$ defined by: - On objects: $F^{\mathrm{op}}(X) = F(X)^{\mathrm{op}}$ for any object $X$ in $C^{\mathrm{op}}$. - On morphisms: For a morphism $f \colon X \to Y$ in $C^{\mathrm{op}}$ (which is a morphism $Y \to X$ in $C$), the morphism $F^{\mathrm{op}}(f)$ is $F(f)^{\mathrm{op}}$, i.e., the morphism $F(Y) \to F(X)$ in $D$ considered as a morphism $F(X)^{\mathrm{op}} \to F(Y)^{\mathrm{op}}$ in $D^{\mathrm{op}}$.
CategoryTheory.Functor.unop definition
(F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D
Full source 
/-- Given a functor `F : Cᵒᵖ ⥤ Dᵒᵖ` we can take the "unopposite" functor `F : C ⥤ D`.
In informal mathematics no distinction is made between these.
-/
@[simps]
protected def unop (F : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D where
  obj X := unop (F.obj (op X))
  map f := (F.map f.op).unop
Unopposite functor
Informal description
Given a functor $F : C^{\mathrm{op}} \to D^{\mathrm{op}}$, the unopposite functor $F : C \to D$ is defined by: - On objects: $F(X) = \mathrm{unop}(F(\mathrm{op}(X)))$ for any object $X$ in $C$. - On morphisms: For any morphism $f : X \to Y$ in $C$, $F(f) = \mathrm{unop}(F(f^{\mathrm{op}}))$. This construction allows us to treat a functor between opposite categories as a functor between the original categories.
CategoryTheory.Functor.opUnopIso definition
(F : C ⥤ D) : F.op.unop ≅ F
Full source 
/-- The isomorphism between `F.op.unop` and `F`. -/
@[simps!]
def opUnopIso (F : C ⥤ D) : F.op.unop ≅ F :=
  NatIso.ofComponents fun _ => Iso.refl _
Isomorphism between opposite-unopposite functor and original functor
Informal description
The natural isomorphism between the functor obtained by first taking the opposite of $F$ and then its unopposite, and the original functor $F \colon C \to D$. For each object $X$ in $C$, the component of this isomorphism at $X$ is the identity isomorphism $\text{id}_{F(X)}$.
CategoryTheory.Functor.unopOpIso definition
(F : Cᵒᵖ ⥤ Dᵒᵖ) : F.unop.op ≅ F
Full source 
/-- The isomorphism between `F.unop.op` and `F`. -/
@[simps!]
def unopOpIso (F : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ) : F.unop.op ≅ F :=
  NatIso.ofComponents fun _ => Iso.refl _
Isomorphism between unopposite-opposite functor and original functor
Informal description
The natural isomorphism between the functor obtained by first taking the unopposite of $F$ and then its opposite, and the original functor $F \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$. For each object $X$ in $C^{\mathrm{op}}$, the component of this isomorphism at $X$ is the identity isomorphism $\text{id}_{F(X)}$.
CategoryTheory.Functor.opHom definition
: (C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ
Full source 
/-- Taking the opposite of a functor is functorial.
-/
@[simps]
def opHom : (C ⥤ D)ᵒᵖ(C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ where
  obj F := (unop F).op
  map α :=
    { app := fun X => (α.unop.app (unop X)).op
      naturality := fun _ _ f => Quiver.Hom.unop_inj (α.unop.naturality f.unop).symm }
Opposite functor construction
Informal description
The functor that takes an opposite functor $F^{\mathrm{op}}$ (where $F \colon C \to D$) and constructs the opposite functor $(F^{\mathrm{op}})^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$. Explicitly: - On objects: For an object $X$ in $C^{\mathrm{op}}$, $(F^{\mathrm{op}})^{\mathrm{op}}(X) = F(X)^{\mathrm{op}}$ in $D^{\mathrm{op}}$. - On morphisms: For a morphism $f \colon X \to Y$ in $C^{\mathrm{op}}$ (which is $Y \to X$ in $C$), the morphism $(F^{\mathrm{op}})^{\mathrm{op}}(f)$ is $F(f)^{\mathrm{op}}$, i.e., the morphism $F(Y) \to F(X)$ in $D$ considered as $F(X)^{\mathrm{op}} \to F(Y)^{\mathrm{op}}$ in $D^{\mathrm{op}}$.
CategoryTheory.Functor.opInv definition
: (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ
Full source 
/-- Take the "unopposite" of a functor is functorial.
-/
@[simps]
def opInv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ where
  obj F := op F.unop
  map α :=
    Quiver.Hom.op
      { app := fun X => (α.app (op X)).unop
        naturality := fun _ _ f => Quiver.Hom.op_inj <| (α.naturality f.op).symm }
Opposite functor involution
Informal description
The functor that takes a functor $F \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$ and constructs its opposite functor $F^{\mathrm{op}} \colon C \to D$ in the opposite category of functors $(C \to D)^{\mathrm{op}}$. Explicitly: - On objects: For a functor $F \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$, the object $\mathrm{opInv}(F)$ is the opposite functor $F^{\mathrm{op}}$ in $(C \to D)^{\mathrm{op}}$. - On morphisms: For a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$, the morphism $\mathrm{opInv}(\alpha)$ is the opposite natural transformation $\alpha^{\mathrm{op}} \colon G^{\mathrm{op}} \to F^{\mathrm{op}}$ in $(C \to D)^{\mathrm{op}}$, where for each object $X$ in $C$, $\alpha^{\mathrm{op}}_X$ is the opposite morphism of $\alpha_{\mathrm{op}(X)}$ in $D$.
CategoryTheory.Functor.leftOp definition
(F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D
Full source 
/--
Another variant of the opposite of functor, turning a functor `C ⥤ Dᵒᵖ` into a functor `Cᵒᵖ ⥤ D`.
In informal mathematics no distinction is made.
-/
@[simps]
protected def leftOp (F : C ⥤ Dᵒᵖ) : CᵒᵖCᵒᵖ ⥤ D where
  obj X := unop (F.obj (unop X))
  map f := (F.map f.unop).unop
Left opposite functor construction
Informal description
Given a functor $F \colon C \to D^{\mathrm{op}}$, the functor $\mathrm{leftOp}(F) \colon C^{\mathrm{op}} \to D$ is defined by: - On objects: $\mathrm{leftOp}(F)(X) = \mathrm{unop}(F(\mathrm{unop}(X)))$ for $X \in C^{\mathrm{op}}$ - On morphisms: $\mathrm{leftOp}(F)(f) = \mathrm{unop}(F(\mathrm{unop}(f)))$ for $f \colon X \to Y$ in $C^{\mathrm{op}}$ This construction converts a functor from $C$ to the opposite category of $D$ into a functor from the opposite category of $C$ to $D$.
CategoryTheory.Functor.rightOp definition
(F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ
Full source 
/--
Another variant of the opposite of functor, turning a functor `Cᵒᵖ ⥤ D` into a functor `C ⥤ Dᵒᵖ`.
In informal mathematics no distinction is made.
-/
@[simps]
protected def rightOp (F : CᵒᵖCᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ where
  obj X := op (F.obj (op X))
  map f := (F.map f.op).op
Right opposite functor
Informal description
Given a functor $F \colon C^{\mathrm{op}} \to D$, the functor $\mathrm{rightOp}(F) \colon C \to D^{\mathrm{op}}$ is defined by: - On objects: $\mathrm{rightOp}(F)(X) = \mathrm{op}(F(\mathrm{op}(X)))$ - On morphisms: $\mathrm{rightOp}(F)(f) = \mathrm{op}(F(f^{\mathrm{op}}))$ This construction converts a contravariant functor from $C$ to $D$ into a covariant functor from $C$ to the opposite category of $D$.
CategoryTheory.Functor.rightOp_map_unop theorem
{F : Cᵒᵖ ⥤ D} {X Y} (f : X ⟶ Y) : (F.rightOp.map f).unop = F.map f.op
Full source 
lemma rightOp_map_unop {F : CᵒᵖCᵒᵖ ⥤ D} {X Y} (f : X ⟶ Y) :
    (F.rightOp.map f).unop = F.map f.op := rfl
Unopposite of Right Opposite Functor's Map Equals Original Functor's Map of Opposite Morphism
Informal description
For any functor $F \colon C^{\mathrm{op}} \to D$ and any morphism $f \colon X \to Y$ in $C$, the unopposite of the morphism $\mathrm{rightOp}(F)(f)$ in $D^{\mathrm{op}}$ equals the image under $F$ of the opposite morphism $f^{\mathrm{op}}$ in $C^{\mathrm{op}}$. In other words, $(\mathrm{rightOp}(F)(f))^{\mathrm{unop}} = F(f^{\mathrm{op}})$.
CategoryTheory.Functor.instFullOppositeOp instance
{F : C ⥤ D} [Full F] : Full F.op
Full source 
instance {F : C ⥤ D} [Full F] : Full F.op where
  map_surjective f := ⟨(F.preimage f.unop).op, by simp⟩
Opposite Functor Preserves Fullness
Informal description
For any functor $F \colon C \to D$ that is full, the opposite functor $F^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$ is also full. This means that for any objects $X, Y$ in $C^{\mathrm{op}}$ and any morphism $g \colon F^{\mathrm{op}}(X) \to F^{\mathrm{op}}(Y)$ in $D^{\mathrm{op}}$, there exists a morphism $f \colon X \to Y$ in $C^{\mathrm{op}}$ such that $F^{\mathrm{op}}(f) = g$.
CategoryTheory.Functor.instFaithfulOppositeOp instance
{F : C ⥤ D} [Faithful F] : Faithful F.op
Full source 
instance {F : C ⥤ D} [Faithful F] : Faithful F.op where
  map_injective h := Quiver.Hom.unop_inj <| by simpa using map_injective F (Quiver.Hom.op_inj h)
Opposite Functor Preserves Faithfulness
Informal description
For any faithful functor $F \colon C \to D$, the opposite functor $F^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$ is also faithful.
CategoryTheory.Functor.rightOp_faithful instance
{F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp
Full source 
/-- If F is faithful then the right_op of F is also faithful. -/
instance rightOp_faithful {F : CᵒᵖCᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp where
  map_injective h := Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h))
Faithfulness Preservation under Right Opposite Functor Construction
Informal description
For any faithful functor $F \colon C^{\mathrm{op}} \to D$, the right opposite functor $F.\mathrm{rightOp} \colon C \to D^{\mathrm{op}}$ is also faithful.
CategoryTheory.Functor.leftOp_faithful instance
{F : C ⥤ Dᵒᵖ} [Faithful F] : Faithful F.leftOp
Full source 
/-- If F is faithful then the left_op of F is also faithful. -/
instance leftOp_faithful {F : C ⥤ Dᵒᵖ} [Faithful F] : Faithful F.leftOp where
  map_injective h := Quiver.Hom.unop_inj (map_injective F (Quiver.Hom.unop_inj h))
Faithfulness Preservation under Left Opposite Functor Construction
Informal description
For any faithful functor $F \colon C \to D^{\mathrm{op}}$, the left opposite functor $F.\mathrm{leftOp} \colon C^{\mathrm{op}} \to D$ is also faithful.
CategoryTheory.Functor.rightOp_full instance
{F : Cᵒᵖ ⥤ D} [Full F] : Full F.rightOp
Full source 
instance rightOp_full {F : CᵒᵖCᵒᵖ ⥤ D} [Full F] : Full F.rightOp where
  map_surjective f := ⟨(F.preimage f.unop).unop, by simp⟩
Fullness Preservation under Right Opposite Functor Construction
Informal description
For any full functor $F \colon C^{\mathrm{op}} \to D$, the right opposite functor $F.\mathrm{rightOp} \colon C \to D^{\mathrm{op}}$ is also full.
CategoryTheory.Functor.leftOp_full instance
{F : C ⥤ Dᵒᵖ} [Full F] : Full F.leftOp
Full source 
instance leftOp_full {F : C ⥤ Dᵒᵖ} [Full F] : Full F.leftOp where
  map_surjective f := ⟨(F.preimage f.op).op, by simp⟩
Fullness Preservation under Left Opposite Functor Construction
Informal description
For any functor $F \colon C \to D^{\mathrm{op}}$ that is full, the left opposite functor $F.\mathrm{leftOp} \colon C^{\mathrm{op}} \to D$ is also full.
CategoryTheory.Functor.leftOpRightOpIso definition
(F : C ⥤ Dᵒᵖ) : F.leftOp.rightOp ≅ F
Full source 
/-- The isomorphism between `F.leftOp.rightOp` and `F`. -/
@[simps!]
def leftOpRightOpIso (F : C ⥤ Dᵒᵖ) : F.leftOp.rightOp ≅ F :=
  NatIso.ofComponents fun _ => Iso.refl _
Isomorphism between double opposite functor and original functor
Informal description
The natural isomorphism between the functor obtained by first applying the left opposite construction and then the right opposite construction to a functor $F \colon C \to D^{\mathrm{op}}$, and the original functor $F$. For each object $X$ in $C$, the isomorphism is given by the identity isomorphism on $F(X)$.
CategoryTheory.Functor.rightOpLeftOpIso definition
(F : Cᵒᵖ ⥤ D) : F.rightOp.leftOp ≅ F
Full source 
/-- The isomorphism between `F.rightOp.leftOp` and `F`. -/
@[simps!]
def rightOpLeftOpIso (F : CᵒᵖCᵒᵖ ⥤ D) : F.rightOp.leftOp ≅ F :=
  NatIso.ofComponents fun _ => Iso.refl _
Isomorphism between double opposite functor and original functor
Informal description
The isomorphism between the functor obtained by first applying the right opposite construction and then the left opposite construction to a functor $F \colon C^{\mathrm{op}} \to D$, and the original functor $F$. For each object $X$ in $C^{\mathrm{op}}$, the isomorphism is given by the identity isomorphism on $F(X)$.
CategoryTheory.Functor.rightOp_leftOp_eq theorem
(F : Cᵒᵖ ⥤ D) : F.rightOp.leftOp = F
Full source 
/-- Whenever possible, it is advisable to use the isomorphism `rightOpLeftOpIso`
instead of this equality of functors. -/
theorem rightOp_leftOp_eq (F : CᵒᵖCᵒᵖ ⥤ D) : F.rightOp.leftOp = F := by
  cases F
  rfl
Equality of Double Opposite Functor Construction: $\mathrm{leftOp} \circ \mathrm{rightOp} = \mathrm{id}$
Informal description
For any functor $F \colon C^{\mathrm{op}} \to D$, the composition of the right opposite and left opposite constructions yields the original functor, i.e., $\mathrm{leftOp}(\mathrm{rightOp}(F)) = F$.
CategoryTheory.NatTrans.op definition
(α : F ⟶ G) : G.op ⟶ F.op
Full source 
/-- The opposite of a natural transformation. -/
@[simps]
protected def op (α : F ⟶ G) : G.op ⟶ F.op where
  app X := (α.app (unop X)).op
  naturality X Y f := Quiver.Hom.unop_inj (by simp)
Opposite natural transformation
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to D$, the opposite natural transformation $\alpha^{\mathrm{op}} \colon G^{\mathrm{op}} \to F^{\mathrm{op}}$ is defined as follows: - For each object $X$ in $C^{\mathrm{op}}$, the component $(\alpha^{\mathrm{op}})_X$ is the morphism $(\alpha_{\mathrm{unop}\, X})^{\mathrm{op}}$, where $\alpha_{\mathrm{unop}\, X}$ is the component of $\alpha$ at $\mathrm{unop}\, X$ in $C$. - The naturality condition is satisfied by construction.
CategoryTheory.NatTrans.op_id theorem
(F : C ⥤ D) : NatTrans.op (𝟙 F) = 𝟙 F.op
Full source 
@[simp]
theorem op_id (F : C ⥤ D) : NatTrans.op (𝟙 F) = 𝟙 F.op :=
  rfl
Identity Natural Transformation Preserved Under Opposite
Informal description
For any functor $F \colon C \to D$, the opposite of the identity natural transformation on $F$ is equal to the identity natural transformation on the opposite functor $F^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$. In symbols, $\mathrm{op}(1_F) = 1_{F^{\mathrm{op}}}$.
CategoryTheory.NatTrans.unop definition
{F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop
Full source 
/-- The "unopposite" of a natural transformation. -/
@[simps]
protected def unop {F G : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop where
  app X := (α.app (op X)).unop
  naturality X Y f := Quiver.Hom.op_inj (by simp)
Unopposite natural transformation
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$, the unopposite natural transformation $\alpha^{\mathrm{unop}} \colon G^{\mathrm{unop}} \to F^{\mathrm{unop}}$ is defined by: - For each object $X$ in $C$, the component $(\alpha^{\mathrm{unop}})_X$ is the morphism $(\alpha_{\mathrm{op}\, X})^{\mathrm{unop}}$, where $\alpha_{\mathrm{op}\, X}$ is the component of $\alpha$ at $\mathrm{op}\, X$ in $C^{\mathrm{op}}$. - The naturality condition is satisfied by construction.
CategoryTheory.NatTrans.unop_id theorem
(F : Cᵒᵖ ⥤ Dᵒᵖ) : NatTrans.unop (𝟙 F) = 𝟙 F.unop
Full source 
@[simp]
theorem unop_id (F : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ) : NatTrans.unop (𝟙 F) = 𝟙 F.unop :=
  rfl
Identity Natural Transformation Preserved Under Unopposite
Informal description
For any functor $F \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$, the unopposite of the identity natural transformation on $F$ is equal to the identity natural transformation on the unopposite functor $F^{\mathrm{unop}} \colon C \to D$. In symbols, $\mathrm{unop}(1_F) = 1_{F^{\mathrm{unop}}}$.
CategoryTheory.NatTrans.removeOp definition
(α : F.op ⟶ G.op) : G ⟶ F
Full source 
/-- Given a natural transformation `α : F.op ⟶ G.op`,
we can take the "unopposite" of each component obtaining a natural transformation `G ⟶ F`.
-/
@[simps]
protected def removeOp (α : F.op ⟶ G.op) : G ⟶ F where
  app X := (α.app (op X)).unop
  naturality X Y f :=
    Quiver.Hom.op_inj <| by simpa only [Functor.op_map] using (α.naturality f.op).symm
Unopposite of a natural transformation between opposite functors
Informal description
Given a natural transformation $\alpha \colon F^{\mathrm{op}} \longrightarrow G^{\mathrm{op}}$ between opposite functors, this constructs a natural transformation $G \longrightarrow F$ by taking the unopposite of each component of $\alpha$. Specifically, for each object $X$ in $C$, the component at $X$ is given by $(\alpha_{\mathrm{op}(X)})^{\mathrm{unop}}$.
CategoryTheory.NatTrans.removeOp_id theorem
(F : C ⥤ D) : NatTrans.removeOp (𝟙 F.op) = 𝟙 F
Full source 
@[simp]
theorem removeOp_id (F : C ⥤ D) : NatTrans.removeOp (𝟙 F.op) = 𝟙 F :=
  rfl
Identity Natural Transformation Preserved Under Remove-Opposite Operation
Informal description
For any functor $F \colon C \to D$, the operation of removing the opposite from the identity natural transformation on the opposite functor $F^{\mathrm{op}}$ yields the identity natural transformation on $F$. In symbols, $\mathrm{removeOp}(1_{F^{\mathrm{op}}}) = 1_F$.
CategoryTheory.NatTrans.removeUnop definition
{F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) : G ⟶ F
Full source 
/-- Given a natural transformation `α : F.unop ⟶ G.unop`, we can take the opposite of each
component obtaining a natural transformation `G ⟶ F`. -/
@[simps]
protected def removeUnop {F G : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) : G ⟶ F where
  app X := (α.app (unop X)).op
  naturality X Y f :=
    Quiver.Hom.unop_inj <| by simpa only [Functor.unop_map] using (α.naturality f.unop).symm
Opposite of a natural transformation between unopposite functors
Informal description
Given a natural transformation $\alpha : F^{\mathrm{unop}} \to G^{\mathrm{unop}}$ between functors $F, G : C^{\mathrm{op}} \to D^{\mathrm{op}}$, the operation constructs a natural transformation $G \to F$ by taking the opposite of each component of $\alpha$. Specifically, for each object $X$ in $C^{\mathrm{op}}$, the component at $X$ is given by $(\alpha_{\mathrm{unop}(X)})^{\mathrm{op}}$.
CategoryTheory.NatTrans.removeUnop_id theorem
(F : Cᵒᵖ ⥤ Dᵒᵖ) : NatTrans.removeUnop (𝟙 F.unop) = 𝟙 F
Full source 
@[simp]
theorem removeUnop_id (F : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ) : NatTrans.removeUnop (𝟙 F.unop) = 𝟙 F :=
  rfl
Identity Natural Transformation Preserved Under Unopposite Construction
Informal description
For any functor $F \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$, the opposite of the identity natural transformation on the unopposite functor $F^{\mathrm{unop}}$ is equal to the identity natural transformation on $F$. In other words, $\mathrm{removeUnop}(1_{F^{\mathrm{unop}}}) = 1_F$.
CategoryTheory.NatTrans.leftOp definition
(α : F ⟶ G) : G.leftOp ⟶ F.leftOp
Full source 
/-- Given a natural transformation `α : F ⟶ G`, for `F G : C ⥤ Dᵒᵖ`,
taking `unop` of each component gives a natural transformation `G.leftOp ⟶ F.leftOp`.
-/
@[simps]
protected def leftOp (α : F ⟶ G) : G.leftOp ⟶ F.leftOp where
  app X := (α.app (unop X)).unop
  naturality X Y f := Quiver.Hom.op_inj (by simp)
Left opposite of a natural transformation
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to D^{\mathrm{op}}$, the operation constructs a natural transformation $G^{\mathrm{leftOp}} \to F^{\mathrm{leftOp}}$ by taking the unopposite of each component of $\alpha$. Specifically, for each object $X$ in $C^{\mathrm{op}}$, the component at $X$ is given by $\mathrm{unop}(\alpha_{\mathrm{unop}(X)})$.
CategoryTheory.NatTrans.leftOp_id theorem
: NatTrans.leftOp (𝟙 F : F ⟶ F) = 𝟙 F.leftOp
Full source 
@[simp]
theorem leftOp_id : NatTrans.leftOp (𝟙 F : F ⟶ F) = 𝟙 F.leftOp :=
  rfl
Identity Natural Transformation Preserved Under Left Opposite Construction
Informal description
For any functor $F \colon C \to D^{\mathrm{op}}$, the left opposite of the identity natural transformation on $F$ is equal to the identity natural transformation on the left opposite functor $F^{\mathrm{leftOp}}$. In other words, $\mathrm{leftOp}(1_F) = 1_{F^{\mathrm{leftOp}}}$.
CategoryTheory.NatTrans.leftOp_comp theorem
(α : F ⟶ G) (β : G ⟶ H) : NatTrans.leftOp (α ≫ β) = NatTrans.leftOp β ≫ NatTrans.leftOp α
Full source 
@[simp]
theorem leftOp_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.leftOp (α ≫ β) =
    NatTrans.leftOpNatTrans.leftOp β ≫ NatTrans.leftOp α :=
  rfl
Composition of Natural Transformations Preserved Under Left Opposite Construction
Informal description
Given natural transformations $\alpha \colon F \to G$ and $\beta \colon G \to H$ between functors $F, G, H \colon C \to D^{\mathrm{op}}$, the left opposite of the composition $\alpha \gg \beta$ is equal to the composition of the left opposites of $\beta$ and $\alpha$ in reverse order, i.e., \[ \mathrm{leftOp}(\alpha \gg \beta) = \mathrm{leftOp}(\beta) \gg \mathrm{leftOp}(\alpha). \]
CategoryTheory.NatTrans.removeLeftOp definition
(α : F.leftOp ⟶ G.leftOp) : G ⟶ F
Full source 
/-- Given a natural transformation `α : F.leftOp ⟶ G.leftOp`, for `F G : C ⥤ Dᵒᵖ`,
taking `op` of each component gives a natural transformation `G ⟶ F`.
-/
@[simps]
protected def removeLeftOp (α : F.leftOp ⟶ G.leftOp) : G ⟶ F where
  app X := (α.app (op X)).op
  naturality X Y f :=
    Quiver.Hom.unop_inj <| by simpa only [Functor.leftOp_map] using (α.naturality f.op).symm
Natural transformation from left opposite functors back to original functors
Informal description
Given a natural transformation $\alpha \colon F.\mathrm{leftOp} \to G.\mathrm{leftOp}$ between left opposite functors, the operation $\mathrm{removeLeftOp}(\alpha)$ produces a natural transformation $G \to F$ between the original functors. For each object $X$ in $C$, the component of $\mathrm{removeLeftOp}(\alpha)$ at $X$ is given by the opposite morphism of the component of $\alpha$ at $\mathrm{op}(X)$.
CategoryTheory.NatTrans.removeLeftOp_id theorem
: NatTrans.removeLeftOp (𝟙 F.leftOp) = 𝟙 F
Full source 
@[simp]
theorem removeLeftOp_id : NatTrans.removeLeftOp (𝟙 F.leftOp) = 𝟙 F :=
  rfl
Identity Natural Transformation Preserved Under Remove Left Opposite
Informal description
For any functor $F \colon C \to D^{\mathrm{op}}$, the natural transformation obtained by applying $\mathrm{removeLeftOp}$ to the identity natural transformation on $F.\mathrm{leftOp}$ is equal to the identity natural transformation on $F$. In symbols: \[ \mathrm{removeLeftOp}(1_{F.\mathrm{leftOp}}) = 1_F. \]
CategoryTheory.NatTrans.rightOp definition
(α : F ⟶ G) : G.rightOp ⟶ F.rightOp
Full source 
/-- Given a natural transformation `α : F ⟶ G`, for `F G : Cᵒᵖ ⥤ D`,
taking `op` of each component gives a natural transformation `G.rightOp ⟶ F.rightOp`.
-/
@[simps]
protected def rightOp (α : F ⟶ G) : G.rightOp ⟶ F.rightOp where
  app _ := (α.app _).op
  naturality X Y f := Quiver.Hom.unop_inj (by simp)
Right opposite of a natural transformation
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C^{\mathrm{op}} \to D$, the operation $\mathrm{rightOp}(\alpha)$ produces a natural transformation $G.\mathrm{rightOp} \to F.\mathrm{rightOp}$ between the corresponding right opposite functors. For each object $X$ in $C$, the component of $\mathrm{rightOp}(\alpha)$ at $X$ is given by the opposite morphism of the component of $\alpha$ at $\mathrm{op}(X)$.
CategoryTheory.NatTrans.rightOp_id theorem
: NatTrans.rightOp (𝟙 F : F ⟶ F) = 𝟙 F.rightOp
Full source 
@[simp]
theorem rightOp_id : NatTrans.rightOp (𝟙 F : F ⟶ F) = 𝟙 F.rightOp :=
  rfl
Identity Natural Transformation Preserved Under Right Opposite
Informal description
The right opposite of the identity natural transformation on a functor $F \colon C^{\mathrm{op}} \to D$ is equal to the identity natural transformation on the right opposite functor $F^{\mathrm{rightOp}} \colon C \to D^{\mathrm{op}}$. In symbols, $\mathrm{rightOp}(1_F) = 1_{F^{\mathrm{rightOp}}}$.
CategoryTheory.NatTrans.rightOp_comp theorem
(α : F ⟶ G) (β : G ⟶ H) : NatTrans.rightOp (α ≫ β) = NatTrans.rightOp β ≫ NatTrans.rightOp α
Full source 
@[simp]
theorem rightOp_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.rightOp (α ≫ β) =
    NatTrans.rightOpNatTrans.rightOp β ≫ NatTrans.rightOp α :=
  rfl
Composition of Natural Transformations Preserved Under Right Opposite
Informal description
For any natural transformations $\alpha \colon F \to G$ and $\beta \colon G \to H$ between functors $F, G, H \colon C^{\mathrm{op}} \to D$, the right opposite of the composition $\alpha \circ \beta$ is equal to the composition of the right opposites of $\beta$ and $\alpha$ in reverse order. That is, $\mathrm{rightOp}(\alpha \circ \beta) = \mathrm{rightOp}(\beta) \circ \mathrm{rightOp}(\alpha)$.
CategoryTheory.NatTrans.removeRightOp definition
(α : F.rightOp ⟶ G.rightOp) : G ⟶ F
Full source 
/-- Given a natural transformation `α : F.rightOp ⟶ G.rightOp`, for `F G : Cᵒᵖ ⥤ D`,
taking `unop` of each component gives a natural transformation `G ⟶ F`.
-/
@[simps]
protected def removeRightOp (α : F.rightOp ⟶ G.rightOp) : G ⟶ F where
  app X := (α.app X.unop).unop
  naturality X Y f :=
    Quiver.Hom.op_inj <| by simpa only [Functor.rightOp_map] using (α.naturality f.unop).symm
Natural transformation from right opposite functors
Informal description
Given a natural transformation $\alpha \colon F^{\mathrm{rightOp}} \to G^{\mathrm{rightOp}}$ between functors $F^{\mathrm{rightOp}}, G^{\mathrm{rightOp}} \colon C \to D^{\mathrm{op}}$, the operation $\mathrm{removeRightOp}(\alpha)$ constructs a natural transformation $G \to F$ between the original functors $F, G \colon C^{\mathrm{op}} \to D$. This is achieved by applying the $\mathrm{unop}$ operation to each component of $\alpha$.
CategoryTheory.NatTrans.removeRightOp_id theorem
: NatTrans.removeRightOp (𝟙 F.rightOp) = 𝟙 F
Full source 
@[simp]
theorem removeRightOp_id : NatTrans.removeRightOp (𝟙 F.rightOp) = 𝟙 F :=
  rfl
Identity Preservation Under removeRightOp Operation
Informal description
For any functor $F \colon C^{\mathrm{op}} \to D$, applying the $\mathrm{removeRightOp}$ operation to the identity natural transformation on $F^{\mathrm{rightOp}}$ yields the identity natural transformation on $F$. That is, $\mathrm{removeRightOp}(1_{F^{\mathrm{rightOp}}}) = 1_F$.
CategoryTheory.Iso.op definition
(α : X ≅ Y) : op Y ≅ op X
Full source 
/-- The opposite isomorphism.
-/
@[simps]
protected def op (α : X ≅ Y) : opop Y ≅ op X where
  hom := α.hom.op
  inv := α.inv.op
  hom_inv_id := Quiver.Hom.unop_inj α.inv_hom_id
  inv_hom_id := Quiver.Hom.unop_inj α.hom_inv_id
Opposite isomorphism
Informal description
Given an isomorphism $\alpha \colon X \cong Y$ in a category $\mathcal{C}$, the operation $\mathrm{op}(\alpha)$ constructs an isomorphism $\mathrm{op}(Y) \cong \mathrm{op}(X)$ in the opposite category $\mathcal{C}^{\mathrm{op}}$. The morphisms in the opposite isomorphism are obtained by applying the $\mathrm{op}$ operation to the morphisms of $\alpha$, and the required composition identities are preserved by this construction.
CategoryTheory.Iso.unop definition
{X Y : Cᵒᵖ} (f : X ≅ Y) : Y.unop ≅ X.unop
Full source 
/-- The isomorphism obtained from an isomorphism in the opposite category. -/
@[simps]
def unop {X Y : Cᵒᵖ} (f : X ≅ Y) : Y.unop ≅ X.unop where
  hom := f.hom.unop
  inv := f.inv.unop
  hom_inv_id := by simp only [← unop_comp, f.inv_hom_id, unop_id]
  inv_hom_id := by simp only [← unop_comp, f.hom_inv_id, unop_id]
Unop operation on isomorphisms in the opposite category
Informal description
Given an isomorphism $f \colon X \cong Y$ in the opposite category $\mathcal{C}^{\mathrm{op}}$, the operation $\mathrm{unop}(f)$ constructs an isomorphism $Y.\mathrm{unop} \cong X.\mathrm{unop}$ in the original category $\mathcal{C}$. The morphisms in the isomorphism are obtained by applying the $\mathrm{unop}$ operation to the morphisms of $f$, and the required composition identities are preserved by this construction.
CategoryTheory.Iso.unop_op theorem
{X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f
Full source 
@[simp]
theorem unop_op {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f := by (ext; rfl)
Involutivity of Opposite and Unopposite Operations on Isomorphisms
Informal description
For any isomorphism $f \colon X \cong Y$ in the opposite category $\mathcal{C}^{\mathrm{op}}$, the composition of the $\mathrm{unop}$ and $\mathrm{op}$ operations yields back the original isomorphism, i.e., $(\mathrm{unop}(f)).\mathrm{op} = f$.
CategoryTheory.Iso.op_unop theorem
{X Y : C} (f : X ≅ Y) : f.op.unop = f
Full source 
@[simp]
theorem op_unop {X Y : C} (f : X ≅ Y) : f.op.unop = f := by (ext; rfl)
Involutivity of Opposite and Unopposite Operations on Isomorphisms
Informal description
For any isomorphism $f \colon X \cong Y$ in a category $\mathcal{C}$, applying the opposite operation followed by the unopposite operation yields back the original isomorphism, i.e., $\mathrm{unop}(\mathrm{op}(f)) = f$.
CategoryTheory.Iso.unop_hom_inv_id_app theorem
: (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma unop_hom_inv_id_app : (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 _ := by
  rw [← unop_comp, inv_hom_id_app, unop_id]
Unopposite Components of Natural Isomorphism Satisfy Hom-Inv Identity
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the composition of the unopposite of the forward component $e.hom.app\ X$ followed by the unopposite of the inverse component $e.inv.app\ X$ is equal to the identity morphism on the unopposite of $G(X)$, i.e., $(e.hom.app\ X)^{\mathrm{unop}} \circ (e.inv.app\ X)^{\mathrm{unop}} = \mathrm{id}_{G(X)^{\mathrm{unop}}}$.
CategoryTheory.Iso.unop_inv_hom_id_app theorem
: (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma unop_inv_hom_id_app : (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 _ := by
  rw [← unop_comp, hom_inv_id_app, unop_id]
Inverse-Hom Composition Identity for Unopposite Natural Isomorphism Components
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the composition of the unopposite of the inverse component $(e.inv.app\ X)^{\mathrm{unop}}$ followed by the unopposite of the forward component $(e.hom.app\ X)^{\mathrm{unop}}$ is equal to the identity morphism on the unopposite of $F(X)$, i.e., $(e.inv.app\ X)^{\mathrm{unop}} \circ (e.hom.app\ X)^{\mathrm{unop}} = \mathrm{id}_{F(X)^{\mathrm{unop}}}$.
CategoryTheory.NatIso.op definition
(α : F ≅ G) : G.op ≅ F.op
Full source 
/-- The natural isomorphism between opposite functors `G.op ≅ F.op` induced by a natural
isomorphism between the original functors `F ≅ G`. -/
@[simps]
protected def op (α : F ≅ G) : G.op ≅ F.op where
  hom := NatTrans.op α.hom
  inv := NatTrans.op α.inv
  hom_inv_id := by ext; dsimp; rw [← op_comp]; rw [α.inv_hom_id_app]; rfl
  inv_hom_id := by ext; dsimp; rw [← op_comp]; rw [α.hom_inv_id_app]; rfl
Opposite natural isomorphism
Informal description
Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$, the opposite natural isomorphism $\alpha^{\mathrm{op}} \colon G^{\mathrm{op}} \cong F^{\mathrm{op}}$ is defined by: - The forward component $\alpha^{\mathrm{op}}.\mathrm{hom}$ is the opposite of the forward component $\alpha.\mathrm{hom}$. - The inverse component $\alpha^{\mathrm{op}}.\mathrm{inv}$ is the opposite of the inverse component $\alpha.\mathrm{inv}$. - The hom-inv and inv-hom identities are satisfied by construction, following from the corresponding identities of $\alpha$.
CategoryTheory.NatIso.removeOp definition
(α : F.op ≅ G.op) : G ≅ F
Full source 
/-- The natural isomorphism between functors `G ≅ F` induced by a natural isomorphism
between the opposite functors `F.op ≅ G.op`. -/
@[simps]
protected def removeOp (α : F.op ≅ G.op) : G ≅ F where
  hom := NatTrans.removeOp α.hom
  inv := NatTrans.removeOp α.inv
Unopposite natural isomorphism
Informal description
Given a natural isomorphism $\alpha \colon F^{\mathrm{op}} \cong G^{\mathrm{op}}$ between opposite functors, this constructs a natural isomorphism $G \cong F$ by taking the unopposite of both the forward and inverse components of $\alpha$.
CategoryTheory.NatIso.unop definition
{F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : G.unop ≅ F.unop
Full source 
/-- The natural isomorphism between functors `G.unop ≅ F.unop` induced by a natural isomorphism
between the original functors `F ≅ G`. -/
@[simps]
protected def unop {F G : CᵒᵖCᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : G.unop ≅ F.unop where
  hom := NatTrans.unop α.hom
  inv := NatTrans.unop α.inv
Unopposite natural isomorphism
Informal description
Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$, the unopposite natural isomorphism $\alpha^{\mathrm{unop}} \colon G^{\mathrm{unop}} \cong F^{\mathrm{unop}}$ is defined by: - The forward component is the unopposite of the forward component of $\alpha$. - The inverse component is the unopposite of the inverse component of $\alpha$. - The isomorphism properties are preserved by construction.
CategoryTheory.Equivalence.op definition
(e : C ≌ D) : Cᵒᵖ ≌ Dᵒᵖ
Full source 
/-- An equivalence between categories gives an equivalence between the opposite categories.
-/
@[simps]
def op (e : C ≌ D) : CᵒᵖCᵒᵖ ≌ Dᵒᵖ where
  functor := e.functor.op
  inverse := e.inverse.op
  unitIso := (NatIso.op e.unitIso).symm
  counitIso := (NatIso.op e.counitIso).symm
  functor_unitIso_comp X := by
    apply Quiver.Hom.unop_inj
    dsimp
    simp
Opposite equivalence of categories
Informal description
Given an equivalence of categories $e \colon C \simeq D$, the opposite equivalence $e^{\mathrm{op}} \colon C^{\mathrm{op}} \simeq D^{\mathrm{op}}$ is constructed as follows: - The functor is the opposite functor $F^{\mathrm{op}}$ of the original functor $F$. - The inverse functor is the opposite functor $G^{\mathrm{op}}$ of the original inverse functor $G$. - The unit isomorphism is the opposite of the original unit isomorphism, with its direction reversed. - The counit isomorphism is the opposite of the original counit isomorphism, with its direction reversed. - The functor-unit isomorphism composition condition is satisfied by construction, as verified by the given proof.
CategoryTheory.Equivalence.unop definition
(e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D
Full source 
/-- An equivalence between opposite categories gives an equivalence between the original categories.
-/
@[simps]
def unop (e : CᵒᵖCᵒᵖ ≌ Dᵒᵖ) : C ≌ D where
  functor := e.functor.unop
  inverse := e.inverse.unop
  unitIso := (NatIso.unop e.unitIso).symm
  counitIso := (NatIso.unop e.counitIso).symm
  functor_unitIso_comp X := by
    apply Quiver.Hom.op_inj
    dsimp
    simp
Unopposite equivalence of categories
Informal description
Given an equivalence of categories $e \colon C^{\mathrm{op}} \simeq D^{\mathrm{op}}$ between opposite categories, the unopposite equivalence $e^{\mathrm{unop}} \colon C \simeq D$ is constructed as follows: - The functor is the unopposite functor $F^{\mathrm{unop}}$ of the original functor $F$. - The inverse functor is the unopposite functor $G^{\mathrm{unop}}$ of the original inverse functor $G$. - The unit isomorphism is the inverse of the unopposite of the original unit isomorphism. - The counit isomorphism is the inverse of the unopposite of the original counit isomorphism. - The functor-unit isomorphism composition condition is satisfied by construction.
CategoryTheory.opEquiv definition
(A B : Cᵒᵖ) : (A ⟶ B) ≃ (B.unop ⟶ A.unop)
Full source 
/-- The equivalence between arrows of the form `A ⟶ B` and `B.unop ⟶ A.unop`. Useful for building
adjunctions.
Note that this (definitionally) gives variants
```
def opEquiv' (A : C) (B : Cᵒᵖ) : (Opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
  opEquiv _ _

def opEquiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ Opposite.op B) ≃ (B ⟶ A.unop) :=
  opEquiv _ _

def opEquiv''' (A B : C) : (Opposite.op A ⟶ Opposite.op B) ≃ (B ⟶ A) :=
  opEquiv _ _
```
-/
@[simps]
def opEquiv (A B : Cᵒᵖ) : (A ⟶ B) ≃ (B.unop ⟶ A.unop) where
  toFun f := f.unop
  invFun g := g.op
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between opposite morphisms and original morphisms
Informal description
The equivalence between morphisms $A \to B$ in the opposite category $\mathcal{C}^\mathrm{op}$ and morphisms $B^\mathrm{unop} \to A^\mathrm{unop}$ in the original category $\mathcal{C}$. This equivalence is definitionally bidirectional, with the forward direction given by `unop` and the reverse direction given by `op`.
CategoryTheory.subsingleton_of_unop instance
(A B : Cᵒᵖ) [Subsingleton (unop B ⟶ unop A)] : Subsingleton (A ⟶ B)
Full source 
instance subsingleton_of_unop (A B : Cᵒᵖ) [Subsingleton (unopunop B ⟶ unop A)] : Subsingleton (A ⟶ B) :=
  (opEquiv A B).subsingleton
Subsingleton Property of Morphisms in Opposite Categories
Informal description
For any objects $A$ and $B$ in the opposite category $\mathcal{C}^\mathrm{op}$, if the morphisms from $B^\mathrm{unop}$ to $A^\mathrm{unop}$ in $\mathcal{C}$ form a subsingleton (i.e., there is at most one morphism between them), then the morphisms from $A$ to $B$ in $\mathcal{C}^\mathrm{op}$ also form a subsingleton.
CategoryTheory.decidableEqOfUnop instance
(A B : Cᵒᵖ) [DecidableEq (unop B ⟶ unop A)] : DecidableEq (A ⟶ B)
Full source 
instance decidableEqOfUnop (A B : Cᵒᵖ) [DecidableEq (unopunop B ⟶ unop A)] : DecidableEq (A ⟶ B) :=
  (opEquiv A B).decidableEq
Decidable Equality of Morphisms in Opposite Categories via Unop
Informal description
For any objects $A$ and $B$ in the opposite category $\mathcal{C}^\mathrm{op}$, if there is a decidable equality for morphisms $B^\mathrm{unop} \to A^\mathrm{unop}$ in the original category $\mathcal{C}$, then there is also a decidable equality for morphisms $A \to B$ in $\mathcal{C}^\mathrm{op}$.
CategoryTheory.isoOpEquiv definition
(A B : Cᵒᵖ) : (A ≅ B) ≃ (B.unop ≅ A.unop)
Full source 
/-- The equivalence between isomorphisms of the form `A ≅ B` and `B.unop ≅ A.unop`.

Note this is definitionally the same as the other three variants:
* `(Opposite.op A ≅ B) ≃ (B.unop ≅ A)`
* `(A ≅ Opposite.op B) ≃ (B ≅ A.unop)`
* `(Opposite.op A ≅ Opposite.op B) ≃ (B ≅ A)`
-/
@[simps]
def isoOpEquiv (A B : Cᵒᵖ) : (A ≅ B) ≃ (B.unop ≅ A.unop) where
  toFun f := f.unop
  invFun g := g.op
  left_inv _ := by
    ext
    rfl
  right_inv _ := by
    ext
    rfl
Equivalence between isomorphisms in opposite categories
Informal description
The equivalence between isomorphisms $A \cong B$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ and isomorphisms $B^{\mathrm{unop}} \cong A^{\mathrm{unop}}$ in the original category $\mathcal{C}$. This equivalence is given by the operations $\mathrm{unop}$ (from $\mathcal{C}^{\mathrm{op}}$ to $\mathcal{C}$) and $\mathrm{op}$ (from $\mathcal{C}$ to $\mathcal{C}^{\mathrm{op}}$), which are mutually inverse.
CategoryTheory.Functor.opUnopEquiv definition
: (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ
Full source 
/-- The equivalence of functor categories induced by `op` and `unop`.
-/
@[simps]
def opUnopEquiv : (C ⥤ D)ᵒᵖ(C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ where
  functor := opHom _ _
  inverse := opInv _ _
  unitIso :=
    NatIso.ofComponents (fun F => F.unop.opUnopIso.op)
      (by
        intro F G f
        dsimp [opUnopIso]
        rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]
        congr 1
        aesop_cat)
  counitIso := NatIso.ofComponents fun F => F.unopOpIso
Equivalence between opposite functor categories via op and unop
Informal description
The equivalence of categories between the opposite category of functors from $C$ to $D$ and the category of functors from $C^{\mathrm{op}}$ to $D^{\mathrm{op}}$. This equivalence is constructed via the operations `opHom` and `opInv`, with natural isomorphisms witnessing the equivalence.
CategoryTheory.Functor.leftOpRightOpEquiv definition
: (Cᵒᵖ ⥤ D)ᵒᵖ ≌ C ⥤ Dᵒᵖ
Full source 
/-- The equivalence of functor categories induced by `leftOp` and `rightOp`.
-/
@[simps!]
def leftOpRightOpEquiv : (Cᵒᵖ ⥤ D)ᵒᵖ(Cᵒᵖ ⥤ D)ᵒᵖ ≌ C ⥤ Dᵒᵖ where
  functor :=
    { obj := fun F => F.unop.rightOp
      map := fun η => NatTrans.rightOp η.unop }
  inverse :=
    { obj := fun F => op F.leftOp
      map := fun η => η.leftOp.op }
  unitIso :=
    NatIso.ofComponents (fun F => F.unop.rightOpLeftOpIso.op)
      (by
        intro F G η
        dsimp
        rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]
        congr 1
        aesop_cat)
  counitIso := NatIso.ofComponents fun F => F.leftOpRightOpIso
Equivalence between opposite functor categories via left and right opposites
Informal description
The equivalence of categories between the opposite category of functors from $C^{\mathrm{op}}$ to $D$ and the category of functors from $C$ to $D^{\mathrm{op}}$. This equivalence is constructed via the `leftOp` and `rightOp` operations on functors, with natural isomorphisms witnessing the equivalence.
CategoryTheory.Functor.instEssSurjOppositeOp instance
{F : C ⥤ D} [EssSurj F] : EssSurj F.op
Full source 
instance {F : C ⥤ D} [EssSurj F] : EssSurj F.op where
  mem_essImage X := ⟨op _, ⟨(F.objObjPreimageIso X.unop).op.symm⟩⟩
Essential Surjectivity of Opposite Functors
Informal description
For any essentially surjective functor $F \colon C \to D$, the opposite functor $F^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$ is also essentially surjective.
CategoryTheory.Functor.instEssSurjOppositeRightOp instance
{F : Cᵒᵖ ⥤ D} [EssSurj F] : EssSurj F.rightOp
Full source 
instance {F : CᵒᵖCᵒᵖ ⥤ D} [EssSurj F] : EssSurj F.rightOp where
  mem_essImage X := ⟨_, ⟨(F.objObjPreimageIso X.unop).op.symm⟩⟩
Essential Surjectivity of the Right Opposite Functor
Informal description
For any essentially surjective functor $F \colon C^{\mathrm{op}} \to D$, the right opposite functor $F.\mathrm{rightOp} \colon C \to D^{\mathrm{op}}$ is also essentially surjective.
CategoryTheory.Functor.instEssSurjOppositeLeftOp instance
{F : C ⥤ Dᵒᵖ} [EssSurj F] : EssSurj F.leftOp
Full source 
instance {F : C ⥤ Dᵒᵖ} [EssSurj F] : EssSurj F.leftOp where
  mem_essImage X := ⟨op _, ⟨(F.objObjPreimageIso (op X)).unop.symm⟩⟩
Essential Surjectivity of the Left Opposite Functor
Informal description
For any essentially surjective functor $F \colon C \to D^{\mathrm{op}}$, the left opposite functor $F.\mathrm{leftOp} \colon C^{\mathrm{op}} \to D$ is also essentially surjective.
CategoryTheory.Functor.instIsEquivalenceOppositeOp instance
{F : C ⥤ D} [IsEquivalence F] : IsEquivalence F.op
Full source 
instance {F : C ⥤ D} [IsEquivalence F] : IsEquivalence F.op where
Opposite Functor Preserves Equivalence of Categories
Informal description
For any functor $F \colon C \to D$ that is an equivalence of categories, the opposite functor $F^{\mathrm{op}} \colon C^{\mathrm{op}} \to D^{\mathrm{op}}$ is also an equivalence of categories.
CategoryTheory.Functor.instIsEquivalenceOppositeRightOp instance
{F : Cᵒᵖ ⥤ D} [IsEquivalence F] : IsEquivalence F.rightOp
Full source 
instance {F : CᵒᵖCᵒᵖ ⥤ D} [IsEquivalence F] : IsEquivalence F.rightOp where
Equivalence of Categories Preserved under Right Opposite Functor Construction
Informal description
For any functor $F \colon C^{\mathrm{op}} \to D$ that is an equivalence of categories, the right opposite functor $F.\mathrm{rightOp} \colon C \to D^{\mathrm{op}}$ is also an equivalence of categories.
CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp instance
{F : C ⥤ Dᵒᵖ} [IsEquivalence F] : IsEquivalence F.leftOp
Full source 
instance {F : C ⥤ Dᵒᵖ} [IsEquivalence F] : IsEquivalence F.leftOp where
Equivalence of Categories Preserved under Left Opposite Functor Construction
Informal description
For any functor $F \colon C \to D^{\mathrm{op}}$ that is an equivalence of categories, the left opposite functor $F.\mathrm{leftOp} \colon C^{\mathrm{op}} \to D$ is also an equivalence of categories.