Commit 2025-06-22 16:54 ffbf9db0

feat(CategoryTheory/Functor/KanExtension): preservations of Kan extensions (#25753) Introduce a typeclass G.PreservesLeftKanExtension F L that asserts that a functor G preserves the left Kan extension of F along a functor L. Introduce a pointwise variant, and relate it to the non-pointwise version when pointwise extensions exist. Show that a functor that preserves the relevant colimits preserve pointwise left Kan extensions. Construct isomorphisms L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G) when G.PreservesLeftKanExtension F L holds. Also construct a functorial version, as an isomorphism L.lan ⋙ (whiskeringRight _ _ _).obj G ≅ (whiskeringRight _ _ _).obj G ⋙ L.lan. All results are dualised to right Kan extensions.