Diamond golf

Stream: general

[Eric Wieser]

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]

$ 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]

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

[Eric Wieser]

Added the missing open_locale

[Eric Wieser]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Still doesn't compile for me.

[Eric Wieser]

open tensor_product?

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Adam Topaz]

Oh I see.

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Eric Wieser]

Is there one?

[Adam Topaz]

Sure, formally add all negations

[Adam Topaz]

You might get the trivial ring but it still works.

[Adam Topaz]

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

[Eric Wieser]

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]

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]

Yeah, I see that now

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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

[Eric Wieser]

Right

[Eric Wieser]

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

[Eric Wieser]

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]

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]

sub_tmul is missing for some reason.

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

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