Zulip Chat Archive
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
Johan Commelin (Jul 22 2020 at 11:52):
Just add a link to this thread
Eric Wieser (Jul 22 2020 at 12:14):
Last updated: Dec 20 2023 at 11:08 UTC