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

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