Commit 2025-04-28 07:13 c7a52c02

View on Github →

feat: sliced adjoint functors (#24388) This is Proposition 3.8 in https://ncatlab.org/nlab/show/adjoint+functor. From Toric

Estimated changes

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

added def CategoryTheory.Over.postAdjunctionRight

added def CategoryTheory.Under.postAdjunctionLeft

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

added def CategoryTheory.Over.postAdjunctionLeft

added def CategoryTheory.Under.postAdjunctionRight