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] - feat(category_theory/limits): preservation of zero morphisms #12068
Conversation
TwoFX
commented
Feb 16, 2022
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.
LGTM, probably @adamtopaz or @jcommelin ought to look too
F.map (0 : X ⟶ Y) = 0 := | ||
preserves_zero_morphisms.map_zero' _ _ | ||
|
||
lemma equivalence_preserves_zero_morphisms (F : C ≌ D) : preserves_zero_morphisms F.functor := |
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.
Is this a special case of something slightly more general, maybe that adjoints preserve zero morphisms? I don't know the maths here enough to be sure
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.
Earlier today I proved on paper that fully faithful is enough, and I'll generalize the proof soon. lt might also be true for adjoints, I'll think about that.
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 managed to prove it for adjoints :) I'll update the PR tomorrow. (Edit: Done.)
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
|
||
We provide the following results: | ||
* Left adjoints and right adjoints preserve zero morphisms; | ||
* full functors preserves zero morphisms; |
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.
* full functors preserves zero morphisms; | |
* full functors preserve zero morphisms; |
Pull request successfully merged into master. Build succeeded: |