Zulip Chat Archive

Stream: Is there code for X?

Topic: Converting a finset to a list


view this post on Zulip Eric Wieser (Dec 08 2020 at 16:56):

I want to express the statement:

lemma sign.map_prod {α β : Sort*} [decidable_eq α] [fintype α] :  (f : β  perm α) (s : finset β),
    sign ( x in s, f x) =  x in s, sign (f x)

But I can't, because requires its argument to be commutative, and the one on the LHS is not.
How can I convert s into a list so that I can express the LHS using list.prod?

view this post on Zulip Reid Barton (Dec 08 2020 at 16:57):

How about starting with a list?

view this post on Zulip Reid Barton (Dec 08 2020 at 16:57):

Otherwise the product is not well-defined

view this post on Zulip Eric Wieser (Dec 08 2020 at 16:58):

Well, the lemma is true whichever of the non well-defined definitions you pick

view this post on Zulip Reid Barton (Dec 08 2020 at 17:00):

but... the lemma has to mean something...

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:04):

To un-#xy my problem, I'm trying to show that (sigma_congr_right σ).sign = ∏ a, (σ a).sign, and I thought I'd do so by breaking down (sigma_congr_right σ) into a product of function.update 1 a (σ a)

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:04):

Since the analogous approach worked for the simpler version expressed with sum

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:05):

But I don't know how to express that product

view this post on Zulip Reid Barton (Dec 08 2020 at 17:33):

You lost me at function.update... but surely if you want to write a permutation as a product, it has to be a product of a list

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:33):

The elements in the list all commute

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:33):

But yes, I guess I could

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:34):

But then I need to push finset.univ αinto that list

view this post on Zulip Reid Barton (Dec 08 2020 at 17:34):

docs#equiv.perm.sign_prod_congr_right looks similar except all the permutations are of the same set there

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:35):

Far from a #mwe, but the sorry in question is here: https://github.com/leanprover-community/mathlib/compare/eric-wieser/sigma_congr_right_sign?expand=1#diff-126733ed2b8b67441355f6f20dbb566366f0dd0844a7d7b6ee5e7c6671c46e68R844

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:35):

Oh sure enough, that contains the fintype.exists_univ_list α which I needed

view this post on Zulip Eric Wieser (Dec 08 2020 at 17:44):

Thanks for point me at that, that's enough to get me going.


Last updated: May 19 2021 at 02:10 UTC