Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 08:17 4813b73a

View on Github →

feat(category_theory/adjunction): general adjoint functor theorem (#4885) A proof of the general adjoint functor theorem. This PR also adds an API for wide equalizers (essentially copied from the equalizer API), as well as results relating adjunctions to (co)structured arrow categories and weakly initial objects. I can split this into smaller PRs if necessary?

Estimated changes