New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - lint(category_theory/equivalence): docstring and a module doc #4495
Conversation
TwoFX
commented
Oct 7, 2020
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks a lot for writing this module doc!
src/category_theory/equivalence.lean
Outdated
notion of "sameness" of categories than the stricter isomorphims of categories. | ||
|
||
Our definition of equivalence includes an additional axiom, and the resulting notion of equivalence | ||
is called a "(half-)adjoint equivalence". We show that, given an equivalence in the sense of the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Most practicing mathematicians know what an equivalence is, and what an adjunction is. But I guess that many don't realise that there are equivalences that are not adjunctions. (I only realised this when I formalised them 😀)
Would you mind explaining in a bit more detail what the subtleties are? (Maybe part of this should even go in the docstring of equivalence, or it could have a pointer to this module docstring.)
For example, I don't know what the difference is between a half-adjoint equivalence
and an adjoin equivalence
. And which one does mathlib have?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried to expand the explanation. Is it a bit clearer now?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Pull request successfully merged into master. Build succeeded: |