# Zulip Chat Archive

## 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],
have := subsingleton.elim add_comm_monoid.nat_semimodule tensor_product.semimodule',
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,
have := subsingleton.elim add_comm_monoid.nat_semimodule tensor_product.semimodule',
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

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

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,
simp [add_smul, hi, add_tmul] },
{ intros i hi,
simp [add_smul, hi, neg_tmul, sub_eq_add_neg, add_tmul], }
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?

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

Is there one?

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

Sure, formally add all negations

#### 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.

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

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 :=
by simp [sub_eq_add_neg, add_tmul, neg_tmul]
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,
simp [add_smul, hi, add_tmul] },
{ 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 [add_smul] using ih,
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: Dec 20 2023 at 11:08 UTC