Hom iso of an adjunction as a natural iso of functors

Stream: Is there code for X?

[Jakob von Raumer]

Do we really not have this for adjunctions? Or am I just not capable of finding it?

import Mathlib

open CategoryTheory

example {C : Type u₁} [Category.{v₁} C] {D : Type u₁} [Category.{v₁} D]
    (F : C ⥤ D) (G : D ⥤ C) (hFG : F ⊣ G) :
    F.op ⋙ coyoneda ≅ coyoneda ⋙ (whiskeringLeft D C _).obj G := by
  sorry

[Jakob von Raumer]

@Dagur Asgeirsson @Joël Riou

[Dagur Asgeirsson]

NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ (hFG.homEquiv _ _).toIso)) works, I'm not sure if we have this as a definition in mathlib

[Jakob von Raumer]

I think I'll add it under the def of Adjunction.homEquiv...

[Jakob von Raumer]

Do we generally prefer to chain isos in e.g. Cᵒᵖ ⥤ D ⥤ Type v₁ instead of chaining type equivalences in proofs? Feels to me that from an aesthetic point of view the former is preferrable, but I'm not sure about performance...

[Jakob von Raumer]

In a similar vein I think we also could use a version of docs#CategoryTheory.Limits.colimCoyoneda which for the case where the lift isn't required

[Joël Riou]

Jakob von Raumer said:

Do we generally prefer to chain isos in e.g. Cᵒᵖ ⥤ D ⥤ Type v₁ instead of chaining type equivalences in proofs? Feels to me that from an aesthetic point of view the former is preferrable, but I'm not sure about performance...

As long as you do not need to evaluate morphisms at elements (i.e. everything works as if Type _ was replaced by any generic category), it is certainly ok to use isos, but otherwise, I prefer type equivalences over isomorphisms in Type* (one of the reasons is that it is possible to phrase equivalences between types in different universes...). For example, I was very much in favor of the refactor part of #12041, where yonedaEquiv was redefined directly as an equivalence rather than obtained from an isomorphism in Type _.

[Jakob von Raumer]

Not sure if I understand what you mean, I wasn't talking about equivs vs isos in Type _

[Jakob von Raumer]

But about proving things pointwise when they can be proven pointfree (not sure if that is the correct term)

[Jakob von Raumer]

The above example is the "pointfree" version of what docs#CategoryTheory.Adjunction.homEquiv is pointwise. When constructing more complex NatIsos , the choice is between using NatIso.ofComponents on the whole composite chain of type equivalences vs to use building blocks like the example above.

[Jakob von Raumer]

(deleted)