[Merged by Bors] - feat: port CategoryTheory.Monoidal.Linear #3112
Conversation
mo271
commented
Mar 26, 2023
mo271
commented
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Parcly-Taxel
added
the
awaiting-review
|
Thanks! |
github-actions
bot
added
ready-to-merge
|
bors r- |
|
Canceled. |
|
|
||
| variable (C : Type _) [Category C] [Preadditive C] [Linear R C] | ||
|
|
||
| variable [MonoidalCategory C] [MonoidalPreadditive C] |
There was a problem hiding this comment.
Since this [MonoidalPreadditive C] is not used in the definition of the class MonoidalLinear, could you remove this variable declaration and add it to a section where is is needed? (I guess it is still needed somewhere).
There was a problem hiding this comment.
Sure, I will have a look tomorrow!
There was a problem hiding this comment.
You have a porting note saying that you removed an argument in a theorem because it was unused. This is weird because the lean3 linter should have complained as well in the original file. So I checked the lean3 file and indeed, we can remove the MonoidalPreadditive C hypothesis when creating the class, and then the argument becomes unused in the theorem. So you did the right thing.
But now we have that variable declaration at the head of the file, which makes the reader think that it is used everywhere, but only a subset of the results actually use it. In particular, the class definition just below does not use it. So it would be better for readability to declare the variable [MonoidalPreadditive C] where it is actually needed.
There was a problem hiding this comment.
Actually now that I read the file docstring more carefully, it looks like we want to force the MonoidalLinear class to take a MonoidalPreadditive C argument: "A monoidal category is MonoidalLinear R if it is monoidal preadditive and tensor product of morphisms is R-linear in both factors.".
I am not familiar with the relevant math.
There was a problem hiding this comment.
ok, I think that makes sense and gave it a try.
There was a problem hiding this comment.
ok, I think that makes sense and gave it a try.
|
bors d+ |
|
✌️ mo271 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Is there a way for me to see it? |
|
Thanks again! |
github-actions
bot
added
ready-to-merge
Co-authored-by: Moritz Firsching <firsching@google.com>
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
