Commit 2025-04-09 12:22 27e272c5

View on Github →

feat: the category over a terminal object (#23702) From Toric

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

added def CategoryTheory.Over.equivalenceOfIsTerminal

added def CategoryTheory.Under.equivalenceOfIsInitial

Modified Mathlib/CategoryTheory/Comma/Over/Pullback.lean

modified def CategoryTheory.Over.forgetAdjStar

modified def CategoryTheory.Over.star

added def CategoryTheory.Under.costar

added def CategoryTheory.Under.costarAdjForget

deleted def CategoryTheory.Under.equivalenceOfIsInitial