English
There is a canonical equivalence between morphisms A → B in the opposite category Cᵒᵖ and morphisms B.unop → A.unop in C. The equivalence is given by toFun f = f.unop and invFun g = g.op.
Русский
Существует каноническая эквивалентность между морфизмами A → B в противоположной категории Cᵒᵖ и морфизмами B.unop → A.unop в C. Эквивалентность задаётся через отображения f ↦ f.unop и g ↦ g.op.
LaTeX
$$$opEquiv(A,B) : (A \to B) \simeq (B.unop \to A.unop) \quad\text{with}\quad toFun\ f = f.unop,\ invFun\ g = g.op$$$
Lean4
/-- 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
