[Merged by Bors] - feat(category_theory): preadditive binary biproducts #2747
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Originally, I for some reason believed that in a preadditve category, every binary biproduct is automatically a preadditive binary biproduct. This is of course not true, which makes this PR a bit less nice than I had originally hoped, but I hope it's fine. This PR introduces two |
Also, move everything over to biproducts.lean
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
May 22, 2020
This PR introduces "preadditive binary biproducts", which correspond to the second definition of biproducts given in #2177. * Preadditive binary biproducts are binary biproducts. * In a preadditive category, a binary product is a preadditive binary biproduct. * This directly implies that `AddCommGroup` has preadditive binary biproducts. The existence of binary coproducts in `AddCommGroup` is then a consequence of abstract nonsense.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
cipher1024
pushed a commit
to cipher1024/mathlib
that referenced
this pull request
Mar 15, 2022
…unity#2747) This PR introduces "preadditive binary biproducts", which correspond to the second definition of biproducts given in leanprover-community#2177. * Preadditive binary biproducts are binary biproducts. * In a preadditive category, a binary product is a preadditive binary biproduct. * This directly implies that `AddCommGroup` has preadditive binary biproducts. The existence of binary coproducts in `AddCommGroup` is then a consequence of abstract nonsense.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces "preadditive binary biproducts", which correspond to the second definition of biproducts given in #2177.
AddCommGrouphas preadditive binary biproducts. The existence of binary coproducts inAddCommGroupis then a consequence of abstract nonsense.