Signed tensor identities

The sign-twisted cycle product for constant sequences, and the signed Frobenius sum expressing the twisted trace in terms of Schur values at the negated sequence.

Helper: cycleProd at a constant sequence

theorem RS.cycleProd_const {n : ℕ} (c : ℂ) (π : Equiv.Perm (Fin n)) : cycleProd (fun (x : ℕ) => c) π = c ^ (π.cycleType.card + (n - π.cycleType.sum))

cycleProd at a constant sequence is a single power.

Helper: ℤˣ sign cast to ℂ

theorem RS.sign_cast_complex {n : ℕ} (π : Equiv.Perm (Fin n)) : ↑↑(Equiv.Perm.sign π) = (-1) ^ (π.cycleType.sum + π.cycleType.card)

The sign of a permutation, cast ℤˣ → ℤ → ℂ, equals (-1 : ℂ) raised to cycleType.sum + card cycleType.

Helper: parity identity

The sign twist of a constant cycle product

theorem RS.sign_mul_cycleProd_const {n : ℕ} (m : ℕ) (π : Equiv.Perm (Fin n)) : ↑↑(Equiv.Perm.sign π) * cycleProd (fun (x : ℕ) => ↑m) π = (-1) ^ n * cycleProd (fun (x : ℕ) => -↑m) π

The sign twist of a constant cycle product is the product at the negated constant.

The signed Frobenius sum

theorem RS.signed_tensor_sum (m : ℕ) (μ : YoungDiagram) : ∑ π : Equiv.Perm (Fin μ.card), jtChar μ π * (↑↑(Equiv.Perm.sign π) * cycleProd (fun (x : ℕ) => ↑m) π) = (-1) ^ μ.card * ↑μ.card.factorial * diagramSchur μ fun (x : ℕ) => -↑m

The signed Frobenius sum: the twisted trace is the Schur value at the negated sequence, up to the sign and the factorial.