Lean4
/-- If `L : (Cᵒᵖ ⥤ Type max v₁ v₂) ⥤ ℰ` is a pointwise left Kan extension
of a functor `A : C ⥤ ℰ` along the Yoneda embedding,
then `L` is a left adjoint of `restrictedULiftYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type max v₁ v₂` -/
noncomputable def uliftYonedaAdjunction : L ⊣ restrictedULiftYoneda.{max w v₁} A :=
Adjunction.mkOfHomEquiv
{ homEquiv := restrictedULiftYonedaHomEquiv L α
homEquiv_naturality_left_symm {P Q X} f
g := by
apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext
intro p
have hfg :=
(Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).comp_homEquiv_symm
((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) p
have hg :=
(Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q).comp_homEquiv_symm
((restrictedULiftYonedaHomEquiv' A Q X).symm g) ((CostructuredArrow.map f).obj p)
dsimp at hfg hg
dsimp [restrictedULiftYonedaHomEquiv]
simp only [assoc, hfg, ← L.map_comp_assoc, hg, restrictedULiftYonedaHomEquiv'_symm_app_naturality_left]
homEquiv_naturality_right {P X Y} f
g :=
by
have := @IsColimit.homEquiv_symm_naturality (h := Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)
dsimp at this
apply (restrictedULiftYonedaHomEquiv L α P Y).symm.injective
apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext
intro
simp [restrictedULiftYonedaHomEquiv, restrictedULiftYonedaHomEquiv'_symm_naturality_right, this] }
