Is there code for nat trans between right adjoints?

Stream: Is there code for X?

[Gareth Ma]

As title. I managed to get some code:

import Mathlib

namespace CategoryTheory.Functor
open Category

universe u v

variable {C D : Type u} [Category C] [Category D] {F G : C ⥤ D}
    [F.IsLeftAdjoint] [G.IsLeftAdjoint]

def rightAdjHom (f : F ⟶ G) : G.rightAdjoint ⟶ F.rightAdjoint:=
  whiskerLeft _ (Adjunction.ofIsLeftAdjoint _).unit
    ≫ whiskerLeft _ (whiskerRight f _)
      ≫ whiskerRight (Adjunction.ofIsLeftAdjoint _).counit _

example : rightAdjHom (𝟙 F) = 𝟙 F.rightAdjoint := by
  sorry

But I can't seem to prove anything about it (as I am not very good at category theory admittedly), even the simplest identity. Does it exist in Mathlib already somehow? cc @Joël Riou

[Aaron Liu]

import Mathlib

namespace CategoryTheory.Functor
open Category

universe u v

variable {C D : Type u} [Category C] [Category D] {F G : C ⥤ D}
    [F.IsLeftAdjoint] [G.IsLeftAdjoint]

noncomputable def rightAdjHom (f : F ⟶ G) : G.rightAdjoint ⟶ F.rightAdjoint:=
  whiskerLeft _ (Adjunction.ofIsLeftAdjoint _).unit
    ≫ whiskerLeft _ (whiskerRight f _)
      ≫ whiskerRight (Adjunction.ofIsLeftAdjoint _).counit _

example : rightAdjHom (𝟙 F) = 𝟙 F.rightAdjoint := by
  rw [rightAdjHom, whiskerRight_id', whiskerLeft_id', id_comp]
  apply CategoryTheory.Adjunction.right_triangle

[Gareth Ma]

While you are at it do you mind showing this as well... and I can PR it (wrapped into a functor or whatever) under your name

example {F G H : C ⥤ D} [F.IsLeftAdjoint] [G.IsLeftAdjoint] [H.IsLeftAdjoint]
    (f : F ⟶ G) (f' : G ⟶ H) :
    rightAdjHom (f ≫ f') = rightAdjHom f' ≫ rightAdjHom f := by
  sorry

[Aaron Liu]

I'm sure you can figure it out on your own

[Gareth Ma]

Well I can't, I tried and it became a mess, that's why I am asking here. But nevermind

[Gareth Ma]

Please don't bother with it haha

[Aaron Liu]

What specifically stopped you?

[Joël Riou]

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

[Aaron Liu]

interesting

[Gareth Ma]

2025-07-16_21-41-54.png

Good to know the Mathlib proof looks like this

[Aaron Liu]

oh it's not just me