Commit 2024-04-20 18:50 32f9bf1b

View on Github →

feat(CategoryTheory): the left Kan extension functor (#12168) Given a functor F : C ⥤ D, we define the left Kan extension functor F.lan : (C ⥤ E) ⥤ (D ⥤ E) which sends a functor G : C ⥤ E to its left Kan extension along F. (This is a step towards the refactor of Lan/Ran in mathlib using the new API for Kan extensions of functors #10425.)

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.Functor.isIso_lanAdjunction_counit_app_iff

added theorem CategoryTheory.Functor.lanAdjunction_counit_app

added theorem CategoryTheory.Functor.lanAdjunction_unit

added theorem CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app

added theorem CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app

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

modified theorem CategoryTheory.Functor.HasLeftKanExtension.mk

modified theorem CategoryTheory.Functor.HasRightKanExtension.mk

modified def CategoryTheory.Functor.LeftExtension.mk

modified def CategoryTheory.Functor.RightExtension.mk

modified theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac

modified theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app

modified theorem CategoryTheory.Functor.hom_ext_of_isLeftKanExtension

modified theorem CategoryTheory.Functor.hom_ext_of_isRightKanExtension

added theorem CategoryTheory.Functor.isLeftKanExtension_iff_isIso

modified theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso

modified theorem CategoryTheory.Functor.isLeftKanExtension_of_iso

modified theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso

modified theorem CategoryTheory.Functor.isRightKanExtension_of_iso

modified theorem CategoryTheory.Functor.leftKanExtension_hom_ext

modified theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac

modified theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app

modified theorem CategoryTheory.Functor.rightKanExtension_hom_ext

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

added theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom

added theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app

added def CategoryTheory.Functor.LeftExtension.coconeAtFunctor

added def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso

added def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso

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

added theorem CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal

added theorem CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial