A iso to B as S-mods => iso as R-mods?

Stream: Is there code for X?

[Kevin Buzzard]

I find this part of the library so confusing. Do we have this?

import Mathlib

example (R S A B) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup A] [AddCommGroup B]
  [Module R A] [Module S A] [IsScalarTower R S A]
  [Module R B] [Module S B] [IsScalarTower R S B]
  (e : A ≃ₗ[S] B) : A ≃ₗ[R] B := sorry

background: I am trying to write down a 3-line proof and it's taken me over an hour and I still haven't managed to write down the first line. I've tried exact?, I've tried loogling for Algebra ?R ?S, LinearEquiv ?S ?A ?B, LinearEquiv ?R ?A ?B, I've tried guessing the name, I've given up and I'm asking here.

What I'm actually trying to write down is the following isomorphism. All rings are commutative. Let $B$ and $K$ be $A$-algebras and let $L$ be a $K$-algebra isomorphic to $K\otimes_AB$. Then for $V$ a $K$-module I claim that $K\otimes_AV$ is isomorphic to $L\otimes_BV$ as $K$-module, with the isomorphism being $K\otimes_AV\cong K\otimes_A(B\otimes_BV)\cong (K\otimes_AB)\otimes_BV \cong L\otimes_BV.$ Even stating the result is a chore.

import Mathlib

open scoped TensorProduct

variable (A B K L V : Type*)
  [CommRing A] [CommRing B] [Algebra A B]
  [CommRing K] [Algebra A K]
  [CommRing L] [Algebra K L] [Algebra B L]
  [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
  [SMulCommClass B K L] -- you have to get this right to
  -- make the example even typecheck; SMulCommClass K B L doesn't work
  [AddCommGroup V] [Module A V] [Module B V] [IsScalarTower A B V]

example (e : K ⊗[A] B ≃ₗ[K] L) : K ⊗[A] V ≃ₗ[K] L ⊗[B] V :=
  sorry

My plan was first to write down the isomorphism $V\cong B\otimes_B V$ as $A$-modules but TensorProduct.lid B V is the isomorphism as B-modules and there's no TensorProduct.AlgebraTensorModule.lid, and I want the isomorphism as A-modules.

To compound my frustration what I actually want is an isomorphism V ⊗[A] K ≃ₗ[K] V ⊗[B] L but this doesn't even typecheck because we don't have the module structure coming from an action on the right term of the tensor product; I have made a scope containing lots of right algebra instances (the fear is ambiguity for the $A$-module action on $A\otimes A$ but this never happens in my situation) but I'm now wondering whether I need to make another scope making lots of right module instances).

[Eric Wieser]

e.restrictScalars R

[Kevin Buzzard]

Thanks. I just don't seem to be able to learn all of these names.

[Eric Wieser]

It's unfortunate that exact? is no use here

[Kevin Buzzard]

exact? has found the next one (iso V=W -> iso K tensor V = K tensor W, apparently it's LinearEquiv.lTensor.

[Kevin Buzzard]

aargh my proof doesn't work in Lean

[Eric Wieser]

Wrong side of the tensor product?

[Kevin Buzzard]

$(K\otimes_AB)\otimes_BV$ doesn't typecheck because $K\otimes_AB$ is not a $B$-module in Lean :-/

[Eric Wieser]

Write it the other way around :)

[Eric Wieser]

It's an intermediate step so you should be ok

[Eric Wieser]

I'm struggling to write the first equality of your proof, because the iso isn't linear over a big enough ring

[Eric Wieser]

Ah,

example (e : K ⊗[A] B ≃ₗ[K] L) : K ⊗[A] V ≃ₗ[K] L ⊗[B] V :=
  have : B ⊗[B] V ≃ₗ[A] V := (TensorProduct.lid B V).restrictScalars _
  have p1 := TensorProduct.AlgebraTensorModule.congr (.refl K K) this.symm
  p1 ≪≫ₗ _

[Andrew Yang]

Do you not need e to also be B linear?

[Kevin Buzzard]

Probably -- it is B-linear in the application

[Kevin Buzzard]

In the application A and B are number fields, and K and L are their adele rings. I don't even know how to say "e is B-linear" though because the LHS isn't a B-module.

[Andrew Yang]

In particular you need them to be iso as $B$-modules for $(K\otimes_AB)\otimes_BV \cong L\otimes_BV$ to go through.

[Andrew Yang]

I am guessing you use [Algebra.IsPushout A K B L] instead.

[Eric Wieser]

Is this a place where directly constructing the map with lift is easier than trying to find a composition?

[Andrew Yang]

Here's one attempt which does not directly fill the sorry above

example (e : B ⊗[A] K ≃ₗ[B] L) : K ⊗[A] V ≃ₗ[A] L ⊗[B] V :=
  TensorProduct.comm _ _ _ ≪≫ₗ ((TensorProduct.AlgebraTensorModule.cancelBaseChange A B B V K).symm.trans
    (TensorProduct.AlgebraTensorModule.congr (.refl _ _) e) ≪≫ₗ TensorProduct.comm _ _ _).restrictScalars A

[Eric Wieser]

(#25379 fixes the lousy "R → S ↓ ↓ R' → S'" docstring for docs#Algebra.IsPushout)

[Kevin Buzzard]

Oh I like that docstring! I was thinking of making A → B ↓ ↓ K → L be notation for the commutative square!

[Kevin Buzzard]

It should expand to [Algebra A B] [Algebra A K] [Algebra K L] [Algebra B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]

[Kevin Buzzard]

I had initially assumed that the author of the docstring was using A → B ↓ ↓ K → L as cool "you can clearly guess what this means" notation for the commutative square, I was surprised when one day I looked in the source code and realised what was actually going on.

[Kevin Buzzard]

Andrew Yang said:

example (e : B ⊗[A] K ≃ₗ[B] L) : K ⊗[A] V ≃ₗ[A] L ⊗[B] V :=
  TensorProduct.comm _ _ _ ≪≫ₗ ((TensorProduct.AlgebraTensorModule.cancelBaseChange A B B V K).symm.trans
    (TensorProduct.AlgebraTensorModule.congr (.refl _ _) e) ≪≫ₗ TensorProduct.comm _ _ _).restrictScalars A

I see -- so this is yet another trick: use TensorProduct.AlgebraTensorModule.cancelBaseChange. This restriction in mathlib of "everything must act on the left" is very frustrating because it is completely unnatural from the point of view of mathematics.

[Eric Wieser]

Maybe there should be a scope you open which just draws all the tensor product symbols backwards

[Eric Wieser]

docs#TensorProduct.AlgebraTensorModule.cancelBaseChange is implemented with the pieces we were reaching for, it's not an "I give up, use lift" situation at least.

[Kevin Buzzard]

But that doesn't solve the problem because I don't really want to be jumping through hoops and applying TensorProduct.comm (twice!) just to make Lean happy, I want to be able to write down the proofs which I'd write down on paper.

[Kevin Buzzard]

How easy is it to prove that Andrew's map sends k tensor v to k tensor v? Actually probably this isn't even true! The e in the theorem should just be the statement that the canonical map (coming from all the algebra and scalar tower instances) is an isomorphism, not a random isomorphism

[Eric Wieser]

Easy:

import Mathlib

open scoped TensorProduct

variable (A B K L V : Type*)
  [CommRing A] [CommRing B] [Algebra A B]
  [CommRing K] [Algebra A K]
  [CommRing L] [Algebra K L] [Algebra B L]
  [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
  [SMulCommClass B K L] -- you have to get this right to
  -- make the example even typecheck; SMulCommClass K B L doesn't work
  [AddCommGroup V] [Module A V] [Module B V] [IsScalarTower A B V]


noncomputable def foo (e : B ⊗[A] K ≃ₗ[B] L) : K ⊗[A] V ≃ₗ[A] L ⊗[B] V :=
  TensorProduct.comm _ _ _ ≪≫ₗ ((TensorProduct.AlgebraTensorModule.cancelBaseChange A B B V K).symm.trans
    (TensorProduct.AlgebraTensorModule.congr (.refl _ _) e) ≪≫ₗ TensorProduct.comm _ _ _).restrictScalars A

theorem foo_tmul (e : B ⊗[A] K ≃ₗ[B] L) (k : K) (v : V) :
    foo A B K L V e (k ⊗ₜ v) = (e (1 ⊗ₜ k)) ⊗ₜ v :=
  rfl

[Eric Wieser]

I am very glad I refactored tensor products to make this type of thing rfl

[Eric Wieser]

(the trick was to make docs#FreeAddMonoid override List.sum to make [x].sum = x rfl, rather than [x].sum = x + 0)

[Andrew Yang]

By the way SMulCommClass B K L is true by default. It is docs#SMulCommClass.of_commMonoid which you can open as a local instance (it cannot be global because of performance reasons)

[Kevin Buzzard]

So it's not true by default :-) (I had to add it in my example to make something typecheck but in the application this is clearly how I should be justifying it)