smul of tmul by ℕ and ℤ

Stream: Is there code for X?

[Eric Wieser]

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],
    rw [add_tmul, tmul_add, r_ih], },
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

[Eric Wieser]

Ah, solved!

[Eric Wieser]

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

[Chris Hughes]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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]

Kicked on the queue

[Eric Wieser]

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