Tensor products

Stream: Is there code for X?

[Antoine Chambert-Loir]

I am struggling to define the following obvious map: S ⊗[R] T →ₐ[R] S ⊗[A] T, where A R S T are commutative rings, S T are R-algebras and Ris an A-algebra.
In the last line of the definition of hr below, Lean can't find the instance I just gave it one line above.

import ring_theory.tensor_product

open_locale tensor_product

variables (A : Type*) [comm_ring A] (R  : Type*)
  [comm_ring R] [algebra A R]
  (S T : Type*) [comm_ring S] [comm_ring T]
  [algebra A S] [algebra R S] [is_scalar_tower A R S]
  [algebra A T] [algebra R T] [is_scalar_tower A R T]

def hl : S →ₐ[R] S ⊗[A] T :=
begin
exact is_scalar_tower.to_alg_hom R S (S ⊗ T),
end

def hr : T →ₐ[R] S ⊗[A] T :=
begin
haveI: algebra T (S ⊗[A] T),
exact algebra.tensor_product.right_algebra,
haveI : is_scalar_tower R T (S ⊗ T),
exact algebra.tensor_product.right_is_scalar_tower,
exact is_scalar_tower.to_alg_hom R T (S ⊗ T),
end

def foo : S ⊗[R] T →ₐ[R] S ⊗[A] T :=
algebra.tensor_product.product_map (hl A R S T) (hr A R S T)
``

[Kevin Buzzard]

...
exact algebra.tensor_product.right_is_scalar_tower,
apply is_scalar_tower.to_alg_hom R T (S ⊗ T),
apply_instance,
convert _inst_12,
-- 34 goals, most of which are `S ⊗ T = S ⊗ T`
end

[Kevin Buzzard]

Oh! The goal state doesn't display it but it's actually S ⊗[R] T = S ⊗[A] T

[Kevin Buzzard]

Change your haveI to haveI : is_scalar_tower R T (S ⊗[A] T), and it works
`

[Eric Wieser]

Doesn't S ⊗[R] T →ₐ[R] S ⊗[A] T exist as something like docs#algebra.tensor_product.map?

[Eric Wieser]

Oh nevermind, I misread that completely

[Kevin Buzzard]

Yeah there should be a map, I think probably the issue is that the goal state isn't saying what we're tensoring over so it can be confusing.

[Kevin Buzzard]

Aah, also haveI: algebra T (S ⊗[A] T), should be letI because it's data. This can lead to very confusing errors :-)

[Antoine Chambert-Loir]

Kevin Buzzard said:

Yeah there should be a map, I think probably the issue is that the goal state isn't saying what we're tensoring over so it can be confusing.

Exactly, the output of Lean takes out all mentions of the rings over which scalar products happen…

[Eric Wieser]

I'm pretty sure this is new behavior introduced by the hole! syntax in notations; I don't remember this happening pre-port

[Eric Wieser]

local notation  M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N

makes the mwe readable again

[Antoine Chambert-Loir]

Thanks for the better notation.
On the other hand, my MWE shouldn't have been expected to work since the map I tried to define went in the bad direction…

[Antoine Chambert-Loir]

import ring_theory.tensor_product


open_locale tensor_product
local notation  M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N

variables (A : Type*) [comm_ring A] (R  : Type*)
  [comm_ring R] [algebra A R]
  (S T : Type*) [comm_ring S] [comm_ring T]
  [algebra A S] [algebra R S] [is_scalar_tower A R S]
  [algebra A T] [algebra R T] [is_scalar_tower A R T]


example : module A (S ⊗[R] T) := infer_instance -- exact tensor_product.left_module

example : module R (S ⊗[A] T) := infer_instance -- algebra.to_module

-- needs to be introduced
instance : algebra A (S ⊗[R] T) := ring_hom.to_algebra ((algebra_map S (S ⊗[R] T)).comp (algebra_map A S))

example (a : A) (s : S) (t : T) :  a • (s ⊗ₜ[R] t) = (a • s) ⊗ₜ[R] t := rfl

example (a : A) (s : S) (t : T) :  a • (s ⊗ₜ[R] t) = s ⊗ₜ[R] (a • t) := by simp only [tensor_product.tmul_smul]

example : is_scalar_tower A S (S ⊗[A] T) := infer_instance -- tensor_product.is_scalar_tower_left

example : is_scalar_tower A S (S ⊗[R] T) := infer_instance -- tensor_product.is_scalar_tower

example : is_scalar_tower A R (S ⊗[A] T) := infer_instance -- tensor_product.is_scalar_tower_left

example : is_scalar_tower A R (S ⊗[R] T) := infer_instance -- tensor_product.is_scalar_tower

example : (S ⊗[A] T) →ₐ[A] (S ⊗[R] T) :=
begin
  let hl : S →ₐ[A] (S ⊗[R] T) := { to_fun := algebra.tensor_product.include_left,
    map_one' := rfl,
    map_mul' := λ x y, by simp only [algebra.tensor_product.include_left_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
    map_zero' := by simp only [algebra.tensor_product.include_left_apply, tensor_product.zero_tmul],
    map_add' := λ x y, by simp only [algebra.tensor_product.include_left_apply, tensor_product.add_tmul],
    commutes' := λ a, rfl, },
    let hr : T →ₐ[A] (S ⊗[R] T) :=  {
to_fun := algebra.tensor_product.include_right,
map_one' := rfl,
map_mul' := λ x y, by simp only [algebra.tensor_product.include_right_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
map_zero' := by simp only [algebra.tensor_product.include_right_apply, tensor_product.tmul_zero],
map_add' := λ x y, by simp only [algebra.tensor_product.include_right_apply, tensor_product.tmul_add],
-- here, that does not work!
    commutes' := λ a, begin
    simp only [algebra.tensor_product.include_right_apply],
    simp only [algebra.algebra_map_eq_smul_one],
    simp only [tensor_product.tmul_smul],
    suffices : (1 ⊗ₜ[R] 1: S ⊗ T) = 1, rw ← this,
-- the two scalar multiplications look distinct…
    sorry,
    refl,
    end, },

end

[Anatole Dedecker]

I think your instance instance : algebra A (S ⊗[R] T) := ring_hom.to_algebra ((algebra_map S (S ⊗[R] T)).comp (algebra_map A S)) is nasty in some way, because if I remove it (and switch to non unital algebra morphism to work around it) then I have no problem constructing the map hr

[Anatole Dedecker]

Indeed if you replace it by instance : algebra A (S ⊗[R] T) := algebra.of_module sorry sorry (and hope really strong that the two sorries are true) then you can do

example : (S ⊗[A] T) →ₐ[A] (S ⊗[R] T) :=
begin
  let hl : S →ₐ[A] (S ⊗[R] T) :=
  { to_fun := algebra.tensor_product.include_left,
    map_one' := rfl,
    map_mul' := λ x y, by simp only [algebra.tensor_product.include_left_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
    map_zero' := by simp only [algebra.tensor_product.include_left_apply, tensor_product.zero_tmul],
    map_add' := λ x y, by simp only [algebra.tensor_product.include_left_apply, tensor_product.add_tmul],
    commutes' := λ a,
    begin
      simp only [algebra.tensor_product.include_left_apply],
      simp only [algebra.algebra_map_eq_smul_one],
      simp only [← tensor_product.smul_tmul'],
      refl,
    end, },
  let hr : T →ₐ[A] (S ⊗[R] T) :=
  { to_fun := algebra.tensor_product.include_right,
    map_one' := rfl,
    map_mul' := λ x y, by simp only [algebra.tensor_product.include_right_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
    map_zero' := by simp only [algebra.tensor_product.include_right_apply, tensor_product.tmul_zero],
    map_add' := λ x y, by simp only [algebra.tensor_product.include_right_apply, tensor_product.tmul_add],
    commutes' := λ a,
    begin
      simp only [algebra.tensor_product.include_right_apply],
      simp only [algebra.algebra_map_eq_smul_one],
      simp only [tensor_product.tmul_smul],
      refl
    end, },
  sorry
end

[Kevin Buzzard]

At the sorry, the goal is ⊢ a • 1 ⊗ₜ[R] 1 = a • 1 ⊗ₜ[R] 1 and if you try congr this reduces the goal to tensor_product.left_has_smul = smul_zero_class.to_has_smul. You can now do ext a st if you want to see the calculation which needs to be done (it looks like ⊢ a • st = a • st so of course here there must be some diamond).

If you now set pp.all on, you can look and see what instances are showing up in both sides of the equality and in particular in the inputs to the two has_smul.smul functions. The right hand side seems to use a lot more of the instances than the left hand side.

[Eric Wieser]

ring_hom.to_algebra is pretty much always nasty

[Eric Wieser]

Use it in a proof if you have to, but don't use it to construct canonical instances

[Anatole Dedecker]

I may have written absolutely stupid things since I'm half-sleeping, but here is a working version:

import ring_theory.tensor_product

open_locale tensor_product
local notation  M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N

variables (A : Type*) [comm_ring A] (R  : Type*)
  [comm_ring R] [algebra A R]
  (S T : Type*) [comm_ring S] [comm_ring T]
  [algebra A S] [algebra R S] [is_scalar_tower A R S]
  [algebra A T] [algebra R T] [is_scalar_tower A R T]

/-
  S   T
   \ /
    R
    |
    A
-/

instance foo : algebra A (S ⊗[R] T) := algebra.of_module'
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [algebra.tensor_product.one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [mul_add, h₁, h₂]))
  -- Copy pasting worked ?!?!?!?!?
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [algebra.tensor_product.one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [add_mul, h₁, h₂]))

example : (S ⊗[A] T) →ₐ[A] (S ⊗[R] T) :=
begin
  let hl : S →ₐ[A] (S ⊗[R] T) :=
  { to_fun := algebra.tensor_product.include_left,
    map_one' := rfl,
    map_mul' := λ x y, by simp only [algebra.tensor_product.include_left_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
    map_zero' := by simp only [algebra.tensor_product.include_left_apply, tensor_product.zero_tmul],
    map_add' := λ x y, by simp only [algebra.tensor_product.include_left_apply, tensor_product.add_tmul],
    commutes' := λ a,
    begin
      simp only [algebra.tensor_product.include_left_apply],
      simp only [algebra.algebra_map_eq_smul_one],
      simp only [← tensor_product.smul_tmul'],
      refl,
    end, },
  let hr : T →ₐ[A] (S ⊗[R] T) :=
  { to_fun := algebra.tensor_product.include_right,
    map_one' := rfl,
    map_mul' := λ x y, by simp only [algebra.tensor_product.include_right_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
    map_zero' := by simp only [algebra.tensor_product.include_right_apply, tensor_product.tmul_zero],
    map_add' := λ x y, by simp only [algebra.tensor_product.include_right_apply, tensor_product.tmul_add],
    commutes' := λ a,
    begin
      simp only [algebra.tensor_product.include_right_apply],
      simp only [algebra.algebra_map_eq_smul_one],
      simp only [tensor_product.tmul_smul],
      refl
    end },
  -- THIS IS VERY UGLY. If we add `foo` to mathlib, we need to remove
  -- `algebra.tensor_product.tensor_product.algebra` and use `foo A A S T` instead,
  -- so that we don't have these problems.
  convert algebra.tensor_product.product_map hl hr,
  ext,
  refl
end

[Kevin Buzzard]

Here's the diamond:

-- needs to be introduced
instance : algebra A (S ⊗[R] T) := ring_hom.to_algebra ((algebra_map S (S ⊗[R] T)).comp (algebra_map A S))

def foo : module A (S ⊗[R] T) := tensor_product.left_module -- found with `apply_instance`
def bar : module A (S ⊗[R] T) := algebra.to_module -- uses the instance introduced.

-- example : foo = bar := rfl -- fails

[Eric Wieser]

@Anatole Dedecker, your two copied proofs should probably be is_scalar_tower/smul_comm_class instances

[Anatole Dedecker]

Yes I know, I just wanted to get it done :sweat_smile:

[Antoine Chambert-Loir]

It seems there should be something for algebras in the same spirit as what is done with docs#tensor_product.left_module and docs#tensor_product.module.

Here is an attempt, borrowing from @Anatole Dedecker 's answer.

import ring_theory.tensor_product


open_locale tensor_product
local notation  M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N

variables (R : Type*) [comm_semiring R] (R' : Type*) [comm_semiring R'] [algebra R R']
(M : Type*) [semiring M] [algebra R M] [algebra R' M]
   [smul_comm_class R' R M]
(N : Type*) [semiring N] [algebra R N] [algebra R' N]

example : module R (M ⊗[R'] N) := infer_instance
-- tensor_product.left_module

instance tensor_product.left_algebra : algebra R (M ⊗[R'] N) := algebra.of_module'
 (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [algebra.tensor_product.one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [mul_add, h₁, h₂]))
  -- Copy pasting worked ?!?!?!?!?
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [algebra.tensor_product.one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [add_mul, h₁, h₂]))

def tensor_product.algebra' : algebra R (M ⊗[R] N) :=
tensor_product.left_algebra R R M N

[Eric Wieser]

I'm somewhat surprised this doesn't already exist

[Eric Wieser]

docs#algebra.tensor_product.left_algebra?

[Anatole Dedecker]

Oh this is really interesting: we can replace [algebra R S] [is_scalar_tower R S A] by [algebra S R] [is_scalar_tower S R A] in docs#algebra.tensor_product.left_algebra and it still works!

[Anatole Dedecker]

And this backwards version is what Antoine wants IIUC

[Antoine Chambert-Loir]

I'm completely confused…

[Antoine Chambert-Loir]

Probably, this means that the is_scalar_tower instance should just be replaced by some smul_comm_class as I suggested.

[Kevin Buzzard]

This is not a propositional diamond, right? The issue is simply that the proof that the two actions coincide is not rfl.

[Kevin Buzzard]

My understanding is that one of the actions of A on S tensor T is "map A to S tensor T through S and use *" and the other one is "A acts on S so we can define an action of A on things of the form s tensor t by sending them to (a bub s) tensor t and now by some inductive principle we have an action on the full tensor product"

[Anatole Dedecker]

Let me give a more concrete example with $\mathbb{R}$ and $\mathbb{C}$.
What Antoine wants is:

If $A, B$ are two $\mathbb{C}$-algebras (and also $\mathbb{R}$-algebras, with the assumptions that these two structures are compatible), then $A \otimes_\mathbb{C} B$ is also an $\R$-algebra (and presumably everything is still compatible in the right way)

What docs#algebra.tensor_product.left_algebra says is:

If $A, B$ are two $\mathbb{R}$-algebras, and $A$ is also a $\mathbb{C}$-algebra in a compatible way, then $A \otimes_\mathbb{R} B$ is a $\mathbb{C}$-algebra

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

Eric Wieser said:

docs#algebra.tensor_product.left_algebra?

To be clear I am answering this.

[Anatole Dedecker]

Kevin Buzzard said:

This is not a propositional diamond, right? The issue is simply that the proof that the two actions coincide is not rfl.

That was the problem indeed, but I think Antoine's last code snippet avoids it (by using the existing smul and proving it still works)

[Eric Wieser]

This does make it sound like something is assuming a tower when it actually only needs commutativity

[Antoine Chambert-Loir]

This is something like that.
In the following file (not “minimal” in any sense), I tried to isolate the cases where smul_comm_class or tensor_product_compatible should be the instances to add. At the end, its a is_scalar_tower, though.

I tried to make it cleaner, introducing many intermediate functions. Nevertheless, the convert at the end of what @Anatole Dedecker wrote (and exact does not work) seems to prevent Lean to unfold the definition. (I get a cast _ which I can't simp.)

import ring_theory.tensor_product
import ring_theory.ideal.quotient_operations
import algebra.algebra.subalgebra.basic

open_locale tensor_product
local notation  M ` ⊗[`:100 R `] `:0 N:100 := tensor_product R M N

/- The goal is to prove lemma 9 in Roby (1965) -/

lemma ring_hom.ker_eq_ideal_iff  {A B : Type*} [comm_ring A] [comm_ring B] (f : A →+* B) (I : ideal A) :
  f.ker = I ↔ ∃ (h : I ≤ f.ker), function.injective (ideal.quotient.lift I f h) :=
begin
  split,
  { intro hI, use le_of_eq hI.symm,
    apply ring_hom.lift_injective_of_ker_le_ideal,
    simp only [hI, le_refl], },
  { rintro ⟨hI, h⟩,
    simp only [ring_hom.injective_iff_ker_eq_bot,
    ideal.ker_quotient_lift f hI,
    ideal.map_eq_bot_iff_le_ker,
    ideal.mk_ker] at h,
    exact le_antisymm h hI, },
end

variables (R : Type*) [comm_ring R]
 (R' : Type*) [comm_ring R']
 (M : Type*) [comm_ring M] [algebra R M] [algebra R' M]
 (N : Type*) [comm_ring N] [algebra R N] [algebra R' N]

section smul_comm

variable [smul_comm_class R' R M]
-- variables [algebra R R'] [is_scalar_tower R R' M] [is_scalar_tower R R' N]

example : module R (M ⊗[R'] N) := infer_instance
-- tensor_product.left_module

instance algebra.tensor_product.left_algebra' : algebra R (M ⊗[R'] N) :=
  algebra.of_module'
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [algebra.tensor_product.one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [mul_add, h₁, h₂]))
  -- Copy pasting worked ?!?!?!?!?
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [algebra.tensor_product.one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [add_mul, h₁, h₂]))

-- def algebra.tensor_product.algebra' : algebra R (M ⊗[R] N) := algebra.tensor_product.left_algebra R R M N

lemma algebra.tensor_product.algebra'_eq_algebra :
algebra.tensor_product.left_algebra' R R M N
  = algebra.tensor_product.tensor_product.algebra :=
by { ext, exact rfl,}

example : comm_ring (M ⊗[R'] M) :=  infer_instance

-- instance : algebra R (M ⊗[R] N) := tensor_product.algebra' R R' M N

def tensor_product.include_left' : M →ₐ[R] (M ⊗[R'] N) := {
  to_fun := algebra.tensor_product.include_left,
  map_one' := ring_hom.map_one _, -- rfl,
  map_mul' := ring_hom.map_mul _, --  λ x y, by simp only [algebra.tensor_product.include_left_apply, algebra.tensor_product.tmul_mul_tmul, mul_one],
  map_zero' := ring_hom.map_zero _, -- by simp only [algebra.tensor_product.include_left_apply, tensor_product.zero_tmul],
  map_add' := ring_hom.map_add _, -- λ x y, by simp only [algebra.tensor_product.include_left_apply, tensor_product.add_tmul],
  commutes' := λ a,
  begin
    simp only [algebra.tensor_product.include_left_apply],
    simp only [algebra.algebra_map_eq_smul_one],
    simp only [← tensor_product.smul_tmul'],
    refl,
  end }

end smul_comm

section tensor_product_compatible

variables [smul_comm_class R' R M] [tensor_product.compatible_smul R' R M N]
-- variables [algebra R R'] [is_scalar_tower R R' M] [is_scalar_tower R R' N]

def tensor_product.include_right' : N →ₐ[R] (M ⊗[R'] N) := {
to_fun := algebra.tensor_product.include_right,
map_one' := rfl,
map_mul' := by convert algebra.tensor_product.include_right.map_mul,
map_zero' := by convert algebra.tensor_product.include_right.map_zero,
map_add' := by convert algebra.tensor_product.include_right.map_add,
commutes' := λ a, by {
  simp only [algebra.tensor_product.include_right_apply,
    algebra.algebra_map_eq_smul_one, tensor_product.tmul_smul],
  refl,} }


def tensor_product.can  : (M ⊗[R] N) →ₐ[R] (M ⊗[R'] N) :=
begin
  convert algebra.tensor_product.product_map (tensor_product.include_left' R R' M N) (tensor_product.include_right' R R' M N),
  apply algebra.tensor_product.algebra'_eq_algebra,
end

/- The following lemma should be straightforward,
but the `convert` in the definition of `tensor_product.can`
leads to a `cast _` which I can't unfold.   -/
lemma tensor_product.can_apply (m : M) (n: N) :
  tensor_product.can R R' M N (m ⊗ₜ[R] n) = m ⊗ₜ[R'] n :=
begin
  simp only [tensor_product.can],
  simp,
  simp_rw [tensor_product.include_left', tensor_product.include_right', algebra.tensor_product.include_left, algebra.tensor_product.include_right],
  simp only [ring_hom.to_fun_eq_coe, alg_hom.coe_mk],
  simp only [algebra.tensor_product.product_map],
sorry,
end


def tensor_product.can_ker : ideal (M ⊗[R] N) :=
  ideal.span ((λ (r : R'), ((r • (1 : M)) ⊗ₜ[R] (1 : N)) - ((1 : M) ⊗ₜ[R] (r • (1 : N)))) '' ⊤)


example : N →ₐ[R] M ⊗[R] N :=
begin
  convert @algebra.tensor_product.include_right R _ M _ _ N _ _,
  apply algebra.tensor_product.algebra'_eq_algebra,
end

example : N →ₐ[R] M ⊗[R] N :=tensor_product.include_right' R R M N

example : N →ₐ[R'] M ⊗[R'] N :=tensor_product.include_right' R' R' M N

end tensor_product_compatible

section is_scalar_tower

variables [algebra R R'] [is_scalar_tower R R' M] [is_scalar_tower R R' N]

def tensor_product.can'_left :
M →ₐ[R'] (M ⊗[R] N) ⧸ (tensor_product.can_ker R R' M N) :=
  (ideal.quotient.mkₐ R' (tensor_product.can_ker R R' M N)).comp
    (tensor_product.include_left' R' R M N)

def tensor_product.can'_right :
N →ₐ[R] (M ⊗[R] N) ⧸ (tensor_product.can_ker R R' M N) :=
  (ideal.quotient.mkₐ R (tensor_product.can_ker R R' M N)).comp
    (tensor_product.include_right' R R M N)

lemma is_R'_linear : is_linear_map R' (tensor_product.can'_right R R' M N) :=
begin
  apply is_linear_map.mk,
  { exact alg_hom.map_add _, },
  intros r n,
  simp [tensor_product.can'_right, tensor_product.include_right'],
  rw ← ideal.quotient.mkₐ_eq_mk R',
  rw ← alg_hom.map_smul,
  simp only [ideal.quotient.mkₐ_eq_mk],
  apply symm,
  rw ideal.quotient.eq ,
  simp only [tensor_product.can_ker],
  suffices : r • (1 : M) ⊗ₜ[R] n - (1 : M) ⊗ₜ[R] (r • n)
    = (r • (1 : M) ⊗ₜ[R] (1 : N) - (1 : M) ⊗ₜ[R] (r • (1 : N))) * ((1 : M) ⊗ₜ[R] n),
  rw this,
--   suffices : (r • (1 : M) ⊗ₜ[R] (1 : N) - (1 : M) ⊗ₜ[R] (r • (1 : N))) ∈ _,
  refine ideal.mul_mem_right ((1 : M) ⊗ₜ[R] n) _ _,
  apply ideal.subset_span,
  use ⟨r, set.mem_univ r, rfl⟩,
  simp only [sub_mul, algebra.smul_mul_assoc, algebra.tensor_product.tmul_mul_tmul, one_mul],
end

def tensor_product.can'_right' :
N →ₐ[R'] (M ⊗[R] N) ⧸ (tensor_product.can_ker R R' M N) := {
to_fun := tensor_product.can'_right R R' M N,
map_zero' := (is_R'_linear R R' M N).map_zero,
map_one' := rfl,
map_add' := (is_R'_linear R R' M N).map_add,
map_mul' := alg_hom.map_mul _,
commutes' := λ r, by simp only [algebra.algebra_map_eq_smul_one, (is_R'_linear R R' M N).map_smul, alg_hom.map_one] }

def tensor_product.can' :
(M ⊗[R'] N) →ₐ[R'] (M ⊗[R] N) ⧸ (tensor_product.can_ker R R' M N) :=
begin
  convert algebra.tensor_product.product_map
    (tensor_product.can'_left R R' M N) (tensor_product.can'_right' R R' M N),
  apply algebra.tensor_product.algebra'_eq_algebra,
end

lemma tensor_product.can'_apply (m : M) (n : N) :
  tensor_product.can' R R' M N (m ⊗ₜ[R'] n)
  = ideal.quotient.mk _ (m ⊗ₜ[R] n) :=
begin
  simp only [tensor_product.can'],
  simp,

sorry
end

example : (tensor_product.can R R' M N).to_ring_hom.ker = (tensor_product.can_ker R R' M N) :=
begin
  suffices h : tensor_product.can_ker R R' M N ≤ ring_hom.ker (tensor_product.can R R' M N).to_ring_hom,
  rw ring_hom.ker_eq_ideal_iff,
  use h,
  apply function.has_left_inverse.injective ,
--  apply function.bijective.injective,
--  rw function.bijective_iff_has_inverse,
  use tensor_product.can' R R' M N,
--   split,
  { -- left_inverse
    intro z,
    obtain ⟨y, rfl⟩ := ideal.quotient.mk_surjective z,
    simp only [alg_hom.to_ring_hom_eq_coe, ideal.quotient.lift_mk, alg_hom.coe_to_ring_hom],

    apply tensor_product.induction_on y,
    simp only [ring_hom.map_zero, alg_hom.map_zero],
    intros m n, simp only [tensor_product.can'_apply, tensor_product.can_apply],
    intros x y hx hy,
    simp only [ring_hom.map_add, alg_hom.map_add, ← ideal.quotient.mkₐ_eq_mk, hx, hy], },
  -- { -- right_inverse  sorry }

  -- h
  simp only [tensor_product.can_ker],
  rw ideal.span_le,
  intros z hz,
  simp only [set.top_eq_univ, set.image_univ, set.mem_range] at hz,
  obtain ⟨r, rfl⟩ := hz,
  simp only [set_like.mem_coe],
  simp only [ring_hom.sub_mem_ker_iff],
  simp only [alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom],
  simp only [tensor_product.can_apply],
  simp only [tensor_product.tmul_smul],
  refl,
end

end is_scalar_tower

[Eric Rodriguez]

@Alex J. Best's generalisation linter may be good here

[Antoine Chambert-Loir]

What do you mean?

[Antoine Chambert-Loir]

It seems that the problem comes from the instance I had to define: it creates a diamond.
I see no other solution than refactoring slightly docs#ring_theory.tensor_product to allow for an additional coefficient ring.
At the same time, one can relax many hypotheses everywhere…

[Eric Wieser]

What's the diamond?

[Antoine Chambert-Loir]

We need to have docs#algebra.tensor_product.left_algebra under less restrictive assumptions

variables (R : Type*) [comm_semiring R]  (R' : Type*) [comm_semiring R']
variables (M : Type*) [semiring M] [algebra R M] [algebra R' M]
variables (N : Type*) [semiring N] [algebra R N] [algebra R' N]

variables [smul_comm_class R' R M]
-- [smul_comm_class R' R N]
-- variables [algebra R R'] [is_scalar_tower R R' M] [is_scalar_tower R R' N]

example : module R (M ⊗[R'] N) := infer_instance
-- tensor_product.left_module

instance left_algebra' : algebra R (M ⊗[R'] N) :=
  algebra.of_module'
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [mul_add, h₁, h₂]))
  -- Copy pasting worked ?!?!?!?!?
  (λ a x, tensor_product.induction_on x
    rfl
    (λ s t, by simp [one_def, tensor_product.smul_tmul'])
    (λ x₁ x₂ h₁ h₂, by simp [add_mul, h₁, h₂]))

This means that one has two algebra structures on M ⊗[R] N when R = R', one given by docs#algebra.tensor_product.left_algebra (implicit parameters R, M and N) and the other given by algebra.tensor_product.left_algebra' R R M N. Thus we need to update the less general instance from mathlib
and set instance : algebra R (M ⊗[R] N) := left_algebra' R R M N .

Nevertheless, they coincide (not definitionally) :

lemma algebra'_eq_algebra :
tensor_product.left_algebra' R R M N  = tensor_product.algebra :=
  by { ext, exact rfl,}

[Antoine Chambert-Loir]

That's OK for me, but the commutativity assumptions in the very definition of the tensor product make me think that a lot of work has to be done sooner or later.

[Eric Wieser]

Those really ought to be definitional

[Anatole Dedecker]

Well I have good news. I finally decided to have a deep look at this and it turns out the solution is really simple. We can just replace https://github.com/leanprover-community/mathlib/blob/917c3c072e487b3cccdbfeff17e75b40e45f66cb/src/ring_theory/tensor_product.lean#L386 by variables {S : Type*} [comm_semiring S] [algebra S A] [smul_comm_class R S A] and the instance below still compiles, and now encompasses all of our use cases...

[Anatole Dedecker]

And I checked that it makes Antoine's original example as simple as:

example : (S ⊗[A] T) →ₐ[A] (S ⊗[R] T) :=
let hl : S →ₐ[A] (S ⊗[R] T) := algebra.tensor_product.include_left.restrict_scalars A in
let hr : T →ₐ[A] (S ⊗[R] T) := algebra.tensor_product.include_right.restrict_scalars A in
algebra.tensor_product.product_map hl hr

[Eric Wieser]

Antoine Chambert-Loir said:

That's OK for me, but the commutativity assumptions in the very definition of the tensor product make me think that a lot of work has to be done sooner or later.

I made a start on this quite some time ago, but the long tail of the work is lost to the porting effort.

[Eric Wieser]

The key missing piece was algbra.to_is_central_scalar, which right now we don't have the ability to state

[Antoine Chambert-Loir]

I understand and appreciate the effort. That's something boring enough to be handled one by a single person.

[Antoine Chambert-Loir]

@Anatole Dedecker , thanks for confirming that (I couldn't be sure because I don't dare changing the mathlib files), but after having looked into that one, I felt that there are several other instances that can be adjusted in a similar way.

[Anatole Dedecker]

#19118 (should be either easy to port or easy to do by hand in mathlib4)

[Anatole Dedecker]

Antoine Chambert-Loir said:

Anatole Dedecker , thanks for confirming that (I couldn't be sure because I don't dare changing the mathlib files), but after having looked into that one, I felt that there are several other instances that can be adjusted in a similar way.

On I hadn't read your last message carefully, indeed you already had the right generality.