Zulip Chat Archive

Stream: Is there code for X?

Topic: finsupp gsmul_eq_smul


view this post on Zulip Kevin Buzzard (Aug 25 2020 at 13:57):

example (n : ) (α : Type) (x : α  ) : n  x = n  x :=
begin
  rw gsmul_eq_smul,
  -- ⊢ n • x = n • x
  congr',
  -- ⊢ finsupp.has_scalar = mul_action.to_has_scalar
  sorry
end

I'm stuck

view this post on Zulip Scott Morrison (Aug 25 2020 at 14:00):

does ext help?

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 14:07):

yes

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 14:07):

 module  (α  )

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 14:08):

example (n : ) (α : Type) (x : α  ) : n  x = n  x :=
begin
  rw module.gsmul_eq_smul_cast ,
  simp,
  apply_instance
end

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 14:09):

example (n : ) (α : Type) (x : α  ) : n  x = n  x :=
by rw [module.gsmul_eq_smul_cast  n x, int.cast_id n]

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 14:09):

Thanks

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 17:44):

/-- The natural ℤ-module structure on any `add_comm_group`. -/
-- We don't immediately make this a global instance, as it results in too many instances,
-- and confusing ambiguity in the notation `n • x` when `n : ℤ`.
-- We do turn it into a global instance, but only at the end of this file,
-- and I remain dubious whether this is a good idea.
def int_module : module  M :=

(Scott said this in algebra.module.basic). This is exactly what I've been seeing with finsupp.

I think these are missing:

lemma finsupp.smul_eq_nsmul {α : Type u} {B : Type v} [add_comm_monoid B] (n : )
  (x : α  B) : n  x = n  x :=
ext $ λ a, nat.rec_on n rfl $ λ d hd,
by rw [nat.succ_eq_add_one, add_nsmul, add_apply,  hd, one_nsmul, add_smul, add_apply, one_smul]

lemma finsupp.smul_eq_gsmul {α : Type u} {B : Type v} [add_comm_group B] (n : )
  (x : α  B) : n  x = n  x :=
ext $ λ a, int.induction_on n rfl
(λ i hi, by rw [add_one_gsmul, add_apply,  hi, add_smul, one_smul, add_apply])
(λ i hi, by rw [sub_gsmul, sub_apply,  hi, sub_smul, one_smul, one_gsmul, sub_apply ])

view this post on Zulip Kevin Buzzard (Aug 25 2020 at 17:55):

aah Chris just pointed out that these are special cases of module.gsmul_eq_smul etc.


Last updated: May 16 2021 at 05:21 UTC