## Stream: Is there code for X?

### Topic: smul of tmul by ℕ and ℤ

#### Eric Wieser (Dec 11 2020 at 09:32):

These statements are true (modulo typos); are they in mathlib? Do they generalize to arbitrary semimodule structures over M and N? Perhaps with smul_comm_class or is_scalar_tower?

lemma smul_tmul_nat {R : Type*} {M : Type*} {N : Type*}
[comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N]
(r : ℕ) (m : M) (n : N) : ((r • m) ⊗ₜ[R] n) = m ⊗ₜ[R] r • n :=
begin
induction r,
{ simp, },
{ rw [nat.smul_def, nat.smul_def, succ_nsmul, succ_nsmul, ←nat.smul_def, ←nat.smul_def],
end

-- note: can be comm_semiring R after #5315
lemma smul_tmul_int {R : Type*} {M : Type*} {N : Type*}
[comm_ring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]
(r : ℤ) (m : M) (n : N) : ((r • m) ⊗ₜ[R] n) = m ⊗ₜ[R] r • n := sorry


Ah, solved!

#### Eric Wieser (Dec 11 2020 at 10:13):

#5317, although I'm worried these instance might be a bad idea.

#### Chris Hughes (Dec 11 2020 at 11:00):

I think there should be an easier proof using the lemma saying r • m = (r : R) • m, and tensor_product.smul_tmul.

#### Eric Wieser (Dec 11 2020 at 13:18):

Yeah, you're right, although I think the lemma you want is missing and I have to build it out of two others (←gsmul_eq_smul, module.gsmul_eq_smul_cast R):

lemma smul_tmul_int {R : Type*} {M : Type*} {N : Type*}
[comm_ring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]
(r : ℤ) (m : M) (n : N) : ((r • m) ⊗ₜ[R] n) = m ⊗ₜ[R] r • n :=
by rw [←gsmul_eq_smul, module.gsmul_eq_smul_cast R, ←gsmul_eq_smul, module.gsmul_eq_smul_cast R,
smul_tmul]

theorem smul_tmul'_int {R : Type*} {M : Type*} {N : Type*}
[comm_ring 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 :=
by rw [←gsmul_eq_smul, module.gsmul_eq_smul_cast R, ←gsmul_eq_smul, module.gsmul_eq_smul_cast R,
smul_tmul']

theorem tmul_smul_int {R : Type*} {M : Type*} {N : Type*}
[comm_ring R] [add_comm_group M] [add_comm_group N] [semimodule R M] [semimodule R N]
(r : ℤ) (m : M) (n : N) :
m ⊗ₜ (r • n) = r • (m ⊗ₜ n : M ⊗[R] N) :=
by rw [←gsmul_eq_smul, module.gsmul_eq_smul_cast R, ←gsmul_eq_smul, module.gsmul_eq_smul_cast R,
tmul_smul]


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

I'm getting some nasty timeouts in src#Module.monoidal_category.pentagon when applying docs#tensor_product.ext_fourfold with my changes in #5317... Any tips for helping the elaborator would be greatly appreciated!

#### Eric Wieser (Dec 15 2020 at 20:27):

I managed to get an 18x speedup on docs#category_theory.Module.monoidal_category.pentagon with #5383

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

I worked out a way to make #5317 happy without slowing down typeclass search everywhere a few days ago - would appreciate a review

#### Johan Commelin (Dec 18 2020 at 12:24):

Kicked on the queue

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

A follow-up to this thread; what I only have comm_semiring. Answer: diamonds!

Last updated: May 07 2021 at 22:14 UTC