evaluationAdjunctionLeft — Mathlib

Lean4
/-- The adjunction showing that evaluation is a left adjoint. -/
@[simps! unit_app_app counit_app]
def evaluationAdjunctionLeft (c : C) : (evaluation _ _).obj c ⊣ evaluationRightAdjoint D c :=
  Adjunction.mkOfHomEquiv
    {
      homEquiv := fun F d =>
        { toFun := fun f => { app := fun _ => Pi.lift fun g => F.map g ≫ f }
          invFun := fun f => f.app _ ≫ Pi.π _ (𝟙 _)
          left_inv := fun f => by simp
          right_inv := by
            intro f
            ext x
            dsimp
            ext g
            simp only [NatTrans.naturality_assoc, evaluationRightAdjoint_obj_obj, evaluationRightAdjoint_obj_map,
              limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Category.comp_id] } }
Похожие утверждения