evaluationAdjunctionRight — Mathlib

Lean4
/-- The adjunction showing that evaluation is a right adjoint. -/
@[simps! unit_app counit_app_app]
def evaluationAdjunctionRight (c : C) : evaluationLeftAdjoint D c ⊣ (evaluation _ _).obj c :=
  Adjunction.mkOfHomEquiv
    {
      homEquiv := fun d F =>
        { toFun := fun f => Sigma.ι (fun _ => d) (𝟙 _) ≫ f.app c
          invFun := fun f => { app := fun _ => Sigma.desc fun h => f ≫ F.map h }
          left_inv := by
            intro f
            ext x
            dsimp
            ext g
            simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ← f.naturality, evaluationLeftAdjoint_obj_map,
              colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Category.id_comp]
          right_inv := fun f => by simp } }
Похожие утверждения