Zulip Chat Archive

Stream: Is there code for X?

Topic: smul of tmul by ℕ and ℤ


view this post on Zulip 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],
    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

view this post on Zulip Eric Wieser (Dec 11 2020 at 09:45):

Ah, solved!

view this post on Zulip Eric Wieser (Dec 11 2020 at 10:13):

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

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Dec 18 2020 at 12:24):

Kicked on the queue

view this post on Zulip 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