Zulip Chat Archive

Stream: maths

Topic: dfinsupp of product is dfinsupp of dfinsupp


view this post on Zulip Eric Wieser (Jul 22 2020 at 11:57):

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!

view this post on Zulip Reid Barton (Jul 22 2020 at 11:58):

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

view this post on Zulip Eric Wieser (Jul 22 2020 at 11:59):

Ideally a random β

view this post on Zulip Eric Wieser (Jul 22 2020 at 11:59):

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

view this post on Zulip Eric Wieser (Jul 22 2020 at 12:01):

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

view this post on Zulip Eric Wieser (Jul 22 2020 at 12:02):

(hence my attempts to go through pre_support instead.)

view this post on Zulip Eric Wieser (Jul 22 2020 at 14:45):

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.

view this post on Zulip Utensil Song (Jul 23 2020 at 12:01):

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:

view this post on Zulip Utensil Song (Jul 23 2020 at 12:02):

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

view this post on Zulip Anne Baanen (Jul 23 2020 at 12:04):

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.

view this post on Zulip Anne Baanen (Jul 23 2020 at 12:08):

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.

view this post on Zulip Chris Hughes (Jul 23 2020 at 15:52):

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.

view this post on Zulip Eric Wieser (Jul 23 2020 at 21:59):

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

view this post on Zulip Eric Wieser (Jul 24 2020 at 07:42):

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


Last updated: May 14 2021 at 20:13 UTC