objOpOp — Mathlib

English

Taking the unop of morphisms yields a natural isomorphism between coyoneda.obj(op(op X)) and yoneda.obj X.

Русский

Обращение к противоположному объекту на оба раза даёт естественный изоморфизм между coyoneda.obj(op(op X)) и yoneda.obj X.

LaTeX

$$$\mathrm{coyoneda.obj}(\mathrm{op}(\mathrm{op} X)) \cong \mathrm{yoneda.obj} X$$$

Lean4

/-- Taking the `unop` of morphisms is a natural isomorphism. -/
@[simps!]
def objOpOp (X : C) : coyoneda.obj (op (op X)) ≅ yoneda.obj X :=
  NatIso.ofComponents fun _ => (opEquiv _ _).toIso

Похожие утверждения