English
There is an equivalence between isomorphisms A ≅ B in Cᵒᵖ and isomorphisms B.unop ≅ A.unop in C; toFun sends an isomorphism to its unop, invFun sends back by op.
Русский
Существует эквивалентность между изоморфизмами A ≅ B в Cᵒᵖ и изоморфизмами B.unop ≅ A.unop в C; отображение toFun отправляет изоморфизм в его unop, invFun возвращает через op.
LaTeX
$$$isoOpEquiv(A,B) : (A \cong B) \simeq (B.unop \cong A.unop) \quad\text{with } toFun f = f.unop,\ invFun g = g.op$$$
Lean4
/-- 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
