Right adjoint from natural isomorphism between homsets

Stream: mathlib4

[Gareth Ma]

I am trying to formalise Proposition 4.3.4 from Riehl's category theory in context, also known as Stacks 0A8B. The proof is supposed to be a very simple application of Yoneda lemma. However, my formalisation seems very unnatural, especially the proof of map_comp I would expect it to be straightforward and not several layers of simp. Can someone more familiar with the category theory library help out? Thanks!

import Mathlib

open CategoryTheory

universe u v
variable {A B : Type u} [Category A] [Category B] (F : A ⥤ B)
    (G_ : B → A) (h : ∀ b : B, (F.op ⋙ yoneda.obj b).RepresentableBy (G_ b)) :

def construct_G : B ⥤ A where
  obj := G_
  map f :=
    Yoneda.fullyFaithful.preimage <|
      (h _).toIso.hom ≫ F.op.whiskerLeft (yoneda.map f) ≫ (h _).toIso.symm.hom
  map_id := by simp
  map_comp f g := by
    expose_names
    simp [Yoneda.fullyFaithful_preimage, Functor.RepresentableBy.toIso,
      Functor.representableByEquiv]
    convert ((h Z).comp_homEquiv_symm _ _).symm
    simp [← Category.assoc]
    congr 1
    convert (h Y).homEquiv_comp ..
    simp
    exact (Equiv.apply_symm_apply _ _).symm

def construct_G_adjoint : F ⊣ construct_G F G_ h := by
  sorry

[Gareth Ma]

Oh I got this working

lemma rw_asdf (a b c : A) (f : yoneda.obj a ⟶ yoneda.obj b) (g : yoneda.obj b ⟶ yoneda.obj c) :
    yonedaEquiv (f ≫ g) = yonedaEquiv f ≫ yonedaEquiv g := by
  simp [yonedaEquiv]

-- proposition 4.3.4
def construct_G (h : ∀ b : B, (F.op ⋙ yoneda.obj b).RepresentableBy (G_ b)) : B ⥤ A where
  obj := G_
  map f := yonedaEquiv <| (h _).toIso.hom ≫ F.op.whiskerLeft (yoneda.map f) ≫ (h _).toIso.inv
  map_id := by simp [yonedaEquiv]
  map_comp := by
    intro X Y Z f g
    rw [← rw_asdf]
    simp

[Joël Riou]

See also https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Adjunction/PartialAdjoint.html

[Gareth Ma]

Does this imply my result? I spent some time looking at it but I think my category theory is too weak to understand its implications

[Joël Riou]

Yes, it does. (I only formalized the case of left adjoints though.)

[Gareth Ma]

Oh I understand now

[Gareth Ma]

Okay I dualised your result to right adjoint

[Gareth Ma]

Also I finally understand the file. In fact, what I need is just Adjunction.rightAdjointOfEquiv, yours is a generalisation of it. Speaking of which, maybe I should also prove that your F.LeftAdjoint equals* the one obtained from Adjunction.leftAdjointOfEquiv (... F.partialLeftAdjointHomEquiv ...) (something using RepresentableBy.comp_homEquiv_symm)

[Gareth Ma]

As in

universe u v
variable {A B : Type u} [Category A] [Category B] (F : A ⥤ B)
    [∀ b : B, (F.op ⋙ yoneda.obj b).IsRepresentable]

def rightAdj' : B ⥤ A :=
  Adjunction.rightAdjointOfEquiv
    (fun _ _ ↦ (F.op ⋙ yoneda.obj _).representableBy.homEquiv.symm)
    (fun _ _ _ _ _ ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)

def construct_G_adjoint : F ⊣ F.rightAdj' :=
  Adjunction.adjunctionOfEquivRight _ _

[Joël Riou]

I think that what could be added (in a separate PR as #27148) is that when F.rightAdjointObjIsDefined = ⊤, then
F.partialRightAdjoint : F.PartialRightAdjointSource ⥤ C is the right adjoint of the functor induced by F (taking into account that F.PartialRightAdjointSource is equivalent to D).

[Gareth Ma]

done