Commit 2025-07-14 10:55 5dc620cc

View on Github →

feat(CategoryTheory/Limits/Shapes/End): functoriality of (co)ends (#27079) We define basic functoriality properties of the construction F ↦ end_ F, and bundle it as a functor whenever all ends exist. The same is done for coends.

Estimated changes

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

added theorem CategoryTheory.Limits.coend.map_comp

added theorem CategoryTheory.Limits.coend.map_id

added theorem CategoryTheory.Limits.coend.ι_map

added theorem CategoryTheory.Limits.end_.map_comp

added theorem CategoryTheory.Limits.end_.map_id

added theorem CategoryTheory.Limits.end_.map_π