finsupp gsmul_eq_smul

Stream: Is there code for X?

[Kevin Buzzard]

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

[Scott Morrison]

does ext help?

[Kevin Buzzard]

yes

[Kevin Buzzard]

⊢ module ℤ (α →₀ ℤ)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Thanks

[Kevin Buzzard]

/-- 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 ])

[Kevin Buzzard]

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