Commit 2025-04-15 16:43 fad8b5dc

View on Github →

feat(CategoryTheory/Limits): preservation of multicoequalizers (#22205)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Shapes/Multiequalizer.lean

added def CategoryTheory.Limits.Multicofork.isColimitMapEquiv

added def CategoryTheory.Limits.Multicofork.map

added def CategoryTheory.Limits.MultispanIndex.map

added def CategoryTheory.Limits.MultispanIndex.multispanMapIso

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

added def CategoryTheory.Limits.Multicofork.ext