to_module and map_range

Stream: Is there code for X?

[Winston Yin]

I'm composing direct_sum.to_module with dfinsupp.map_range. Is there any way to simplify that? Here's what I'm doing. I have:

• a collection of spaces V : ι → Type _, each of which is a module k (V i),
• a target space W : Type _ as a module k W,
• a collection of linear maps ρ : Π i : ι, V i →ₗ[k] V i, and
• a collection of linear maps φ : Π i : ι, V i →ₗ[k] W.
  What I need is that ∀ (v : direct_sum ι V), (direct_sum.to_module k ι W φ) (dfinsupp.map_range.linear_map ρ v) = direct_sum.to_module k ι W (λ i : ι, (φ i).comp (ρ i)) v.

[Winston Yin]

Is there something similar to dfinsupp.map_range_comp but for composing to_module and map_range?

[Kevin Buzzard]

Can you just make a #mwe ? It would be much easier for me to digest!

[Eric Wieser]

Your best bet is to unfold to_module

[Eric Wieser]

There are lots of lemmas about dfinsupp, and it's a lot of effort for little gain to copy all the lemmas between the two

[Winston Yin]

variables
  {k : Type _} [comm_semiring k]
  {A : Type _} [semiring A] [algebra k A]
  (ι : Type _) [decidable_eq ι] {V : ι → Type _}
  [Π (i : ι), add_comm_monoid (V i)] [Π (i : ι), module k (V i)]
  {W : Type _} [add_comm_monoid W] [module k W]
  (ρ : Π i : ι, V i →ₗ[k] V i)
  (φ : Π i : ι, V i →ₗ[k] W)

example : ∀ (v : direct_sum ι V), (direct_sum.to_module k ι W φ) (dfinsupp.map_range.linear_map ρ v) = direct_sum.to_module k ι W (λ i : ι, (φ i).comp (ρ i)) v := sorry

[Winston Yin]

After a bit a struggle, I was able to prove the above statement as follows:

example : ∀ (v : direct_sum ι V), (direct_sum.to_module k ι W φ) (dfinsupp.map_range.linear_map ρ v) = direct_sum.to_module k ι W (λ i : ι, (φ i).comp (ρ i)) v :=
begin
  intro vv,
  rw ←linear_map.comp_apply,
  apply direct_sum.to_module.ext,
  intro i,
  change λ (i : ι), V i with V,
  apply linear_map.ext,
  intro v,
  rw linear_map.comp_apply,
  rw linear_map.comp_apply,
  rw linear_map.comp_apply,
  rw direct_sum.to_module_lof,
  simp,
  rw ←direct_sum.single_eq_lof,
  unfold direct_sum.to_module dfinsupp.lsum,
  simp
end

It seems to me that it would be useful to include (some more general form of) this lemma in data.dfinsupp, as it is probably common to build a map by composing lsum (direct sum to module) with map_range (direct sum to direct sum).

[Eric Wieser]

Is there no lemma that says docs#dfinsupp.map_range is lsum combined with single?

[Winston Yin]

Perhaps I could have used dfinsupp.map_range_single, but I've now moved on