## Stream: general

### Topic: Diamond golf

#### Eric Wieser (Dec 18 2020 at 18:09):

Can anyone suggest a shorter proof for this lemma (to qualify you have to be using mathlib@775edc615ecec631d65b6180dbcc7bc26c3abc26 or newer):

import linear_algebra.tensor_product

theorem smul_tmul'_int {R : Type*} {M : Type*} {N : Type*}
[comm_semiring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]
(r : ℤ) (m : M) (n : N) :
r • (m ⊗ₜ n : M ⊗[R] N) = (r • m) ⊗ₜ n :=
begin
simp only [←gsmul_eq_smul],
induction r,
{ simp only [gsmul_of_nat, ←nat.smul_def],
convert smul_tmul' _ _ _,
rw this,
refl,
repeat {apply_instance }, },
{ simp only [gsmul_neg_succ_of_nat, ←nat.smul_def, neg_tmul, tmul_neg],
rw neg_inj,
convert smul_tmul' _ _ _,
rw this,
refl,
repeat {apply_instance }, }
end


#### Kevin Buzzard (Dec 18 2020 at 18:27):

\$ git checkout 775edc615ecec631d65b6180dbcc7bc26c3abc26
fatal: reference is not a tree: 775edc615ecec631d65b6180dbcc7bc26c3abc26


and on master I get an unexpected token at M ⊗[R] N in the statement.

#### Eric Wieser (Dec 18 2020 at 18:28):

https://github.com/leanprover-community/mathlib/commit/775edc615ecec631d65b6180dbcc7bc26c3abc26

#### Eric Wieser (Dec 18 2020 at 18:29):

Added the missing open_locale

#### Eric Wieser (Dec 18 2020 at 18:34):

The proof for that lemma was easier before that commit, but on the other hand the proof for nat was harder.

#### Kevin Buzzard (Dec 18 2020 at 18:36):

aah, I was a few hours out of date :-)

#### Kevin Buzzard (Dec 18 2020 at 18:40):

Still doesn't compile for me.

#### Eric Wieser (Dec 18 2020 at 18:40):

open tensor_product?

#### Eric Wieser (Dec 18 2020 at 18:42):

I wonder if either there's a clever simp lemma that could be made to solve this type of thing, or whether it would need to be a tactic.

#### Adam Topaz (Dec 18 2020 at 18:45):

why doesn't docs#tensor_product.smul_tmul and docs#tensor_product.tmul_smul take care of this?

#### Eric Wieser (Dec 18 2020 at 18:49):

Because there is no Z-module instance for comm_semiring R provided in that file

Oh I see.

#### Kevin Buzzard (Dec 18 2020 at 18:49):

theorem smul_tmul'_int {R : Type*} {M : Type*} {N : Type*}
[comm_semiring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]
(r : ℤ) (m : M) (n : N) :
r • (m ⊗ₜ n : M ⊗[R] N) = (r • m) ⊗ₜ n :=
begin
apply int.induction_on r,
{ simp },
{ intros i hi,
{ intros i hi,
end


#### Eric Wieser (Dec 18 2020 at 18:49):

Adam, in master there is now an instance for comm_ring R though, and those lemmas do work

#### Adam Topaz (Dec 18 2020 at 18:52):

Do we have the construction which "ringifies" a semiring?

Is there one?

#### Adam Topaz (Dec 18 2020 at 18:52):

You might get the trivial ring but it still works.

#### Adam Topaz (Dec 18 2020 at 18:53):

E.g. the ringification of $\mathbb{N}$ is $\mathbb{Z}$.

#### Eric Wieser (Dec 18 2020 at 18:54):

Oh right, I thought you mean a mechanism to create a ring structure on N, not a new type that has the structure

#### Adam Topaz (Dec 18 2020 at 18:55):

My point is the an additive commutative group which is a semimodule over a semiring turns out to be a module over the ringification

#### Eric Wieser (Dec 18 2020 at 18:55):

Yeah, I see that now

#### Adam Topaz (Dec 18 2020 at 18:56):

So if we had this construction and some simp lemma that takes tmul over the semiring to tmul over the ringification, then those two lemmas would prove your result immediately

#### Eric Wieser (Dec 18 2020 at 18:56):

my original plan was to create a new tensor_product.smul_compatible type-class, and add is_scalar_tower.to_smul_compatible and int.smul_compatible so that the smul_tmul' lemma automatically works for int in this case

#### Eric Wieser (Dec 18 2020 at 18:57):

But maybe there's a better generalization of is_scalar_tower to make this case work

#### Adam Topaz (Dec 18 2020 at 18:57):

Kevin's proof is very special for $\mathbb{Z}$, it seems.

Right

#### Eric Wieser (Dec 18 2020 at 18:58):

Hence my plan to create a typeclass to hook the proof into

#### Eric Wieser (Dec 18 2020 at 18:58):

Which means that the user doesn't have to care that the proof is special, they just apply the smul_tmul lemma and it works

#### Kevin Buzzard (Dec 18 2020 at 18:59):

import linear_algebra.tensor_product

open_locale tensor_product

open tensor_product

variables {R : Type*} {M : Type*} {N : Type*}
[comm_semiring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]

lemma sub_tmul (m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = m₁ ⊗ₜ n - m₂ ⊗ₜ[R] n :=

theorem smul_tmul'_int (r : ℤ) (m : M) (n : N) :
r • (m ⊗ₜ n : M ⊗[R] N) = (r • m) ⊗ₜ n :=
begin
apply int.induction_on r,
{ simp },
{ intros i hi,
{ intros i hi,
simp [sub_smul, hi, sub_tmul] },
end


#### Kevin Buzzard (Dec 18 2020 at 18:59):

sub_tmul is missing for some reason.

#### Eric Wieser (Dec 18 2020 at 19:01):

I suspect a lot of sub lemmas were missing because we could get away with definitional equality to add before

#### Eric Wieser (Dec 18 2020 at 19:16):

My lean is stuck on orange bars again, but I think sub_tmul golfs to

lemma sub_tmul (m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = m₁ ⊗ₜ n - m₂ ⊗ₜ[R] n :=
((mk R M N).flip _).map_sub _ _


#### Eric Wieser (Dec 18 2020 at 19:35):

Thanks Kevin, I've added the missing sub lemmas in #5428

#### Eric Wieser (Dec 18 2020 at 21:10):

Eric Wieser said:

my original plan was to create a new tensor_product.smul_compatible type-class, and add is_scalar_tower.to_smul_compatible and int.smul_compatible so that the smul_tmul' lemma automatically works for int in this case

And #5430 contains a sketch of this idea, although I wonder if it makes sense to try to generalize it to also solve:

-- with a suitable typeclass, this could be solved with apply map_smul
lemma map_smul_int (l : M →ₗ[R] N) (z : ℤ) (m : M) : l (z • m) = z • l m :=
begin
induction z using int.induction_on with r ih r ih,
simp,
simpa [sub_smul] using ih,
end


#### Eric Wieser (Dec 23 2020 at 13:13):

I've updated #5430 to make the above provable with linear_map.map_smul_of_tower, would appreciate if someone could take a look

#### Eric Wieser (Dec 28 2020 at 14:12):

I also found that I could make a lot of diamond pain go away by making the is_scalar_tower \N instances not depend on a specific instance of has_scalar: #5509

Last updated: Aug 03 2023 at 10:10 UTC