Skip to content

Instantly share code, notes, and snippets.

@eric-wieser
Last active July 25, 2020 09:41
Show Gist options
  • Save eric-wieser/aacbfa18ba834afcdd61f8d668ba057f to your computer and use it in GitHub Desktop.
Save eric-wieser/aacbfa18ba834afcdd61f8d668ba057f to your computer and use it in GitHub Desktop.
An alternative formulation of finsupp.finsupp_prod_equiv
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment