Cancel in composition of base change

Stream: Is there code for X?

[Christian Merten]

Is there a lemma on cancelling the intermediate base change in a composition of base changes, i.e. something like this:

import Mathlib

open TensorProduct

variable (R S M N : Type*) [CommRing R] [CommRing S] [Algebra R S]
  [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N] :

instance : Module S (M ⊗[R] N) := sorry

def baseChangeCancel : (M ⊗[R] S) ⊗[S] N ≃ₗ[S] M ⊗[R] N := sorry

If M is a S-algebra, this can be deduced from docs#IsBaseChange.comp . Note that also the Module instance is not inferred, here I want to act on M ⊗[R] N by acting on N.

[Adam Topaz]

I'm quite sure we have this.

[Adam Topaz]

hmmm... maybe not.

[Eric Wieser]

In mathlib, the module with the larger base has to be on the left of the tensor product

[Eric Wieser]

So Module S (N ⊗[R] M) should be found automatically there

[Eric Wieser]

And the def you want would then be

def baseChangeCancel :
  N ⊗[S] (S ⊗[R] M) ≃ₗ[S] N ⊗[R] M := sorry

[Eric Wieser]

I think this follows from docs#TensorProduct.AlgebraTensorModule.assoc ?

[Christian Merten]

Eric Wieser said:

I think this follows from docs#TensorProduct.AlgebraTensorModule.assoc ?

Probably you meant docs#TensorProduct.assoc (The algebra version only applies if N is a S-Algebra), but still I am not sure how I proceed with this, since docs#TensorProduct.assoc works with three modules over the same ring.

[Christian Merten]

Nvmd, I think you meant docs#TensorProduct.AlgebraTensorModule.assoc and this looks more promising. I clicked on your link earlier and it gave me a 404, but I think you edited your message. Thanks!

[Christian Merten]

Took me some time, but your suggestion worked:

import Mathlib

open TensorProduct

variable (R S M N : Type*) [CommRing R] [CommRing S] [Algebra R S]
  [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]

noncomputable def baseChangeCancel : N ⊗[R] M ≃ₗ[S] N ⊗[S] (S ⊗[R] M) := by
  letI g : (N ⊗[S] S) ⊗[R] M ≃ₗ[S] N ⊗[R] M :=
    AlgebraTensorModule.congr (TensorProduct.rid S N) (LinearEquiv.neg R)
  exact g.symm ≪≫ₗ (AlgebraTensorModule.assoc R S S N S M)

[Christian Merten]

Unfortunately in the doc string of docs#TensorProduct.AlgebraTensorModule.assoc some variable names were mixed up, I fixed it in #10051.