Commit 2024-02-11 09:45 a7e85ccb

View on Github →

feat(CategoryTheory): the typeclass Functor.HasRightKanExtension (#10384) This PR introduces the typeclass HasRightKanExtension L F which asserts the existence of a right Kan extension of a functor F along L. A chosen extension is obtained as rightKanExtension L F.

Estimated changes

Modified Mathlib/CategoryTheory/Equivalence.lean

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

added theorem CategoryTheory.Functor.HasLeftKanExtension.mk

added theorem CategoryTheory.Functor.HasRightKanExtension.mk

added theorem CategoryTheory.Functor.hasLeftExtension_iff_of_iso₁

added theorem CategoryTheory.Functor.hasLeftExtension_iff_of_iso₂

added theorem CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁

added theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₁

added theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₂

added theorem CategoryTheory.Functor.hasRightExtension_iff_postcomp₁

added def CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁

added def CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂

added theorem CategoryTheory.Functor.leftKanExtension_hom_ext

added def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁

added def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂

added theorem CategoryTheory.Functor.rightKanExtension_hom_ext