tensoring up a submodule

Stream: Is there code for X?

[Kevin Buzzard]

If $R$ is a commutative ring and $M,N$ are $R$-modules, then there's a function from Submodule N to Submodule M ⊗[R] N` sending a submodule $P$ of $N$ to the image of $M\otimes P$ in $M\otimes N$ (note that the map $M\otimes P\to M\otimes N$ might not be injective; this is related to flatness). Do we have this function?

I need this construction to state some results of the form "under certain circumstances, tensoring commutes with restricted product". Here on the LHS we have "M tensor (the restricted product)" and on the RHS we have "the restricted product of (M tensor the factors)" but the way restricted products are set up we take the restricted product of a family of pairs consisting of an object and a subobject, so this is why it would be convenient to tensor up a submodule and get a submodule.

import Mathlib

variable {ι : Type*}
variable {R : ι → Type*}
variable {ℱ : Filter ι}

variable {S : ι → Type*} -- subobject type
variable [Π i, SetLike (S i) (R i)]
variable {B : Π i, S i}

open scoped RestrictedProduct TensorProduct

variable {A : Type*} [CommRing A]

-- In open PR #25715
-- restricted product of addcommgroups is an addcommgroup
instance [Π i, AddCommGroup (R i)] [∀ i, AddSubgroupClass (S i) (R i)]:
    AddCommGroup (Πʳ i, [R i, B i]_[ℱ]) where
  __ := inferInstanceAs (AddGroup (Πʳ i, [R i, B i]_[ℱ]))
  add_comm a b := by ext i; simp [add_comm]

-- when #25715 lands we'll be able to change these to AddCommMonoid
-- restricted product of A-modules is an A-module
instance [Π i, AddCommGroup (R i)] [∀ i, Module A (R i)]
    -- next line is how we do "SubmoduleClass"
    [∀ i, AddSubgroupClass (S i) (R i)] [∀ i, SMulMemClass (S i) A (R i)] :
    Module A (Πʳ i, [R i, B i]_[ℱ]) := sorry -- this is done and not hard

-- The question I asked above:
def basechange (M : Type*) {N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    (P : Submodule A N) : Submodule A (M ⊗[A] N) := sorry

-- this now compiles
def RestrictedProduct.tensor_comm' [Π i, AddCommGroup (R i)]
    [∀ i, Module A (R i)] {C : Π i, Submodule A (R i)}
    {M : Type*} [AddCommGroup M] [Module A M] [Module.FinitePresentation A M] :
    M ⊗[A] (Πʳ i, [R i, C i]_[ℱ]) ≃ₗ[A] Πʳ i, [M ⊗[A] R i, basechange M (C i)]_[ℱ] := sorry

[Kenny Lau]

@Kevin Buzzard you would write it as LinearMap.range (P.subtype.lTensor M), I don't think it's in the library, but there's Submodule.baseChange for when M is an A-algebra

[Kevin Buzzard]

Oh nice find! Yeah this is related to, but not quite, what I want. Maybe I'll just go with the LinearMap.range.

[Eric Wieser]

docs#Submodule.map2 ?

[Eric Wieser]

Well, docs#Submodule.map₂ but zulip refuses

[Eric Wieser]

Nevermind, I skim read too much, that tensors a submodule with another one

[Eric Wieser]

Arguably your def should be called lTensor not baseChange, since it isn't using Ring M

[Antoine Chambert-Loir]

By the way, in #26717, @María Inés de Frutos Fernández and I define DirectedSystem.rTensor and make use of the right-exactness of the tensor product proven by docs#TensorProduct.directLimitLeft