ranAdjunction — Mathlib

Lean4
/-- The right Kan extension functor `L.ran` is right adjoint to the
precomposition by `L`. -/
noncomputable def ranAdjunction : (whiskeringLeft C D H).obj L ⊣ L.ran :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun F G => (homEquivOfIsRightKanExtension (α := L.ranCounit.app G) _ F).symm
      homEquiv_naturality_right := fun {F G₁ G₂} β f ↦
        hom_ext_of_isRightKanExtension _ (L.ranCounit.app G₂) _ _
          (by
            ext X
            dsimp [homEquivOfIsRightKanExtension]
            rw [liftOfIsRightKanExtension_fac_app, NatTrans.comp_app, assoc]
            have h := congr_app (L.ranCounit.naturality f) X
            dsimp at h ⊢
            rw [h, liftOfIsRightKanExtension_fac_app_assoc])
      homEquiv_naturality_left_symm := fun {F₁ F₂ G} β f ↦
        by
        dsimp [homEquivOfIsRightKanExtension]
        rw [assoc] }
Похожие утверждения