# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Splitting a finset.sum over an involutive function

#### Eric Wieser (Nov 28 2020 at 10:56):

If I have an involutive function `f : A -> A`

where there is no `a`

st `f a = a`

, then I can argue that `sum a \in finset.univ A, g a`

can be rewritten into `sum a \in half_of_univ, g a + g (f a)`

. How would I begin to formalize this?

#### Kevin Buzzard (Nov 28 2020 at 11:09):

I ran into this problem in 2018 and I think there ended up being a lemma in mathlib which could help.

#### Kevin Buzzard (Nov 28 2020 at 11:11):

I'm thinking of docs#finset.prod_involution which probably isn't much help for you. It's related, but probably not enough.

#### Eric Wieser (Nov 28 2020 at 11:15):

Now that I have vs code to hand to type stuff, I think an auxiliary lemma that would be enough is

```
example {α : Type*} (f : α → α) (hf : function.involutive f) (hf' : ∀ a, f a ≠ a) :
∃ (x : set α), x ∪ f '' x = set.univ ∧ x ∩ f '' x = ∅ := sorry
```

#### Kevin Buzzard (Nov 28 2020 at 11:15):

As a mathematician my immediate instinct would be to be summing over equivalence classes. `half_of_univ`

could be the noncomputable `out`

or whatever it's called. You'll have to do something to choose the x.

#### Kevin Buzzard (Nov 28 2020 at 11:16):

Right, that set is the image of the noncomputable injection that you get from the surjection from alpha to alpha/~

#### Kevin Buzzard (Nov 28 2020 at 11:17):

the noncomputable injection gives you an isomorphism alpha = q x bool where q is the quotient.

#### Eric Wieser (Nov 28 2020 at 11:18):

docs#finset.sum_involution looks like it has everything I need

#### Kevin Buzzard (Nov 28 2020 at 11:18):

the definition of the equivalence associated to an involution is in TPIL near the end

#### Eric Wieser (Nov 28 2020 at 11:19):

https://leanprover.github.io/theorem_proving_in_lean/search.html?q=involution gives nothing

#### Kevin Buzzard (Nov 28 2020 at 11:19):

it's in the bit about quotients at the very end

#### Kevin Buzzard (Nov 28 2020 at 11:20):

oh I misremembered, it's making unordered pairs from ordered pairs. Section 11.4.

#### Eric Wieser (Nov 28 2020 at 11:30):

docs#finset.sum_cancels_of_partition_cancels is also close to what I want

Last updated: May 07 2021 at 22:14 UTC