Commit 2026-01-26 16:58 58d84683

View on Github →

chore(CategoryTheory/Limits): add IsColimit.nonempty_isColimit_iff_isIso_desc and golf (#34237) We also fix the name of Cofan.isColimit_iff_isIso_sigmaDesc and turn the iff around.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

added theorem CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc

added theorem CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_lift

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

deleted theorem CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc

added theorem CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc

added def CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift

added theorem CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean