Commit 2024-10-19 19:08 37de4d77

View on Github →

feat(CategoryTheory/KanExtensions): Evaluating lan twice amounts to taking a colimit (#17531)

Estimated changes

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

added theorem CategoryTheory.Functor.ranObjObjIsoLimit_hom_π

added theorem CategoryTheory.Functor.ranObjObjIsoLimit_inv_π

added theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_hom

added theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_inv

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

added theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom

added theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv

added theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π

added theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π