Conversation
MultilinearMap and DirectSum, and between PiTensorProduct and DirectSumMultilinearMap and DirectSum, and between PiTensorProduct and DirectSum
eric-wieser
reviewed
Mar 9, 2024
eric-wieser
reviewed
Mar 9, 2024
eric-wieser
reviewed
Mar 9, 2024
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
reviewed
Mar 23, 2024
eric-wieser
reviewed
Mar 23, 2024
eric-wieser
reviewed
Oct 27, 2024
eric-wieser
reviewed
Oct 28, 2024
| (by | ||
| ext f x | ||
| dsimp | ||
| erw [MultilinearMap.dfinsuppFamily_single, DirectSum.toModule_lof] |
Member
There was a problem hiding this comment.
These erws are my fault, and are because we are abusing defeq by using MultilinearMap.dfinsuppFamilyₗ instead of duplicating the construction for directSum. Probably we should spin out a PR to do that, where all the defs and lemmas are one-liners in terms of the dfinsupp versions.
Member
There was a problem hiding this comment.
I've done that in this PR for now, but will come back and split later.
eric-wieser
reviewed
Nov 3, 2024
4 tasks
Collaborator
|
This pull request has conflicts, please merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 4, 2025
Adds a basis for MulilinearMap given bases for the domain and codomain. This PR builds upon work started in #25141 toward #11155. Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Eric Wieser <efw@google.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>
Contributor
|
Thanks to @morrison-daniel I believe all of this work is now in master and we can close this PR 🎉 In particular I highlight the PRs #32456 and #32450 and can point to: etc |
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
8 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.
This does three things:
MultilinearMap.fromDirectSumEquiv(inLinearAlgebra/MultilinearMap/DirectSum.lean) calculatesMultilinearMaps on a family ofDirectSums. More precisely, ifιis aFintype, ifκ iis a family of types indexed byιand we have aR-moduleM i jfor everyi : ιandj : κ i, this is the linear equivalence betweenΠ p : (i : ι) → κ i, MultilinearMap R (fun i ↦ M i (p i)) M'andMultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M'.PiTensorProduct.directSum(inLinearAlgebra/DirectSum/PiTensorProduct.lean): the distributivity property of aPiTensorProductwith respect toDirectSums in all its arguments.finsuppPiTensorProduct(inLinearAlgebra/DirectSum/Finsupp.lean): Ifιis aFintype,κ iis a family of types indexed byιandM iis a family ofR-modules indexed byι, then the tensor product of the familyκ i →₀ M iis linearly equivalent to∏ i, κ i →₀ ⨂[R] i, M i.PiTensorProduct#11152MultilinearMap.dfinsuppFamilyandMultilinearMap.piFamily#17881LinearMap.compMultilinear#17932