
[Sep. 19th, 201606:37 pm]
Jason

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 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 melement 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 say
sum_{rho in S_m} sum_{zeta in S_m} prod_{rho^1 k in 1..m} f(rho^1 k, zeta k, k) 

