Commit 2026-05-28 11:18 4e174f59

View on Github →

chore(CategoryTheory/Functor): pointwise Kan extensions under isomorphisms (#39883) We already have the versions for HasPointwiseLeftKanExtensionAt in the L argument, this PR adds the version for isomorphisms in both functor arguments. We also add the variants for HasPointwiseLeftKanExtension.

Estimated changes

Modified Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

added theorem CategoryTheory.Functor.HasPointwiseLeftKanExtension.of_iso

added theorem CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt.of_natIso

added theorem CategoryTheory.Functor.HasPointwiseRightKanExtension.of_iso

added theorem CategoryTheory.Functor.HasPointwiseRightKanExtensionAt.of_natIso

modified theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_natIso

added theorem CategoryTheory.Functor.hasPointwiseLeftKanExtension_iff_of_iso

modified theorem CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_natIso

added theorem CategoryTheory.Functor.hasPointwiseRightKanExtension_iff_of_iso