[Merged by Bors] - feat(Mathlib/LinearAlgebra/DirectSum/Finsupp): tensor products of finsupp sums#11635
Closed
AntoineChambert-Loir wants to merge 7 commits intomasterfrom
Closed
[Merged by Bors] - feat(Mathlib/LinearAlgebra/DirectSum/Finsupp): tensor products of finsupp sums#11635AntoineChambert-Loir wants to merge 7 commits intomasterfrom
AntoineChambert-Loir wants to merge 7 commits intomasterfrom
Conversation
Collaborator
|
Thank you very much! It looks good for me. |
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit b400dac. Benchmark Metric Change
================================================================
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp instructions 244.6% |
alreadydone
reviewed
Mar 27, 2024
Contributor
alreadydone
left a comment
There was a problem hiding this comment.
Largely LGTM but I might come back to golf some proofs ...
Collaborator
Author
|
@alreadydone, is there something else that you would want me to add or change? |
alreadydone
reviewed
Apr 2, 2024
Contributor
alreadydone
left a comment
There was a problem hiding this comment.
Sorry for the delay, I'll get back to this tomorrow.
alreadydone
approved these changes
Apr 3, 2024
Contributor
There was a problem hiding this comment.
I've done the golfs here. I made the defs finsuppLeft etc. shorter but it may make it harder for the reader, so feel free to adopt the changes that you think is appropriate. I gave two proofs for finsuppLeft_apply_tmul etc. and you're free to adopt either.
It's a bit weird that finsuppLeft etc. have no explicit argument, but LGTM.
Collaborator
Author
|
Thanks for the shorter versions, I'll use them, and I'm OK to make the arguments of finsuppLeft explicit, in accordance with what is done for docs#TensorProduct.directSumLeft |
Contributor
|
Can you please fix the compile errors (which probably results from the implicitness changes)? Thanks! |
Collaborator
Author
|
I had not noticed that there were errors left, sorry. I make the necessary adjustments at once. |
Contributor
|
Thanks 🎉 |
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Contributor
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 8, 2024
…supp sums (#11635) ## Modules * `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` * `TensorProduct.finsuppRight`, the tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppLeft'`, if `M` is an `S`-module, then the tensor product of `ι →₀ M` and `N` is `S`-linearly equivalent to `ι →₀ M ⊗[R] N` This is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials. It has been split because this part is reasonably sound, while the three other files are more like propositions.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
…supp sums (#11635) ## Modules * `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` * `TensorProduct.finsuppRight`, the tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppLeft'`, if `M` is an `S`-module, then the tensor product of `ι →₀ M` and `N` is `S`-linearly equivalent to `ι →₀ M ⊗[R] N` This is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials. It has been split because this part is reasonably sound, while the three other files are more like propositions.
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
…supp sums (#11635) ## Modules * `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` * `TensorProduct.finsuppRight`, the tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppLeft'`, if `M` is an `S`-module, then the tensor product of `ι →₀ M` and `N` is `S`-linearly equivalent to `ι →₀ M ⊗[R] N` This is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials. It has been split because this part is reasonably sound, while the three other files are more like propositions.
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
…supp sums (#11635) ## Modules * `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` * `TensorProduct.finsuppRight`, the tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppLeft'`, if `M` is an `S`-module, then the tensor product of `ι →₀ M` and `N` is `S`-linearly equivalent to `ι →₀ M ⊗[R] N` This is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials. It has been split because this part is reasonably sound, while the three other files are more like propositions.
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
…supp sums (#11635) ## Modules * `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` * `TensorProduct.finsuppRight`, the tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppLeft'`, if `M` is an `S`-module, then the tensor product of `ι →₀ M` and `N` is `S`-linearly equivalent to `ι →₀ M ⊗[R] N` This is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials. It has been split because this part is reasonably sound, while the three other files are more like propositions.
1 task
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
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.
Modules
TensorProduct.finsuppLeft, the tensor product ofι →₀ MandNis linearly equivalent toι →₀ M ⊗[R] NTensorProduct.finsuppScalarLeft, the tensor product ofι →₀ RandNis linearly equivalent toι →₀ NTensorProduct.finsuppRight, the tensor product ofMandι →₀ Nis linearly equivalent toι →₀ M ⊗[R] NTensorProduct.finsuppLeft', ifMis anS-module, then the tensor product ofι →₀ MandNisS-linearly equivalent toι →₀ M ⊗[R] NThis is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials.
It has been split because this part is reasonably sound, while the three other files are more like propositions.