Commit 2025-06-15 14:52 0e9bcbf7

View on Github →

chore(CategoryTheory/Limits/Shape/End): define coends (#25763) The content of CategoryTheory/Limits/Shapes/End was not dualized, so only ends where defined, but not coends. This PR dualizes the content of the file: we introduce Cowedges as special kinds of Multicoforks, and define the coend_ F as the colimit of a canonical cowedge we can build from F : Jᵒᵖ ⥤ J ⥤ C. Also, we rename CategoryTheory.Limits.hom_ext to CategoryTheory.Limits.end_.hom_ext.

Estimated changes

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

added def CategoryTheory.Limits.Cowedge.IsColimit.desc

added theorem CategoryTheory.Limits.Cowedge.IsColimit.hom_ext

added theorem CategoryTheory.Limits.Cowedge.IsColimit.π_desc

added theorem CategoryTheory.Limits.Cowedge.condition

added theorem CategoryTheory.Limits.Cowedge.mk_π

added theorem CategoryTheory.Limits.coend.condition

added theorem CategoryTheory.Limits.coend.hom_ext

added theorem CategoryTheory.Limits.coend.ι_desc

added theorem CategoryTheory.Limits.end_.hom_ext

deleted theorem CategoryTheory.Limits.hom_ext

added def CategoryTheory.Limits.multispanIndexCoend

added def CategoryTheory.Limits.multispanShapeCoend

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

added def CategoryTheory.Limits.Multicofork.IsColimit.desc

added theorem CategoryTheory.Limits.Multicofork.IsColimit.fac