Commit 2025-11-01 00:46 8a3dc61b

View on Github →

feat(CategoryTheory): (Co)limits in preorders (#29253) Characterize (co)limits in preorders as glbs/lubs, plus some other instances.

Estimated changes

Modified Mathlib/CategoryTheory/Discrete/Basic.lean

added theorem CategoryTheory.Discrete.functor_ext

added theorem CategoryTheory.Discrete.id_def'

Modified Mathlib/CategoryTheory/Limits/Preorder.lean

added def CategoryTheory.Limits.IsInitial.orderBot

added def CategoryTheory.Limits.IsTerminal.orderTop

added def Preorder.coconePt_mem_upperBounds

added def Preorder.coneOfLowerBound

added theorem Preorder.conePt_mem_lowerBounds

added theorem Preorder.hasColimit_iff_hasLUB

added theorem Preorder.hasLimit_iff_hasGLB

modified def Preorder.isColimitBinaryCofan

added def Preorder.isColimitOfIsLUB

added theorem Preorder.isGLB_of_isLimit

modified def Preorder.isInitialBot

added theorem Preorder.isLUB_of_isColimit

modified def Preorder.isLimitBinaryFan

added def Preorder.isLimitOfIsGLB

modified def Preorder.isTerminalTop

added def Preorder.semilatticeInfOfIsLimitBinaryFan

added def Preorder.semilatticeSupOfIsColimitBinaryCofan

added theorem Preorder.upperBoundOfCocone