inverseFunctorObjIso — Mathlib

English

There is a canonical identity isomorphism between the inverse functor's object and the opposite of the inverse equivalence.

Русский

Существует каноническое тождественное изоморфление между объектом обратного функторa и противоположностью обратной эквивалентности.

LaTeX

$$$(\\text{inverseFunctor } C D).\\mathrm{obj}\\; e \\cong \\mathrm{Opposite.op}\\; e^{-1}$$$

Lean4

/-- The `inverse` functor sends an equivalence to its inverse. -/
@[simps!]
def inverseFunctorObjIso (e : C ≌ D) : (inverseFunctor C D).obj e ≅ Opposite.op e.inverse :=
  Iso.refl _

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