Zulip Chat Archive

Stream: maths

Topic: stuck on generalising finsupp.to_module


view this post on Zulip Johan Commelin (May 28 2018 at 11:35):

I really don't see why I'm getting stuck here. See the two comment lines just after the first sorry.

/- should this be stronger? [module γ β] → module γ (α →₀ β) -/   -- yes!
def to_module [decidable_eq γ] [ring β] [module β γ] : module β (α  γ) :=
{ smul     := begin
                intros r f,
                apply f.map_range (() r) _,
                simp
              end, -- (•)
  smul_add := begin
                intros r f g,
                apply finsupp.ext,
                intro a,
                simp,
                rw smul_add,
                sorry
  end, -- assume a x y, finsupp.ext $ by simp [mul_add], -- original
  -- assume a x y, finsupp.ext $ by simp [map_range,smul_add], -- why doesn't this one work? <=====
  add_smul := sorry, --assume a x y, finsupp.ext $ by simp [add_mul],
  one_smul := assume x, finsupp.ext $ by simp,
  mul_smul := assume r s x, finsupp.ext $ by simp [mul_smul],
  .. finsupp.add_comm_group }

view this post on Zulip Johan Commelin (May 28 2018 at 11:47):

Never mind. I just realised that is_linear_map is not a class. Not going down the rabbit hole of modules.

view this post on Zulip Kenny Lau (May 28 2018 at 11:47):

linear_map is

view this post on Zulip Johan Commelin (May 28 2018 at 11:49):

And where does that beast live?

view this post on Zulip Johan Commelin (May 28 2018 at 11:49):

not in algebra/module

view this post on Zulip Johan Commelin (May 28 2018 at 11:52):

Ok, I found it... thanks!


Last updated: May 19 2021 at 02:10 UTC