Commit 2024-05-24 09:21 0b29d6a8

View on Github →

feat(CategoryTheory): transport Kan extensions via equivalences (#12785) In this PR, it is shown that left/right Kan extensions of functors F : C ⥤ H along a functor L : C ⥤ D are compatible with changing the functors F and L by isomorphic functors, by the precomposition with an equivalence G : C' ⥤ C, and postcomposition with an equivalence D ⥤ D'.

Estimated changes

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

added def CategoryTheory.Functor.LeftExtension.postcomp₁

added def CategoryTheory.Functor.LeftExtension.precomp

added def CategoryTheory.Functor.RightExtension.postcomp₁

added def CategoryTheory.Functor.RightExtension.precomp

added theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso₂

added theorem CategoryTheory.Functor.isLeftKanExtension_iff_postcomp₁

added theorem CategoryTheory.Functor.isLeftKanExtension_iff_precomp

added theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso₂

added theorem CategoryTheory.Functor.isRightKanExtension_iff_postcomp₁

added theorem CategoryTheory.Functor.isRightKanExtension_iff_precomp

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

added def CategoryTheory.Limits.IsInitial.equivOfIso

added def CategoryTheory.Limits.IsTerminal.equivOfIso