Slot labellings and the Koszul sign of a permutation

The combinatorial half of the transport. A word Fin n → Bool records which slots of a tensor power carry the odd line, a permutation reindexes it, and the induced permutation of the odd slots alone has a sign — the sign a symmetric category produces when the letters of the word are permuted, one factor of −1 per crossing of two odd letters. Nothing here mentions a category; the categorical side consumes it in Letters.lean.

• permIndex: the reindexing of a slot labelling by a permutation, with its two functoriality laws.
• trueSet, popCount_eq_card: the odd slots of a word.
• oddPerm, parSign: the induced permutation of the odd slots and its sign, with oddPerm_mul and parSign_mul, and the value parSign_swap on an adjacent transposition.

Reindexing slot labellings

A permutation routes the factor in slot i to slot σ i (permMor); the labelling of the slots follows along.

def RS.permIndex {K : Type u_1} {n : ℕ} (σ : Equiv.Perm (Fin n)) (c : Fin n → K) : Fin n → K

Reindexing a slot labelling along a permutation: the label of slot i moves to slot σ i.

Equations

• RS.permIndex σ c = c ∘ ⇑σ⁻¹

@[simp]

theorem RS.permIndex_one {K : Type u_1} {n : ℕ} (c : Fin n → K) : permIndex 1 c = c

The identity permutation does not move labels.

theorem RS.permIndex_apply {K : Type u_1} {n : ℕ} (σ : Equiv.Perm (Fin n)) (c : Fin n → K) (i : Fin n) : permIndex σ c i = c (σ⁻¹ i)

The label a slot receives under reindexing.

theorem RS.permIndex_apply_self {K : Type u_1} {n : ℕ} (σ : Equiv.Perm (Fin n)) (c : Fin n → K) (i : Fin n) : permIndex σ c (σ i) = c i

The label of the image slot is the original label.

The odd slots of a word and the Koszul sign

For a parity word w : Fin n → Bool the true slots are the odd ones. A permutation induces a bijection from the odd slots of w to those of the shuffled word; conjugating by the monotone enumerations gives a permutation of Fin (popCount w) whose sign is the Koszul sign of the shuffle.

def RS.trueSet {n : ℕ} (w : Fin n → Bool) : Finset (Fin n)

The set of true slots of a word.

Equations

• RS.trueSet w = {i : Fin n | w i = true}

theorem RS.mem_trueSet {n : ℕ} {w : Fin n → Bool} {i : Fin n} : i ∈ trueSet w ↔ w i = true

Membership in the true slots.

theorem RS.popCount_eq_card {n : ℕ} (w : Fin n → Bool) : popCount w = (trueSet w).card

popCount is the size of the set of true slots.

theorem RS.trueSet_permIndex {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : trueSet (permIndex σ w) = Finset.map (Equiv.toEmbedding σ) (trueSet w)

Reindexing maps the true slots along the permutation.

theorem RS.popCount_permIndex {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : popCount (permIndex σ w) = popCount w

Reindexing preserves the number of true slots.

noncomputable def RS.trueEnum {n : ℕ} (w : Fin n → Bool) : Fin (popCount w) ≃o ↥(trueSet w)

The monotone enumeration of the true slots.

Equations

• RS.trueEnum w = (RS.trueSet w).orderIsoOfFin ⋯

def RS.trueShift {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : ↥(trueSet w) ≃ ↥(trueSet (permIndex σ w))

A permutation carries the true slots of a word bijectively onto the true slots of the shuffled word.

Equations

• RS.trueShift σ w = Equiv.subtypeEquiv σ ⋯

theorem RS.trueShift_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) (i : ↥(trueSet w)) : ↑((trueShift σ w) i) = σ ↑i

The shift, applied.

noncomputable def RS.oddPerm {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : Equiv.Perm (Fin (popCount w))

The induced permutation on the odd slots: conjugate the shift by the monotone enumerations.

Equations

• RS.oddPerm σ w = (RS.trueEnum w).trans ((RS.trueShift σ w).trans ((RS.trueEnum (RS.permIndex σ w)).symm.trans (finCongr ⋯)))

theorem RS.oddPerm_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) (x : Fin (popCount w)) : (oddPerm σ w) x = (finCongr ⋯) ((trueEnum (permIndex σ w)).symm ((trueShift σ w) ((trueEnum w) x)))

The induced permutation, applied.

noncomputable def RS.parSign {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : ℂ

The Koszul sign of a shuffle: the sign of the induced permutation of the odd slots.

Equations

• RS.parSign σ w = ↑↑(Equiv.Perm.sign (RS.oddPerm σ w))

@[simp]

theorem RS.parSign_one {n : ℕ} (w : Fin n → Bool) : parSign 1 w = 1

The identity shuffles nothing: its Koszul sign is 1.

theorem RS.oddPerm_val {n : ℕ} (σ : Equiv.Perm (Fin n)) (w : Fin n → Bool) (x : Fin (popCount w)) : ↑((oddPerm σ w) x) = ↑((trueEnum (permIndex σ w)).symm ((trueShift σ w) ((trueEnum w) x)))

The value of the induced permutation, as a slot number.

theorem RS.oddPerm_mul {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : oddPerm (σ * τ) w = (finCongr ⋯).permCongr (oddPerm σ (permIndex τ w)) * oddPerm τ w

The induced permutation is multiplicative, up to transport of the count equality.

theorem RS.parSign_mul {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (w : Fin n → Bool) : parSign (σ * τ) w = parSign σ (permIndex τ w) * parSign τ w

The Koszul sign is a cocycle for the shuffle action.

The Koszul sign of an adjacent transposition

An adjacent swap crosses exactly one pair of letters: its Koszul sign is −1 when both are odd and 1 otherwise.

theorem RS.parSign_swap {n : ℕ} (i : Fin n) (w : Fin (n + 1) → Bool) : parSign (Equiv.swap i.castSucc i.succ) w = if w i.castSucc = true ∧ w i.succ = true then -1 else 1

The Koszul sign of an adjacent transposition: −1 when both crossed letters are odd, 1 otherwise.