evaluation is right adjoint

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have the following? It seems like something basic that should be there, but I can't seem to find anything similar...

import category_theory.types
import category_theory.const
import category_theory.functor_category
import category_theory.limits.shapes.products

namespace category_theory

open category_theory.limits

universes v u₁ u₂
variables {C : Type u₁} [category.{v} C] {D : Type u₂} [category.{v} D]
variables [∀ (a b : C), has_coproducts_of_shape (a ⟶ b) D]

-- Some more code goes here...

noncomputable
instance (a : C) : is_right_adjoint ((evaluation C D).obj a) :=
⟨_, evaluation_adjunction _ _⟩

end category_theory

[Adam Topaz]

(The --some more code part can be found here: https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/evaluation_adjunction.lean )

[Adam Topaz]

I mostly want this because of the following

lemma mono_iff_app_mono {F G : C ⥤ D} (η : F ⟶ G) :
  mono η ↔ (∀ X, mono (η.app X)) :=
begin
  split,
  { intros h X,
    exact right_adjoint_preserves_mono (evaluation_adjunction _ _) h },
  { introsI _, apply nat_trans.mono_app_of_mono }
end