sigma_finsupp_to_dfinsupp

Stream: Is there code for X?

[Riccardo Brasca]

Hi all, I am trying to prove the following

import linear_algebra.dfinsupp

variables {ι : Type*} {R : Type*} {η : ι → Type*} {N : Type*}
variables [semiring R] [add_comm_monoid N] [module R N]

noncomputable theory
open_locale classical

local attribute [-instance] mul_zero_class.to_has_zero finsupp.has_zero
  finsupp.add_zero_class finsupp.add_monoid

def sigma_finsupp_to_dfinsupp : ((Σ i, η i) →₀ N) →ₗ[R] (Π₀ i, (η i →₀ N)) :=
{ to_fun := λ f, dfinsupp.mk (finsupp.split_support f) (λ i, finsupp.split f _),
  map_add' := sorry,
  map_smul' := sorry, }

(this is a linear equivalence, but let's start with this). The proof of map_add' seems quite painful: I can do it (I think) by several by_cases, looking at f.split_support, g.split_support and (f + g).split_support. Do someone see a better way of doing this? Maybe avoiding dfinsupp.mk or something.

[Riccardo Brasca]

Note that the line local attribute [-instance] mul_zero_class.to_has_zero finsupp.has_zero finsupp.add_zero_class finsupp.add_monoid is necessary, otherwise Lean is unable to find the R-module instance on (Π₀ i, (η i →₀ N)).

[Kevin Buzzard]

import linear_algebra.dfinsupp

variables {ι : Type*} {R : Type*} {η : ι → Type*} {N : Type*}
variables [semiring R] [add_comm_monoid N] [module R N]

noncomputable theory
open_locale classical

lemma not_iff_of_iff_not {P Q : Prop} : (P ↔ ¬ Q) → (¬ P ↔ Q) := by tauto!

namespace finsupp

lemma not_mem_split_support_iff_zero {ι M : Type*} {αs : ι → Type*}
  [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) (i : ι) :
  i ∉ split_support l ↔ split l i = 0 :=
not_iff_of_iff_not $ mem_split_support_iff_nonzero _ _

end finsupp

open finsupp

@[simp] lemma dfinsupp.mk_split_apply (f : (Σ i, η i) →₀ N) (x : ι) (a : η x) :
  (dfinsupp.mk (finsupp.split_support f) (λ i, finsupp.split f _) : Π₀ i, (η i →₀ N)) x a =
  f ⟨x, a⟩ :=
begin
  rw dfinsupp.mk_apply,
  split_ifs,
  { refl },
  { rw not_mem_split_support_iff_zero at h,
    rw [← finsupp.split_apply, h] },
end

-- this should be fixed, not worked around...
local attribute [-instance] mul_zero_class.to_has_zero finsupp.has_zero
  finsupp.add_zero_class finsupp.add_monoid

def sigma_finsupp_to_dfinsupp : ((Σ i, η i) →₀ N) →ₗ[R] (Π₀ i, (η i →₀ N)) :=
{ to_fun := λ f, dfinsupp.mk (finsupp.split_support f) (λ i, finsupp.split f _),
  map_add' := begin
    intros f g,
    ext x,
    simp [-dfinsupp.mk_apply],
  end,
  map_smul' := begin
    intros r f,
    ext x,
    simp [-dfinsupp.mk_apply],
  end }

[Riccardo Brasca]

I just had the idea of something like dfinsupp.mk_split_apply, but you are too fast!

I agree that the problem with local attribute [-instance]... should be fixed, but I think it's a little to complicated for me...

[Eric Wieser]

I think you can do better by avoiding dfinsupp.mk, which introduces an annoying if

[Riccardo Brasca]

My idea was to prove immediately after the definition

lemma foo {η : ι → Type*} (f : ((Σ i, η i) →₀ N)) :
finsupp.split f = sigma_finsupp_to_dfinsupp f

so for all the proof I can move to (Π i, (η i →₀ N)), where the claim are more or less obvious.

[Riccardo Brasca]

I was looking for a direct way to construct an element of (Π₀ i, (η i →₀ N)) from an element of (Π i, (η i →₀ N)) and a proof that the support is finite, but this seems to be missing.

[Eric Wieser]

Here's the mk-free version:

import linear_algebra.dfinsupp

variables {ι : Type*} {R : Type*} {η : ι → Type*} {N : Type*}
variables [semiring R] [add_comm_monoid N] [module R N]

noncomputable theory
open_locale classical

-- this lemmas should definitely exist
@[simp]
lemma dfinsupp.coe_mk [∀i, has_zero (η i)] (f : Π i, η i) (s : multiset ι) (hf) :
  ⇑(⟦dfinsupp.pre.mk f s hf⟧ : Π₀ i, η i) = f := rfl

namespace finsupp

-- this should be fixed, not worked around...
local attribute [-instance] mul_zero_class.to_has_zero finsupp.has_zero
  finsupp.add_zero_class finsupp.add_monoid

def sigma_finsupp_to_dfinsupp : ((Σ i, η i) →₀ N) →ₗ[R] (Π₀ i, (η i →₀ N)) :=
{ to_fun := λ f, ⟦⟨finsupp.split f, (finsupp.split_support f : finset ι).val, λ i, begin
    rw [←finset.mem_def, mem_split_support_iff_nonzero],
    exact (decidable.em _).symm
  end⟩⟧,
  map_add' := λ f g, begin
    ext,
    simp [finsupp.split_apply],
  end,
  map_smul' := λ r f, begin
    ext,
    simp [finsupp.split_apply],
  end }

[Eric Wieser]

This one has the nice property that finsupp.split f = sigma_finsupp_to_dfinsupp f is true by rfl

[Riccardo Brasca]

Ah, it's dfinsupp.pre.mk!

[Riccardo Brasca]

I am trying to investigate why local attribute [-instance] finsupp.has_zero is needed. The workaround has been suggested by @Anne Baanen here
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/finite.20free.20modules/near/240928594

Here is a minimal example showing that something is wrong, but lemma test is indeed true by rfl (I am not sure it is relevant). I don't have a clue about how to correct this, but if you have any indication I can work on it.

import data.dfinsupp
import data.finsupp.basic

variables {ι : Type*} {N : Type*} {η : ι → Type*}

lemma test [h : add_zero_class N] :
  @add_zero_class.to_has_zero (ι →₀ N) (@finsupp.add_zero_class ι N h) =
  @finsupp.has_zero ι N (@add_zero_class.to_has_zero N h) := rfl

--this fail
--noncomputable lemma foo1 [h : add_zero_class N] : has_add (Π₀ i, (η i →₀ N)) := by apply_instance

local attribute [-instance] finsupp.has_zero

--this works
noncomputable lemma foo2 [h : add_zero_class N] : has_add (Π₀ i, (η i →₀ N)) := by apply_instance

[Eric Wieser]

#7806 contains dfinsupp.coe_mk, renamed to dfinsupp.coe_pre_mk