Commit 2025-05-27 06:38 e76b292c

View on Github →

feat(CategoryTheory/Functor): more API for pointwise Kan extensions (#22474) Transport pointwise Kan extensions via isomorphisms/equivalences.

Estimated changes

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

added def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso'

added def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtOfIso'

added def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso'

added def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtOfIso'

added theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_equivalence

added theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso

added theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_natIso

added theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_of_equivalence

added theorem CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_equivalence

added theorem CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_iso

added theorem CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_natIso

added theorem CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_of_equivalence

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

deleted theorem CategoryTheory.Limits.hasLimitOfEquivalenceComp

added theorem CategoryTheory.Limits.hasLimit_of_equivalence_comp

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean