[Merged by Bors] - feat(category_theory/idempotents): biproducts in idempotent completions #12333
Conversation
joelriou
changed the title
joelriou
added
the
awaiting-review
| { X := | ||
| { X := biproduct (λ j, (F j).X), | ||
| p := biproduct.map (λ j, (F j).p), | ||
| idempotence := begin |
There was a problem hiding this comment.
Maybe this ship has sailed, but idempotent would have been a better name than idempotence here: it's too hard in English to consistently come up with variants of words that mean "the property of being X", and it's easier to consistently just say "X".
There was a problem hiding this comment.
What about the shorter idem? (Similarly as factori[sz]ation is often shortened as fac in other places in mathlib.) May I do such a change slightly later in a separate PR?
There was a problem hiding this comment.
Sure, either idempotent or idem are good as far as I'm concerned. Yes -- no need to worry about it for this PR, but it would be nice if we eventually get to it.
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
If
Cis an additive category, thenkaroubi Cis an additive category.