natIsoOfRightAdjointNatIso — Mathlib

Lean4

/-- Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left
adjoints.

Note: it is generally better to use `Adjunction.natIsoEquiv`, see the file `Adjunction.Unique`.
The reason this definition still exists is that apparently `CategoryTheory.extendAlongYonedaYoneda`
uses its definitional properties (TODO: figure out a way to avoid this).
-/
def natIsoOfRightAdjointNatIso {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (r : G ≅ G') : F ≅ F' :=
  NatIso.removeOp
    ((Coyoneda.fullyFaithful.whiskeringRight _).isoEquiv.symm (leftAdjointsCoyonedaEquiv adj2 (adj1.ofNatIsoRight r)))

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