Commit 2024-10-25 21:52 989ad277

View on Github →

feat(CategoryTheory/KanExtension): Composing lan with colim (#17355)

Estimated changes

Modified Mathlib/CategoryTheory/Functor/Const.lean

added def CategoryTheory.Functor.constCompWhiskeringLeftIso

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

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

added def CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension

added def CategoryTheory.Functor.isLimitConeOfIsRightKanExtension

added theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π

added theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π

added theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom

added theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv