An alternative formulation of finsupp.finsupp_prod_equiv

finsupp_prod_equiv.lean

import data.finsupp

namespace finsupp.eric

#check finset.sigma


universes u v w
def bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α → finset β) : finset (α × β)
  := (sa.sigma fb).map (equiv.sigma_equiv_prod _ _).to_embedding

lemma mem_bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α → finset β) (ab : α × β) :
  ab ∈ bind_prod sa fb ↔ ab.fst ∈ sa ∧ ab.snd ∈ fb ab.fst
:= begin
  unfold bind_prod,
  rw finset.mem_map,
  simp only [exists_prop, sigma.exists, finset.mem_sigma, equiv.to_embedding_coe_fn, equiv.sigma_equiv_prod, equiv.coe_fn_mk],
  split,
  {
    rintros ⟨a, b, ⟨ha, hb⟩, h⟩,
    simp only [← h],
    exact ⟨ha, hb⟩,
  },
  {
    rintros ⟨ha, hb⟩,
    use [ab.fst, ab.snd],
    simp only [ha, hb, true_and, prod.mk.eta],
  },
end

#check finset.mem_bind

variables {ii : Type u} {jj : Type v} {α : Type w} [has_zero α]

def uncurry (f : ii →₀ jj →₀ α) : ii × jj →₀ α := {
  support := bind_prod f.support (λ i, (f i).support),
  to_fun := λ ij, f ij.fst ij.snd,
  mem_support_to_fun := λ ij, iff.intro
    (λ h, begin
      rw mem_bind_prod at h,
      obtain ⟨hi, hj⟩ := h,
      rw (f ij.fst).mem_support_to_fun _ at hj,
      exact hj,
    end)
    (λ h, begin
      rw mem_bind_prod,
      split,
      {
        rw f.mem_support_to_fun,
        intro hf,
        apply h,
        unfold_coes,
        rw hf,
        refl,
      },
      {
        rw (f ij.fst).mem_support_to_fun,
        exact h,
      },
    end)
}

-- invocation of the curried function, separated for clarity
@[reducible]
private def curry_at [decidable_eq ii] [decidable_eq jj] (f : ii × jj →₀ α) (i : ii) : jj →₀ α := {
  support := (f.support.filter (λ (ij : ii × jj), ij.fst = i)).image prod.snd,
  to_fun := λ j, f (i, j),
  mem_support_to_fun := λ j, iff.intro
    (λ h, begin
      rw finset.mem_image at h,
      obtain ⟨ij, hij, rfl⟩ := h,
      rw finset.mem_filter at hij,
      obtain ⟨hij, rfl⟩ := hij,
      rw prod.mk.eta,
      rw ← finsupp.mem_support_iff,
      exact hij
    end)
    (λ h, begin
      rw finset.mem_image,
      use (i, j),
      rw finset.mem_filter,
      refine ⟨⟨_, rfl⟩, rfl⟩,
      rw finsupp.mem_support_iff,
      exact h,
    end)
}

lemma curry_at_eq [decidable_eq ii] [decidable_eq jj] (f : ii × jj →₀ α) (i : ii) (j : jj) : f (i, j) = curry_at f i j := begin
  unfold curry_at,
  unfold_coes,
end

def curry [decidable_eq ii] [decidable_eq jj] (f : ii × jj →₀ α) : ii →₀ jj →₀ α := {
  support := f.support.image prod.fst,
  to_fun := curry_at f,
  mem_support_to_fun := λ i, ⟨λ h, begin
    rw finset.mem_image at h,
    obtain ⟨ij, hij, rfl⟩ := h,
    intro h2,
    rw finsupp.ext_iff at h2,
    specialize h2 ij.snd,
    rw finsupp.zero_apply at h2,
    rw [← curry_at_eq, prod.mk.eta] at h2,
    rw finsupp.mem_support_iff at hij,
    exact hij h2,
  end, λ h, begin
    rw finset.mem_image,
    rw ne.def at h,
    conv at h {
      congr,
      rw [finsupp.ext_iff],
      simp [finsupp.zero_apply, ← curry_at_eq], 
    },
    -- I wonder if we can avoid classical here
    simp [classical.not_forall, ← ne.def] at h,
    obtain ⟨j, hb⟩ := h,
    use (i, j),
    refine ⟨_, rfl⟩,
    rw finsupp.mem_support_iff,
    exact hb,
  end⟩
}

def prod_equiv [decidable_eq ii] [decidable_eq jj] : (ii × jj →₀ α) ≃ (ii →₀ jj →₀ α) := {
  to_fun := curry,
  inv_fun := uncurry,
  left_inv := begin
    intro f_prod,
    rw finsupp.ext_iff,
    intro ij,
    unfold uncurry curry,
    unfold_coes,
    simp only [prod.mk.eta],
    unfold_coes,
  end,
  right_inv := begin
    intro f_nested,
    rw finsupp.ext_iff,
    intro i,
    rw finsupp.ext_iff,
    intro j,
    unfold uncurry curry,
    unfold_coes,
    simp only [],
    unfold_coes,
  end }

-- note different assumptions
/-
noncomputable def finsupp.finsupp_prod_equiv :
  Π {α : Type u_1} {β : Type u_2} {γ : Type u_3} [_inst_1 : add_comm_monoid γ],
  (α × β →₀ γ) ≃ (α →₀ β →₀ γ) := ...
-/
#print finsupp.finsupp_prod_equiv

/-
def finsupp.eric.prod_equiv :
  Π {ii : Type u} {jj : Type v} {α : Type w} [_inst_1 : decidable_eq ii] [_inst_2 : decidable_eq jj] [_inst_3 : has_zero α],
  (ii × jj →₀ α) ≃ (ii →₀ jj →₀ α) := ...
-/
#print prod_equiv


end finsupp.eric