[Merged by Bors] - feat(LinearAlgebra/TensorProduct/Submodule): add some linear maps induced by multiplication for submodules#12498
Closed
[Merged by Bors] - feat(LinearAlgebra/TensorProduct/Submodule): add some linear maps induced by multiplication for submodules#12498
Conversation
1 task
erdOne
reviewed
Apr 29, 2024
erdOne
reviewed
May 1, 2024
Member
erdOne
left a comment
There was a problem hiding this comment.
I hope these work? These comments also apply to rTensorOne.
Collaborator
Author
Unfortunately, this file does not import the definition of |
eric-wieser
reviewed
May 7, 2024
Member
|
You can also use |
Collaborator
Author
No, there is no instance
Thanks. Now I'm satisfied (sort of) with current code. |
Member
|
Ok. Sorry again for the long wait! |
|
🚀 Pull request has been placed on the maintainer queue by erdOne. |
Member
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 26, 2024
…uced by multiplication for submodules (#12498) ... used in the definition of linearly disjointness. Let `R` be a commutative ring, `S` be an `R`-algebra (not necessarily commutative). Let `M` and `N` be `R`-submodules in `S`. - `Submodule.mulMap`: the natural `R`-linear map `M ⊗[R] N →ₗ[R] S` induced by the multiplication in `S`, whose image is `M * N` (`Submodule.mulMap_range`). - `Submodule.mulMap'`: the natural map `M ⊗[R] N →ₗ[R] M * N` induced by multiplication in `S`, which is surjective (`Submodule.mulMap'_surjective`). - `Submodule.lTensorOne`, `Submodule.rTensorOne`: the natural isomorphism between `i(R) ⊗[R] N` and `N`, resp. `M ⊗[R] i(R)` and `M`, induced by multiplication in `S`, here `i : R → S` is the structure map. They generalize `TensorProduct.lid` and `TensorProduct.rid`, as `i(R)` is not necessarily isomorphic to `R`. Note that we use `⊥ : Subalgebra R S` instead of `1 : Submodule R S`, since the map `R →ₗ[R] (1 : Submodule R S)` is not defined directly in mathlib yet. - `Submodule.mulLeftMap`: if `m : ι → M` is a family of elements, then there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`. - `Submodule.mulRightMap`: if `n : ι → N` is a family of elements, then there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
kbuzzard
pushed a commit
that referenced
this pull request
Jun 26, 2024
…uced by multiplication for submodules (#12498) ... used in the definition of linearly disjointness. Let `R` be a commutative ring, `S` be an `R`-algebra (not necessarily commutative). Let `M` and `N` be `R`-submodules in `S`. - `Submodule.mulMap`: the natural `R`-linear map `M ⊗[R] N →ₗ[R] S` induced by the multiplication in `S`, whose image is `M * N` (`Submodule.mulMap_range`). - `Submodule.mulMap'`: the natural map `M ⊗[R] N →ₗ[R] M * N` induced by multiplication in `S`, which is surjective (`Submodule.mulMap'_surjective`). - `Submodule.lTensorOne`, `Submodule.rTensorOne`: the natural isomorphism between `i(R) ⊗[R] N` and `N`, resp. `M ⊗[R] i(R)` and `M`, induced by multiplication in `S`, here `i : R → S` is the structure map. They generalize `TensorProduct.lid` and `TensorProduct.rid`, as `i(R)` is not necessarily isomorphic to `R`. Note that we use `⊥ : Subalgebra R S` instead of `1 : Submodule R S`, since the map `R →ₗ[R] (1 : Submodule R S)` is not defined directly in mathlib yet. - `Submodule.mulLeftMap`: if `m : ι → M` is a family of elements, then there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`. - `Submodule.mulRightMap`: if `n : ι → N` is a family of elements, then there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
dagurtomas
pushed a commit
that referenced
this pull request
Jul 2, 2024
…uced by multiplication for submodules (#12498) ... used in the definition of linearly disjointness. Let `R` be a commutative ring, `S` be an `R`-algebra (not necessarily commutative). Let `M` and `N` be `R`-submodules in `S`. - `Submodule.mulMap`: the natural `R`-linear map `M ⊗[R] N →ₗ[R] S` induced by the multiplication in `S`, whose image is `M * N` (`Submodule.mulMap_range`). - `Submodule.mulMap'`: the natural map `M ⊗[R] N →ₗ[R] M * N` induced by multiplication in `S`, which is surjective (`Submodule.mulMap'_surjective`). - `Submodule.lTensorOne`, `Submodule.rTensorOne`: the natural isomorphism between `i(R) ⊗[R] N` and `N`, resp. `M ⊗[R] i(R)` and `M`, induced by multiplication in `S`, here `i : R → S` is the structure map. They generalize `TensorProduct.lid` and `TensorProduct.rid`, as `i(R)` is not necessarily isomorphic to `R`. Note that we use `⊥ : Subalgebra R S` instead of `1 : Submodule R S`, since the map `R →ₗ[R] (1 : Submodule R S)` is not defined directly in mathlib yet. - `Submodule.mulLeftMap`: if `m : ι → M` is a family of elements, then there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`. - `Submodule.mulRightMap`: if `n : ι → N` is a family of elements, then there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
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
4 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.
... used in the definition of linearly disjointness.
Let
Rbe a commutative ring,Sbe anR-algebra (not necessarily commutative).Let
MandNbeR-submodules inS.Submodule.mulMap: the naturalR-linear mapM ⊗[R] N →ₗ[R] Sinduced by the multiplication in
S, whose image isM * N(Submodule.mulMap_range).Submodule.mulMap': the natural mapM ⊗[R] N →ₗ[R] M * Ninduced by multiplication in
S, which is surjective (Submodule.mulMap'_surjective).Submodule.lTensorOne,Submodule.rTensorOne: the natural isomorphism betweeni(R) ⊗[R] NandN, resp.M ⊗[R] i(R)andM, induced by multiplication inS,here
i : R → Sis the structure map. They generalizeTensorProduct.lidand
TensorProduct.rid, asi(R)is not necessarily isomorphic toR.Note that we use
⊥ : Subalgebra R Sinstead of1 : Submodule R S, since the mapR →ₗ[R] (1 : Submodule R S)is not defined directly in mathlib yet.Submodule.mulLeftMap: ifm : ι → Mis a family of elements, then there is anR-linear mapfrom
ι →₀ NtoSwhich maps{ n_i }to the sum ofm_i * n_i.Submodule.mulRightMap: ifn : ι → Nis a family of elements, then there is anR-linear mapfrom
ι →₀ MtoSwhich maps{ m_i }to the sum ofm_i * n_i.discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312498.20some.20linear.20maps.20induced.20by.20mul.2E.20for.20submodules