Splitting a finset.sum over an involutive function

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Eric Wieser]

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