lanAdjunction — Mathlib

Lean4
/-- The left Kan extension functor `L.Lan` is left adjoint to the precomposition by `L`. -/
noncomputable def lanAdjunction : L.lan ⊣ (whiskeringLeft C D H).obj L :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun F G => homEquivOfIsLeftKanExtension _ (L.lanUnit.app F) G
      homEquiv_naturality_left_symm := fun {F₁ F₂ G} f α =>
        hom_ext_of_isLeftKanExtension _ (L.lanUnit.app F₁) _ _
          (by
            ext X
            dsimp [homEquivOfIsLeftKanExtension]
            rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
            have h := congr_app (L.lanUnit.naturality f) X
            dsimp at h ⊢
            rw [← h, assoc, descOfIsLeftKanExtension_fac_app])
      homEquiv_naturality_right := fun {F G₁ G₂} β f =>
        by
        dsimp [homEquivOfIsLeftKanExtension]
        rw [assoc] }
Похожие утверждения