dfinsupp of product is dfinsupp of dfinsupp

Stream: maths

[Eric Wieser]

I'm trying to obtain the equivalence in the following, (Π₀ (ij : ii × jj), β ij.1 ij.2) ≃ (Π₀ i j, β i j)

import data.dfinsupp
universes u v w

-- requirements of Π₀
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

I initially posted this over at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/dfinsupp.20of.20product.20is.20dfinsupp.20of.20dfinsupp/near/204537032.

Over there, you can see a definition of the forward transformation, (Π₀ (ij : ii × jj), β ij.1 ij.2)) → (Π₀ i, Π₀ j, β i j), but I'm struggling to de-sorry the reverse transformation.

I suspect my issue here is a lack of familiarity with quotient types in lean.

Help finishing those definitions would be greatly appreciated!

[Reid Barton]

do you need this for a random β, or are they actually at least add_comm_monoid?

[Eric Wieser]

Ideally a random β

[Eric Wieser]

I think the add_comm_monoid version probably applies better to direct_sum than to dfinsupp

[Eric Wieser]

I was also trying to avoid needing the decidability of {f : β i j}, f = 0, which is required if I try to use .support

[Eric Wieser]

(hence my attempts to go through pre_support instead.)

[Eric Wieser]

I've made a PR at https://github.com/leanprover-community/mathlib/pull/3515 which contains the bits of the proof I was able to put together, so that it's not completely lost to zulip streams.

[Utensil Song]

I don't understand why there would be "goals accomplished" and

tactic failed, result contains meta-variables
state:
no goals

at the same time for the following #mwe related to this PR:

[Utensil Song]

import data.dfinsupp
import tactic

universes u v w

namespace dfinsupp.prod

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

def prod_to_nested (f : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j := begin
  apply quotient.lift_on f,
  intros a b h,
  unfold has_equiv.equiv at h,
  unfold setoid.r at h,
  apply quotient.sound,
  intro i,
  simp [h],  -- goals accomplished
end -- result contains meta-variables

[Anne Baanen]

This happens when tactics claim to have solved all the metavariables (i.e. there are no more goals), but there are still metavariables that need to be filled out. You can use the recover tactic to get the missing goal.

[Anne Baanen]

More specifically, the line apply quotient.sound, causes a goal to be hidden, I guess because the tactic expects that it will be filled by unification. If you write refine quotient.sound _, instead, the goal will still be around.

[Chris Hughes]

I did manage to prove this, but it's not pretty (link). I think this might be a case of the #xy problem. dfinsupp is not really intended to be used unless the β i are add_comm_monoids, in fact it shouldn't really be used directly as dfinsupp, but you should use direct_sum instead most of the time for the interface. It is strange to want to use it with just has_zero, and the library really isn't set up for that usage.

[Eric Wieser]

This is just an x problem, I decided it was more challenging than my original y problem

[Eric Wieser]

Although I think if you're willing to assume[Π i j, decidable_eq (β i j)], there are some shorter solutions - my difficulty was trying to avoid that assumption