Commit 2024-02-08 08:31 a1d9afe7

View on Github →

feat(CategoryTheory/Functor): definition of Kan extensions (#10195) This PR introduces basic definitions for Kan extensions of functors. It prepares for future development of derived functors and a refactor of the file CategoryTheory.Limits.KanExtension.

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Functor.LeftExtension.mk

added def CategoryTheory.Functor.RightExtension.mk

added theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac

added theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app

added theorem CategoryTheory.Functor.hom_ext_of_isLeftKanExtension

added theorem CategoryTheory.Functor.hom_ext_of_isRightKanExtension

added theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso

added theorem CategoryTheory.Functor.isLeftKanExtension_of_iso

added theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso

added theorem CategoryTheory.Functor.isRightKanExtension_of_iso

added theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac

added theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Whiskering.lean