Zulip Chat Archive

Stream: Is there code for X?

Topic: big_operators and bijections


view this post on Zulip Heather Macbeth (Oct 17 2020 at 01:56):

I would like to use the fact that one can pull back a sum over a fintype under a bijection. I can prove this as follows:

lemma sum_bij'' {α : Type*} {β : Type*} {γ : Type*} [add_comm_monoid β] [fintype α] [fintype γ]
  {g : γ  β} (i : α  γ) (i_inj : injective i) (i_surj : surjective i) :
  ( x, g (i x)) = ( x, g x) :=
begin
  refine finset.sum_bij _ _ _ (λ a₁ a₂ _ _ , @i_inj a₁ a₂) _,
  { simp },
  { simp },
  { intros b _,
    obtain a, ha := @i_surj b,
    exact a, finset.mem_univ a, ha.symm },
end

view this post on Zulip Heather Macbeth (Oct 17 2020 at 01:57):

As one can see, the key point of the proof is docs#finset.sum_bij. I found the hypotheses there quite hard to check, which is why I wrote my own lemma (for now -- not sure whether it's appropriate for a PR).

view this post on Zulip Heather Macbeth (Oct 17 2020 at 01:58):

But I was wondering if I am missing some folk wisdom on how to use a lemma like this docs#finset.sum_bij neatly.

view this post on Zulip Heather Macbeth (Oct 17 2020 at 01:59):

For example, the "surjectivity" hypothesis on that lemma is

 (b : γ), b  t  ( (a : α) (ha : a  s), b = i a ha)

Is there a cleaner way of deducing this from surjective i than what I wrote?

view this post on Zulip Heather Macbeth (Oct 17 2020 at 02:00):

And perhaps more generally, docs#finset.sum_bij is written for a strange object of type Π (a : α), a ∈ s → γ -- effectively a partially defined function. I can see why that choice is made, but how do I turn my actual function i into an object like this?

view this post on Zulip Johan Commelin (Oct 17 2020 at 04:18):

I think there is also sum_equiv

view this post on Zulip Johan Commelin (Oct 17 2020 at 04:18):

Let me search a bit

view this post on Zulip Johan Commelin (Oct 17 2020 at 04:24):

Test: docs#equiv.sum_comp

view this post on Zulip Johan Commelin (Oct 17 2020 at 04:25):

@Heather Macbeth If you upgrade your map i to an equiv then you're done by that lemma.

view this post on Zulip Heather Macbeth (Oct 17 2020 at 04:27):

Great! Thank you! Actually my map was already an equiv, I downgraded it to try to match the other lemma :)


Last updated: May 17 2021 at 16:26 UTC