English
For an isomorphism e: F ≅ G of functors F,G: C ⥤ D^{op}, and any object X, the composite (e.hom.app X)^{op} ∘ (e.inv.app X)^{op} equals the identity on G.obj X.
Русский
Для изоморфизма e: F ≅ G между F,G: C ⥤ D^{op} и любого X должен выполняться (e.hom.app X)^{op} ∘ (e.inv.app X)^{op} = id_{G.obj X}.
LaTeX
$$$\\\\forall {C} [Category C], \\\\forall {D} [Category D^{op}], \\\\forall {F G : C \\\\to D^{op}}, \\\\forall e: F \\\\cong G, \\\\forall X, (e.hom.app X)^{\\\\mathrm{op}} \\\\circ (e.inv.app X)^{\\\\mathrm{op}} = id_{G.obj X}.$$$
Lean4
/-- The opposite isomorphism.
-/
@[simps]
protected def op (α : X ≅ Y) : op 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
