### (no subject)

Actually figured out the proof now, see https://twitter.com/jcreed/status/778001357160808448/photo/1 for impenetrable details.

The bit I like most about it is how it actually uses the fact that the group of permutations

It comes up because I'm summing twice over all permutations of an m-element set, and then considering a product over all elements in that set, so like

sum_{rho in S_m} sum_{pi in S_m} prod_{j in 1..m} f(j, pi j, rho j)

There's one kind of reindexing that I am somewhat used to, which is replacing j with an expression like rho^-1 k to get

sum_{rho in S_m} sum_{pi in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, pi rho^-1 k, k)

and using the fact that rho is an isomorphism acting on the set 1..m to drop the rho^-1 from the product:

sum_{rho in S_m} sum_{pi in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, pi rho^-1 k, k)

The extra neat thing is exactly that you can do a substitution 'one level up' and say pi = zeta o rho

sum_{rho in S_m} sum_{(zeta o rho) in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, zeta k, k)

and reason that since rho acting

sum_{rho in S_m} sum_{zeta in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, zeta k, k)

The bit I like most about it is how it actually uses the fact that the group of permutations

*acting on itself*always yields isomorphism. This may sounds like a stupidly elementary fact about group theory, but it's just not a thing that I've had to use very often in manipulating expressions with pis and sigmas.It comes up because I'm summing twice over all permutations of an m-element set, and then considering a product over all elements in that set, so like

sum_{rho in S_m} sum_{pi in S_m} prod_{j in 1..m} f(j, pi j, rho j)

There's one kind of reindexing that I am somewhat used to, which is replacing j with an expression like rho^-1 k to get

sum_{rho in S_m} sum_{pi in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, pi rho^-1 k, k)

and using the fact that rho is an isomorphism acting on the set 1..m to drop the rho^-1 from the product:

sum_{rho in S_m} sum_{pi in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, pi rho^-1 k, k)

The extra neat thing is exactly that you can do a substitution 'one level up' and say pi = zeta o rho

sum_{rho in S_m} sum_{(zeta o rho) in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, zeta k, k)

and reason that since rho acting

*on S_m*is an isomorphism, you might as well saysum_{rho in S_m} sum_{zeta in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, zeta k, k)