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] - refactor(category_theory): make has_zero_object a Prop #13517
Conversation
jcommelin
commented
Apr 19, 2022
•
edited by github-actions
bot
edited by github-actions
bot
- depends on: [Merged by Bors] - feat(category_theory/limits): add characteristic predicate for zero objects #13511
This PR/issue depends on: |
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! Just one minor comment for you to consider.
bors d+
@@ -164,8 +166,9 @@ is the same as the zero functor. | |||
-/ | |||
noncomputable | |||
def homology_functor_succ_single₀ (n : ℕ) : single₀ V ⋙ homology_functor V _ (n+1) ≅ 0 := |
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.
Could you also add a is_zero
instance based on this isomorphisms (and its variant(s) below)?
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 will do this in a follow-up PR
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Build failed (retrying...): |
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |