feat(LinearAlgebra/DirectSum/Finsupp) : tensor products of finsupp functions #10824
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
eric-wieser
reviewed
Feb 21, 2024
| variable {ι : Type*} [DecidableEq ι] | ||
|
|
||
| /-- The tensor product of `i →₀ M` and `N` is linearly equivalent to `i →₀ M ⊗[R] N` -/ | ||
| noncomputable def Finsupp.rTensor : |
There was a problem hiding this comment.
Arguably this should be called TensorProduct.finsuppLeft for consistency with TensorProduct.directSumLeft and TensorProduct.prodLeft, and similarly for Right
There was a problem hiding this comment.
(I had to check for the actual meaning of “Arguably” ! — it doesn't mean one can argue, and indeed, i won't…)
There was a problem hiding this comment.
In the initial file, finsuppTensorProductFinsupp is in the root name space. Is this reasonable? (but I don't want to have to track at all instances…)
eric-wieser
reviewed
Feb 21, 2024
added 10 commits
February 21, 2024 17:58
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
AntoineChambert-Loir
added
the
awaiting-review
|
I am presently trying to prove the multiplicativity. |
alreadydone
reviewed
Feb 23, 2024
Change i to iota Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
|
!bench |
|
Here are the benchmark results for commit cfa238f. Benchmark Metric Change
================================================================
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp instructions 243.8% |
|
Is it possible to split the changes in |
|
Not it's not really possible, that's the whole goal of having these results |
It's best if the changes in |
acmepjz
reviewed
Mar 23, 2024
leanprover-community-mathlib4-bot
added
the
merge-conflict
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.
leanprover-community-mathlib4-bot
removed
the
merge-conflict
Louddy
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.
erdOne
reviewed
Apr 20, 2024
Comment on lines
+108
to
+142
| /- | ||
| lemma TensorProduct.map_isLinearMap' | ||
| [Module S M] [IsScalarTower R S M] [Module S N] [IsScalarTower R S N] | ||
| {P : Type*} [AddCommMonoid P] [Module R P] | ||
| {Q : Type*} [AddCommMonoid Q] [Module R Q] | ||
| (e : M →ₗ[S] N) (f : P →ₗ[R] Q) : | ||
| IsLinearMap S (TensorProduct.map (e.restrictScalars R) f) where | ||
| map_add := LinearMap.map_add _ | ||
| map_smul := fun s t ↦ by | ||
| induction t using TensorProduct.induction_on with | ||
| | zero => simp | ||
| | add x y hx hy => | ||
| simp only [smul_add, map_add] at hx hy ⊢ | ||
| simp only [hx, hy] | ||
| | tmul m p => | ||
| rw [smul_tmul'] | ||
| simp only [map_tmul, coe_restrictScalars, map_smul] | ||
| rfl | ||
| -/ | ||
|
|
||
| /- lemma TensorProduct.congr_isLinearMap' | ||
| [Module S M] [IsScalarTower R S M] [Module S N] [IsScalarTower R S N] | ||
| {P : Type*} [AddCommMonoid P] [Module R P] | ||
| {Q : Type*} [AddCommMonoid Q] [Module R Q] | ||
| (e : M ≃ₗ[S] N) (f : P ≃ₗ[R] Q) : | ||
| IsLinearMap S (TensorProduct.congr (e.restrictScalars R) f) := | ||
| TensorProduct.map_isLinearMap' e.toLinearMap f.toLinearMap -/ | ||
|
|
||
| /- | ||
| lemma LinearEquiv.rTensor_isLinearMap' | ||
| [Module S M] [IsScalarTower R S M] [Module S N] [IsScalarTower R S N] | ||
| (P : Type*) [AddCommMonoid P] [Module R P] (e : M ≃ₗ[S] N) : | ||
| IsLinearMap S (LinearEquiv.rTensor P (e.restrictScalars R)) := | ||
| TensorProduct.map_isLinearMap' e.toLinearMap _ | ||
| -/ |
There was a problem hiding this comment.
Are these supposed to be here?
And is it possible to split the PR into three, considering there are three new files added?
There was a problem hiding this comment.
I'll do that.
There was a problem hiding this comment.
I suppose this PR can be closed now.
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.
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.
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] NMonoid algebras
MonoidAlgebra.rTensorAlgEquiv: the tensor product ofMonoidAlgebra M αwithNisR-linearly equivalent toMonoidAlgebra (M ⊗[R] N) αMonoidAlgebra.scalarRTensorAlgEquiv, the tensor product ofMonoidAlgebra R αwithNisR-linearly equivalent toMonoidAlgebra N αCase of MvPolynomial
These functions apply to
MvPolynomial, one can defineA proposition in this direction is given in
LinearAlgebra/TensorProduct/MvPolynomialCase of
PolynomialPolynomialis a structure containing aFinsupp, so these functionscan't be applied directly to
Polynomial.Some linear equivs need to be added to mathlib for that.
A proposition in this direction is given in
LinearAlgebra.TensorProduct.PolynomialTODO
reprove
TensorProduct.finsuppLeft'using existing heterobasic version ofTensorProduct.congralign what has been done for monoid agebras with what is missing for MvPolynomial or Polynomial