The sign character of a symmetric group

Mathlib's Equiv.Perm.sign is valued in ℤˣ. Representation theory wants the linear character it induces over a coefficient ring: the homomorphism Equiv.Perm α →* kˣ obtained by pushing the sign forward along ℤ → k. That is TauCeti.signLinearCharacter, and it is the sgn of the character tables and of the induction examples -- the one-dimensional representation it carries is FDRep.ofLinearCharacter (signLinearCharacter k α), and restricting it along a subgroup inclusion is precomposition, so a subgroup meets it as (signLinearCharacter k α).comp H.subtype.

Only two facts are needed to compute with it, and both are recorded here: its value in k is the sign cast into k, and it sends a transposition to -1. In characteristic two those two values coincide and the character is trivial; every statement that needs it to be nontrivial has to say so by excluding that characteristic.

Main definitions

• TauCeti.signLinearCharacter: the sign of a permutation, as a linear character valued in kˣ.

Main statements

• TauCeti.coe_signLinearCharacter_apply: its value in k is the sign of the permutation, cast.
• TauCeti.signLinearCharacter_swap: it sends a transposition to -1.

def TauCeti.signLinearCharacter (k : Type u) [Ring k] (α : Type v) [DecidableEq α] [Fintype α] : Equiv.Perm α →* kˣ

The sign character of a symmetric group: the linear character of Equiv.Perm α sending a permutation to its sign, read in the units of k along the ring homomorphism ℤ → k.

Equations

• TauCeti.signLinearCharacter k α = (Units.map ↑(Int.castRingHom k)).comp Equiv.Perm.sign

@[simp]

theorem TauCeti.coe_signLinearCharacter_apply {k : Type u} [Ring k] {α : Type v} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) : ↑((signLinearCharacter k α) σ) = ↑↑(Equiv.Perm.sign σ)

The value of the sign character in k is the sign, cast into k. This is the defining equation: the definition itself is not exposed, and every computation with the character goes through this lemma and TauCeti.signLinearCharacter_swap.

@[simp]

theorem TauCeti.signLinearCharacter_swap {k : Type u} [Ring k] {α : Type v} [DecidableEq α] [Fintype α] {i j : α} (h : i ≠ j) : (signLinearCharacter k α) (Equiv.swap i j) = -1

The sign character sends a transposition to -1. Over a ring of characteristic two this value is 1, which is why nontriviality of the character always carries a hypothesis on the characteristic.