Commit 2024-10-04 11:14 5ddd0ae2

View on Github →

feat(CategoryTheory): lemmas about descOfIsLeftKanExtension for pointwise left Kan extensions (+dual) (#17383)

Estimated changes

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

added def CategoryTheory.Functor.costructuredArrowMapCocone

added theorem CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app

added theorem CategoryTheory.Functor.pointwiseRightKanExtension_lift_app

added def CategoryTheory.Functor.structuredArrowMapCone