## Stream: Is there code for X?

### Topic: big_operators and bijections

#### 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


#### 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).

#### 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.

#### 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?

#### 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?

#### Johan Commelin (Oct 17 2020 at 04:18):

I think there is also sum_equiv

#### Johan Commelin (Oct 17 2020 at 04:18):

Let me search a bit

#### Johan Commelin (Oct 17 2020 at 04:24):

Test: docs#equiv.sum_comp

#### 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.

#### 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