## Stream: Is there code for X?

### Topic: dfinsupp of product is dfinsupp of dfinsupp

#### Eric Wieser (Jul 21 2020 at 11:39):

Is there anything in mathlib resembling the sorry here?

import data.dfinsupp
import tactic

universes u v w

variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, has_zero (β i j)]

example : (Π₀ (ij : ii × jj), β ij.1 ij.2) ≃ Π₀ i, Π₀ j, β i j := sorry


#### Scott Morrison (Jul 21 2020 at 12:29):

Quite possibly not. dfinsupp is not very well developed.

#### Eric Wieser (Jul 21 2020 at 14:07):

Is ≃ the right statement to try to make?

#### Scott Morrison (Jul 21 2020 at 14:10):

Depends what you need it for. Lots of algebra structures are going to be compatible with this equivalence, too.

#### Eric Wieser (Jul 21 2020 at 16:26):

I can make a start on this with:

def prod_to_nested (f : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j := begin
fapply quotient.lift_on f,
exact λ fij, ⟦{
to_fun := λ i, ⟦ {
to_fun := λ j, fij.to_fun (i, j),
pre_support := fij.pre_support.map (λ (ij : ii × jj), ij.snd),
zero := λ j, begin
obtain hin | h0 := fij.zero (i, j),
{apply or.inl, rw multiset.mem_map, use (i, j), simp only [hin, eq_self_iff_true, and_self]},
{exact or.inr h0},
end
} ⟧,
pre_support := fij.pre_support.map (λ ij, ij.fst),
zero := λ i, begin
have h := λ j, fij.zero (i, j),
rw multiset.mem_map,
sorry
end
}⟧,
exact λ a b H, quotient.sound $λ i, by { simp [H (i, _)], exact λ j, by simp [H (i, j)] }, end  although this all feels super awkward #### Eric Wieser (Jul 21 2020 at 18:27): Updated the above to be sorry-free, would appreciate feedback on whether I'm missing a trick. In paticular, the  λ j, (fij.zero (i, j)).elim proof is repeated twice, and I'm not sure how to remove it. #### Eric Wieser (Jul 21 2020 at 19:30): The other direction is proving even more challenging: def nested_to_prod (f : Π₀ i j, β i j) : Π₀ (ij : ii × jj), β ij.1 ij.2 := begin fapply quotient.lift_on f, { intro fi, refine ⟦{ to_fun := λ ij, fi.to_fun ij.fst ij.snd, pre_support := fi.pre_support.product (begin let j_sets := fi.pre_support.map (λ i, begin let fi_val := (fi.to_fun i), /- This is unprovable, I think lift_on is the wrong approach, or I need to return a clever quotient -/ exact quotient.lift_on fi_val dfinsupp.pre.pre_support (λ a b H, begin sorry end) end), /- should be union of j_sets -/ exact (sorry : multiset jj), end), zero := λ ij, begin rw multiset.mem_product, cases fi.zero ij.fst, { left, simp [h], sorry}, { right, simp [h] } end }⟧, }, exact λ a b H, quotient.sound$ λ ij, by simp [H ij.fst],
end


#### Eric Wieser (Jul 22 2020 at 11:51):

Would this be more suited to #general, now that it's established the answer to "is there code for X in mathlib" is no?

#### Johan Commelin (Jul 22 2020 at 11:52):

Yes, or #maths

#### Eric Wieser (Jul 22 2020 at 11:52):

Shall I repost, or ask someone with the magic bit to move it?

#### Johan Commelin (Jul 22 2020 at 11:52):

I think reposting is easier