More about lengths and simples

This file continues the study of lengths of permutations, building on the basic definitions of inversions and Lehmer codes. The main results are:

1. The length of a permutation equals the length of its inverse
2. The single swap lemma: how length changes when multiplying by a simple transposition
3. How length changes when multiplying by an arbitrary transposition
4. The first reduced word theorem: every permutation can be written as a product of exactly ℓ(σ) simple transpositions
5. Properties of length under composition

Main definitions

• Equiv.Perm.simpleTransposition - The simple transposition s_k that swaps k and k+1 (equivalent to AlgebraicCombinatorics.simpleTransposition, see simpleTransposition_eq_canonical)
• Equiv.Perm.inversions - The set of inversions (equivalent to AlgebraicCombinatorics.Perm.inv)
• Equiv.Perm.length - The length/inversion count (equivalent to AlgebraicCombinatorics.Perm.invCount)
• Equiv.Perm.lehmerEntry - Alias for AlgebraicCombinatorics.Perm.lehmerEntry
• Equiv.Perm.lehmerCode - The Lehmer code as a list (uses AlgebraicCombinatorics.Perm.lehmerCode_toList)
• Equiv.Perm.lehmerBlock - The block of simple transpositions for row i
• Equiv.Perm.canonicalReducedWord - The canonical reduced word from the Lehmer code

Equivalence lemmas

This file defines local versions of concepts from Inversions1.lean and Basics.lean, providing explicit equivalence lemmas to bridge between the different naming conventions:

• inversions_eq_inv - Equiv.Perm.inversions σ = AlgebraicCombinatorics.Perm.inv σ
• length_eq_invCount - Equiv.Perm.length σ = AlgebraicCombinatorics.Perm.invCount σ
• simpleTransposition_eq_canonical - Equiv.Perm.simpleTransposition k = AlgebraicCombinatorics.simpleTransposition k

Which definitions to use?

The definitions in this file (Equiv.Perm.inversions, Equiv.Perm.length, etc.) and those in Inversions1.lean (AlgebraicCombinatorics.Perm.inv, AlgebraicCombinatorics.Perm.invCount, etc.) are definitionally equal (provable by rfl). Choose based on context:

Use case	Recommended namespace
Basic inversion properties	AlgebraicCombinatorics.Perm (Inversions1.lean)
Lehmer codes (function form)	AlgebraicCombinatorics.Perm (Inversions1.lean)
Longest element w₀	AlgebraicCombinatorics.Perm (Inversions1.lean)
Reduced words	Equiv.Perm (this file)
Simple transposition products	Equiv.Perm (this file)
Coxeter-style arguments	Equiv.Perm (this file)
Lehmer codes (list form)	Equiv.Perm (this file)

Since the definitions are rfl-equal, you can freely use theorems from either file. The @[simp] lemmas inversions_eq_inv and length_eq_invCount help the simplifier rewrite between the two forms automatically.

Main results

• Equiv.Perm.length_inv - ℓ(σ⁻¹) = ℓ(σ)
• Equiv.Perm.length_mul_swap_right - Single swap lemma (right multiplication)
• Equiv.Perm.length_mul_swap_left - Single swap lemma (left multiplication)
• Equiv.Perm.length_mul_transposition - Length change for arbitrary transposition
• Equiv.Perm.exists_reduced_word - First reduced word theorem (existence)
• Equiv.Perm.length_le_word_length - First reduced word theorem (minimality)
• Equiv.Perm.length_mul_mod_two - ℓ(στ) ≡ ℓ(σ) + ℓ(τ) (mod 2)
• Equiv.Perm.length_mul_le - ℓ(στ) ≤ ℓ(σ) + ℓ(τ)
• Equiv.Perm.generated_by_simples - S_n is generated by simple transpositions
• Equiv.Perm.canonicalReducedWord_prod - The canonical reduced word produces σ
• Equiv.Perm.canonicalReducedWord_isReduced - The canonical reduced word is reduced

References

• Darij Grinberg, Notes on Algebraic Combinatorics, Chapter on Permutations
• [detnotes] Exercise 5.2 and related exercises

Tags

permutation, inversion, length, simple transposition, reduced word, Lehmer code

Simple transpositions

Design note: This definition is equivalent to AlgebraicCombinatorics.simpleTransposition from Basics.lean. The equivalence is proven by simpleTransposition_eq_canonical.

The canonical definition in Basics.lean is preferred for new code. This definition exists for historical reasons and uses a dite guard that simplifies proof automation within this file. Both definitions compute the same permutation: Equiv.swap k (k+1).

def Equiv.Perm.simpleTransposition {n : ℕ} (k : Fin (n - 1)) : Perm (Fin n)

The simple transposition s_k that swaps k and k+1 in Fin n. For k : Fin (n-1), this swaps positions k.castSucc and k.succ.

Note: This is equivalent to AlgebraicCombinatorics.simpleTransposition k from Basics.lean. See simpleTransposition_eq_canonical for the proof of equivalence.

Recommended: For new code, prefer AlgebraicCombinatorics.simpleTransposition (the canonical definition). Use this definition when working with reduced words and Coxeter-style arguments within this file.

Equations

• Equiv.Perm.simpleTransposition k = if h : n > 0 then Equiv.swap (Fin.castLE ⋯ k.castSucc) (Fin.castLE ⋯ k.succ) else 1

def Equiv.Perm.termS : Lean.ParserDescr

Notation: s k for the simple transposition swapping k and k+1.

Equations

• Equiv.Perm.termS = Lean.ParserDescr.node `Equiv.Perm.termS 1024 (Lean.ParserDescr.symbol "s")

def Equiv.Perm.posK {n : ℕ} (k : Fin (n - 1)) : Fin n

Helper: position k as an element of Fin n.

Equations

• Equiv.Perm.posK k = Fin.castLE ⋯ k.castSucc

def Equiv.Perm.posK1 {n : ℕ} (k : Fin (n - 1)) : Fin n

Helper: position k+1 as an element of Fin n.

Equations

• Equiv.Perm.posK1 k = Fin.castLE ⋯ k.succ

theorem Equiv.Perm.simpleTransposition_apply_posK {n : ℕ} (k : Fin (n - 1)) (hn : n > 0) : (simpleTransposition k) (posK k) = posK1 k

The simple transposition applies to position k.

theorem Equiv.Perm.simpleTransposition_apply_posK1 {n : ℕ} (k : Fin (n - 1)) (hn : n > 0) : (simpleTransposition k) (posK1 k) = posK k

The simple transposition applies to position k+1.

theorem Equiv.Perm.simpleTransposition_apply_of_ne {n : ℕ} (k : Fin (n - 1)) (i : Fin n) (hn : n > 0) (h1 : i ≠ posK k) (h2 : i ≠ posK1 k) : (simpleTransposition k) i = i

The simple transposition fixes positions other than k and k+1.

theorem Equiv.Perm.posK_lt_posK1 {n : ℕ} (k : Fin (n - 1)) : posK k < posK1 k

Position k is strictly less than position k+1.

Equivalence with Basics.lean simpleTransposition

theorem Equiv.Perm.simpleTransposition_eq_canonical {n : ℕ} (k : Fin (n - 1)) : simpleTransposition k = AlgebraicCombinatorics.simpleTransposition k

Equiv.Perm.simpleTransposition equals AlgebraicCombinatorics.simpleTransposition.

Both definitions represent the simple transposition s_k that swaps positions k and k+1. The definitions differ slightly in their construction:

• Equiv.Perm.simpleTransposition uses a dite to handle n = 0 case
• AlgebraicCombinatorics.simpleTransposition directly constructs the swap

But they produce the same permutation for all valid inputs.

Inversions and length

def Equiv.Perm.IsInversion {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Prop

An inversion of a permutation σ is a pair (i, j) with i < j and σ(i) > σ(j).

Equations

• σ.IsInversion i j = (i < j ∧ σ j < σ i)

def Equiv.Perm.inversions {n : ℕ} (σ : Perm (Fin n)) : Finset (Fin n × Fin n)

The set of inversions of a permutation.

Equations

• σ.inversions = {p : Fin n × Fin n | p.1 < p.2 ∧ σ p.2 < σ p.1}

def Equiv.Perm.length {n : ℕ} (σ : Perm (Fin n)) : ℕ

The length of a permutation is the number of its inversions.

Equations

• σ.length = σ.inversions.card

def Equiv.Perm.termℓ : Lean.ParserDescr

Notation for length.

Equations

• Equiv.Perm.termℓ = Lean.ParserDescr.node `Equiv.Perm.termℓ 1024 (Lean.ParserDescr.symbol "ℓ")

Equivalence with Inversions1 definitions

@[simp]

theorem Equiv.Perm.inversions_eq_inv {n : ℕ} (σ : Perm (Fin n)) : σ.inversions = AlgebraicCombinatorics.Perm.inv σ

Equiv.Perm.inversions equals AlgebraicCombinatorics.Perm.inv.

@[simp]

theorem Equiv.Perm.length_eq_invCount {n : ℕ} (σ : Perm (Fin n)) : σ.length = AlgebraicCombinatorics.Perm.invCount σ

Equiv.Perm.length equals AlgebraicCombinatorics.Perm.invCount.

Length of inverse (Proposition prop.perm.len.inv)

noncomputable def Equiv.Perm.inversionsBijection {n : ℕ} (σ : Perm (Fin n)) : ↥σ.inversions ≃ ↥σ⁻¹.inversions

The bijection between inversions of σ and inversions of σ⁻¹. If (i,j) is an inversion of σ (meaning i < j and σ(i) > σ(j)), then (σ(j), σ(i)) is an inversion of σ⁻¹.

Equations

• σ.inversionsBijection = Equiv.ofBijective (fun (p : ↥σ.inversions) => ⟨Equiv.Perm.inversionBijAux✝ σ ↑p, ⋯⟩) ⋯

theorem Equiv.Perm.length_inv {n : ℕ} (σ : Perm (Fin n)) : σ⁻¹.length = σ.length

Proposition prop.perm.len.inv: The length of a permutation equals the length of its inverse: ℓ(σ⁻¹) = ℓ(σ).

The proof establishes a bijection between inversions of σ and inversions of σ⁻¹: if (i,j) is an inversion of σ, then (σ(j), σ(i)) is an inversion of σ⁻¹.

Single swap lemma (Lemma lem.perm.len.ssl)

Helper definitions and lemmas for the single swap lemma

theorem Equiv.Perm.length_mul_swap_right {n : ℕ} (σ : Perm (Fin n)) (k : Fin (n - 1)) (h : n > 1) : (σ * simpleTransposition k).length = if σ (Fin.castLE ⋯ k.castSucc) < σ (Fin.castLE ⋯ k.succ) then σ.length + 1 else σ.length - 1

Lemma lem.perm.len.ssl (a): When multiplying a permutation σ on the right by a simple transposition s_k:

• If σ(k) < σ(k+1), then ℓ(σ·s_k) = ℓ(σ) + 1
• If σ(k) > σ(k+1), then ℓ(σ·s_k) = ℓ(σ) - 1

This lemma is fundamental for understanding how length changes under composition.

theorem Equiv.Perm.length_mul_swap_left {n : ℕ} (σ : Perm (Fin n)) (k : Fin (n - 1)) (h : n > 1) : (simpleTransposition k * σ).length = if σ⁻¹ (Fin.castLE ⋯ k.castSucc) < σ⁻¹ (Fin.castLE ⋯ k.succ) then σ.length + 1 else σ.length - 1

Lemma lem.perm.len.ssl (b): When multiplying a permutation σ on the left by a simple transposition s_k:

• If σ⁻¹(k) < σ⁻¹(k+1), then ℓ(s_k·σ) = ℓ(σ) + 1
• If σ⁻¹(k) > σ⁻¹(k+1), then ℓ(s_k·σ) = ℓ(σ) - 1

Note: σ⁻¹(i) is the position where i appears in the one-line notation of σ.

Length change for arbitrary transpositions (Proposition prop.perm.lisitij)

theorem Equiv.Perm.mem_inversions_iff {n : ℕ} (σ : Perm (Fin n)) (a b : Fin n) : (a, b) ∈ σ.inversions ↔ a < b ∧ σ b < σ a

def Equiv.Perm.setQ {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Finset (Fin n)

The set Q from Proposition prop.perm.lisitij: Q = {k ∈ {i+1, ..., j-1} | σ(i) > σ(k) > σ(j)} This counts elements between i and j whose images are strictly between σ(j) and σ(i).

Equations

• σ.setQ i j = {k : Fin n | i < k ∧ k < j ∧ σ j < σ k ∧ σ k < σ i}

def Equiv.Perm.setR {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Finset (Fin n)

The set R from Proposition prop.perm.lisitij: R = {k ∈ {i+1, ..., j-1} | σ(i) < σ(k) < σ(j)} This counts elements between i and j whose images are strictly between σ(i) and σ(j).

Equations

• σ.setR i j = {k : Fin n | i < k ∧ k < j ∧ σ i < σ k ∧ σ k < σ j}

def Equiv.Perm.setBelow {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Finset (Fin n)

The set of elements k between i and j with σ(k) ≤ σ(j).

Equations

• σ.setBelow i j = {k : Fin n | i < k ∧ k < j ∧ σ k ≤ σ j}

def Equiv.Perm.setAbove {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Finset (Fin n)

The set of elements k between i and j with σ(k) ≥ σ(i).

Equations

• σ.setAbove i j = {k : Fin n | i < k ∧ k < j ∧ σ i ≤ σ k}

theorem Equiv.Perm.setQ_swap_eq_setR {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : (σ * swap i j).setQ i j = σ.setR i j

Key symmetry: Q for σ * swap i j equals R for σ (when σ(i) < σ(j)). This allows us to reduce the case σ(i) < σ(j) to the case σ(i) > σ(j).

def Equiv.Perm.setA {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Finset (Fin n)

The set A: elements a < i with σ(j) < σ(a) < σ(i). These contribute to both lost and gained inversions (paired).

Equations

• σ.setA i j = {a : Fin n | a < i ∧ σ j < σ a ∧ σ a < σ i}

def Equiv.Perm.setB {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Finset (Fin n)

The set B: elements b > j with σ(j) < σ(b) < σ(i). These contribute to both lost and gained inversions (paired).

Equations

• σ.setB i j = {b : Fin n | j < b ∧ σ j < σ b ∧ σ b < σ i}

theorem Equiv.Perm.setA_setQ_disjoint {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : σ.setA i j ∩ σ.setQ i j = ∅

Sets A, Q, B are pairwise disjoint.

theorem Equiv.Perm.setA_setB_disjoint {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) (hij : i < j) : σ.setA i j ∩ σ.setB i j = ∅

theorem Equiv.Perm.setQ_setB_disjoint {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : σ.setQ i j ∩ σ.setB i j = ∅

theorem Equiv.Perm.ik_lost_for_k_in_Q {n : ℕ} (σ : Perm (Fin n)) (i j k : Fin n) (hk : k ∈ σ.setQ i j) : (i, k) ∈ σ.inversions \ (σ * swap i j).inversions

For k ∈ Q: (i, k) is a lost inversion.

theorem Equiv.Perm.kj_lost_for_k_in_Q {n : ℕ} (σ : Perm (Fin n)) (i j k : Fin n) (hk : k ∈ σ.setQ i j) : (k, j) ∈ σ.inversions \ (σ * swap i j).inversions

For k ∈ Q: (k, j) is a lost inversion.

theorem Equiv.Perm.ij_lost {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) (hij : i < j) (h : σ j < σ i) : (i, j) ∈ σ.inversions \ (σ * swap i j).inversions

(i, j) is a lost inversion when σ(j) < σ(i).

theorem Equiv.Perm.ai_gained_for_a_in_A {n : ℕ} (σ : Perm (Fin n)) (i j a : Fin n) (hij : i < j) (ha : a ∈ σ.setA i j) : (a, i) ∈ (σ * swap i j).inversions \ σ.inversions

For a ∈ A: (a, i) is a gained inversion.

theorem Equiv.Perm.jb_gained_for_b_in_B {n : ℕ} (σ : Perm (Fin n)) (i j b : Fin n) (hij : i < j) (hb : b ∈ σ.setB i j) : (j, b) ∈ (σ * swap i j).inversions \ σ.inversions

For b ∈ B: (j, b) is a gained inversion.

theorem Equiv.Perm.aj_lost_for_a_in_A {n : ℕ} (σ : Perm (Fin n)) (i j a : Fin n) (hij : i < j) (_h : σ j < σ i) (ha : a ∈ σ.setA i j) : (a, j) ∈ σ.inversions \ (σ * swap i j).inversions

For a ∈ A: (a, j) is a lost inversion.

theorem Equiv.Perm.ib_lost_for_b_in_B {n : ℕ} (σ : Perm (Fin n)) (i j b : Fin n) (hij : i < j) (_h : σ j < σ i) (hb : b ∈ σ.setB i j) : (i, b) ∈ σ.inversions \ (σ * swap i j).inversions

For b ∈ B: (i, b) is a lost inversion.

theorem Equiv.Perm.lost_inversion_complete {n : ℕ} (σ : Perm (Fin n)) (i j a b : Fin n) (hij : i < j) (h : σ j < σ i) (hmem : (a, b) ∈ σ.inversions \ (σ * swap i j).inversions) : a = i ∧ b = j ∨ a ∈ σ.setA i j ∧ b = j ∨ a = i ∧ b ∈ σ.setB i j ∨ a = i ∧ b ∈ σ.setQ i j ∨ a ∈ σ.setQ i j ∧ b = j

Completeness: every lost inversion is one of the five types.

theorem Equiv.Perm.gained_inversion_complete {n : ℕ} (σ : Perm (Fin n)) (i j a b : Fin n) (hij : i < j) (h : σ j < σ i) (hmem : (a, b) ∈ (σ * swap i j).inversions \ σ.inversions) : a ∈ σ.setA i j ∧ b = i ∨ a = j ∧ b ∈ σ.setB i j

Completeness: every gained inversion is one of the two types.

theorem Equiv.Perm.lost_minus_gained_eq {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) (hij : i < j) (h : σ j < σ i) : (σ.inversions \ (σ * swap i j).inversions).card = ((σ * swap i j).inversions \ σ.inversions).card + 2 * (σ.setQ i j).card + 1

Key counting lemma for prop.perm.lisitij: When σ(i) > σ(j), the number of lost inversions exceeds gained inversions by exactly 2|Q| + 1.

The proof proceeds by partitioning pairs (a, b) with a < b into categories:

1. The pair (i, j) itself: loses 1 inversion
2. Pairs (i, k) and (k, j) for k ∈ Q: each loses 1 inversion (total 2|Q|)
3. Pairs (a, i) and (a, j) for a < i: swap status, so net 0
4. Pairs (i, b) and (j, b) for b > j: swap status, so net 0
5. Pairs (i, k) and (k, j) for i < k < j, k ∉ Q: unchanged or swap, net 0
6. Other pairs: unchanged

Total: lost - gained = 2|Q| + 1

theorem Equiv.Perm.length_mul_transposition {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) (hij : i < j) : (σ * swap i j).length = if σ j < σ i then σ.length - 2 * (σ.setQ i j).card - 1 else σ.length + 2 * (σ.setR i j).card + 1

Proposition prop.perm.lisitij (b): The exact formula for length change:

• If σ(i) > σ(j): ℓ(σ·t_{i,j}) = ℓ(σ) - 2|Q| - 1
• If σ(i) < σ(j): ℓ(σ·t_{i,j}) = ℓ(σ) + 2|R| + 1

where Q and R are the sets of "intermediate" elements.

theorem Equiv.Perm.length_mul_transposition_compare {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) (hij : i < j) : (σ j < σ i → (σ * swap i j).length < σ.length) ∧ (σ i < σ j → σ.length < (σ * swap i j).length)

Proposition prop.perm.lisitij (a): For a transposition t_{i,j} with i < j:

• ℓ(σ·t_{i,j}) < ℓ(σ) if σ(i) > σ(j)
• ℓ(σ·t_{i,j}) > ℓ(σ) if σ(i) < σ(j)

The length decreases if (i,j) was an inversion, increases if it wasn't.

This follows immediately from part (b): when σ(i) > σ(j), the formula gives ℓ(σ·t_{i,j}) = ℓ(σ) - 2|Q| - 1 < ℓ(σ), and when σ(i) < σ(j), the formula gives ℓ(σ·t_{i,j}) = ℓ(σ) + 2|R| + 1 > ℓ(σ).

First reduced word theorem (Theorem thm.perm.len.redword1)

@[reducible, inline]

abbrev Equiv.Perm.Word (n : ℕ) : Type

A word is a list of indices representing simple transpositions.

Equations

• Equiv.Perm.Word n = List (Fin (n - 1))

def Equiv.Perm.wordProd {n : ℕ} (w : Word n) : Perm (Fin n)

The product of simple transpositions corresponding to a word.

Equations

• Equiv.Perm.wordProd w = (List.map Equiv.Perm.simpleTransposition w).prod

def Equiv.Perm.IsReduced {n : ℕ} (w : Word n) : Prop

A word is reduced if its length equals the length of the permutation it represents.

Equations

• Equiv.Perm.IsReduced w = (List.length w = (Equiv.Perm.wordProd w).length)

Helper lemmas for the first reduced word theorem

theorem Equiv.Perm.exists_reduced_word {n : ℕ} (σ : Perm (Fin n)) : ∃ (w : Word n), IsReduced w ∧ wordProd w = σ

Theorem thm.perm.len.redword1 (a): Every permutation can be written as a composition of ℓ(σ) simple transpositions.

This is proved by induction on ℓ(σ): if σ has an inversion at position k (meaning σ(k) > σ(k+1)), then ℓ(σ·s_k) = ℓ(σ) - 1, so by induction σ·s_k can be written with ℓ(σ) - 1 simples, and thus σ = (σ·s_k)·s_k can be written with ℓ(σ) simples.

theorem Equiv.Perm.length_le_word_length {n : ℕ} (w : Word n) : (wordProd w).length ≤ List.length w

Theorem thm.perm.len.redword1 (b): The length ℓ(σ) is the minimum number of simple transpositions needed to express σ.

This follows from the fact that multiplying by a simple transposition changes the length by at most 1.

theorem Equiv.Perm.length_eq_min_word_length {n : ℕ} (σ : Perm (Fin n)) : σ.length = List.length ⋯.choose

Combining parts (a) and (b): ℓ(σ) is exactly the minimum word length.

Corollaries (Corollary cor.perm.red.sigtau)

theorem Equiv.Perm.length_mul_mod_two {n : ℕ} (σ τ : Perm (Fin n)) : (σ * τ).length % 2 = (σ.length + τ.length) % 2

Corollary cor.perm.red.sigtau (a): The length of a product has the same parity as the sum of lengths: ℓ(στ) ≡ ℓ(σ) + ℓ(τ) (mod 2).

This follows from the fact that multiplying by a simple transposition always changes the length by exactly 1 (either +1 or -1).

theorem Equiv.Perm.length_mul_le {n : ℕ} (σ τ : Perm (Fin n)) : (σ * τ).length ≤ σ.length + τ.length

Corollary cor.perm.red.sigtau (b): The length of a product is at most the sum of lengths: ℓ(στ) ≤ ℓ(σ) + ℓ(τ).

This is the triangle inequality for the length function.

theorem Equiv.Perm.word_length_ge_and_parity {n : ℕ} (w : Word n) : List.length w ≥ (wordProd w).length ∧ List.length w % 2 = (wordProd w).length % 2

Corollary cor.perm.red.sigtau (c): For any word representing σ, the word length is at least ℓ(σ) and has the same parity as ℓ(σ).

Generation by simples (Corollary cor.perm.generated)

theorem Equiv.Perm.generated_by_simples {n : ℕ} : Subgroup.closure {σ : Perm (Fin n) | ∃ (k : Fin (n - 1)), σ = simpleTransposition k} = ⊤

Corollary cor.perm.generated: The symmetric group S_n is generated by the simple transpositions s_1, s_2, ..., s_{n-1}.

This is a direct consequence of the first reduced word theorem.

Lehmer code and reduced words (Remark rmk.perm.redword-lehmer and

Proposition prop.perm.redword-lehmer) 

@[reducible, inline]

abbrev Equiv.Perm.lehmerEntry {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ℕ

Alias for the canonical Lehmer entry definition from AlgebraicCombinatorics.Perm.lehmerEntry. Counts inversions (i, j) with first coordinate i.

Equations

• σ.lehmerEntry i = AlgebraicCombinatorics.Perm.lehmerEntry σ i

def Equiv.Perm.lehmerCode {n : ℕ} (σ : Perm (Fin n)) : List ℕ

The Lehmer code of a permutation as a list of Lehmer entries. This is the list representation of AlgebraicCombinatorics.Perm.lehmerCode.

Equations

• σ.lehmerCode = AlgebraicCombinatorics.Perm.lehmerCode_toList σ

def Equiv.Perm.inRotheDiagram {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Prop

A cell (i, j) is in the Rothe diagram of σ if σ(i) > j and σ⁻¹(j) > i. These are the cells that are not "hit" by the Lehmer lasers.

Equations

• σ.inRotheDiagram i j = (j < σ i ∧ i < σ⁻¹ j)

instance Equiv.Perm.instDecidableInRotheDiagram {n : ℕ} (σ : Perm (Fin n)) (i j : Fin n) : Decidable (σ.inRotheDiagram i j)

Equations

• σ.instDecidableInRotheDiagram i j = inferInstanceAs (Decidable (j < σ i ∧ i < σ⁻¹ j))

theorem Equiv.Perm.rotheDiagram_card_eq_length {n : ℕ} (σ : Perm (Fin n)) : {p : Fin n × Fin n | σ.inRotheDiagram p.1 p.2}.card = σ.length

The number of cells in the Rothe diagram equals the length.

Lehmer entry bounds

theorem Equiv.Perm.lehmerEntry_lt {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : σ.lehmerEntry i < n - ↑i

The Lehmer entry at position i is strictly less than n - i. This is because ℓ_i(σ) counts elements j > i such that σ(j) < σ(i), and there are only n - 1 - i elements greater than i.

theorem Equiv.Perm.sigma_zero_eq_lehmerEntry {n : ℕ} (σ : Perm (Fin n)) (hn : n > 0) : ↑(σ ⟨0, hn⟩) = σ.lehmerEntry ⟨0, hn⟩

Key characterization: σ(0) equals the Lehmer entry at position 0. This is because lehmerEntry σ 0 counts how many of σ(1), ..., σ(n-1) are less than σ(0), which equals σ(0) since σ is a bijection onto {0, ..., n-1}.

theorem Equiv.Perm.lehmerEntry_bound {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ↑i + σ.lehmerEntry i ≤ n - 1

Key bound: i + ℓ_i(σ) ≤ n - 1 for any position i. This ensures that the indices in the row word are valid.

Canonical reduced word construction (Proposition prop.perm.redword-lehmer)

def Equiv.Perm.rowWordIndex {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) (j : Fin (σ.lehmerEntry i)) : Fin (n - 1)

Helper function to create the index for the row word. For row i with Lehmer entry ℓ_i, the j-th element (0-indexed) of the word is the simple transposition s_{i+ℓ_i-1-j}.

Equations

• σ.rowWordIndex i j = ⟨↑i + σ.lehmerEntry i - 1 - ↑j, ⋯⟩

def Equiv.Perm.rowWord {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : Word n

The word for row i in the Lehmer-based reduced word construction. For row i with Lehmer entry ℓ_i, this produces [s_{i+ℓ_i-1}, s_{i+ℓ_i-2}, ..., s_i], which corresponds to the cycle (i+ℓ_i, i+ℓ_i-1, ..., i) = s_{i+ℓ_i-1} s_{i+ℓ_i-2} ... s_i.

This is the explicit formula from Proposition prop.perm.redword-lehmer: a_i = cyc_{i', i'-1, ..., i} where i' = i + ℓ_i(σ).

Equations

• σ.rowWord i = List.map (σ.rowWordIndex i) (List.finRange (σ.lehmerEntry i))

theorem Equiv.Perm.rowWord_length {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : List.length (σ.rowWord i) = σ.lehmerEntry i

The length of the row word equals the Lehmer entry.

theorem Equiv.Perm.lehmerEntry_add_le' {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ↑i + σ.lehmerEntry i ≤ n - 1

The Lehmer entry ℓ_i(σ) satisfies i + ℓ_i(σ) ≤ n - 1. This is because ℓ_i(σ) counts j with i < j, and there are at most n - 1 - i such j.

theorem Equiv.Perm.sum_lehmerEntry_eq_length {n : ℕ} (σ : Perm (Fin n)) : ∑ i : Fin n, σ.lehmerEntry i = σ.length

The sum of Lehmer entries equals the length.

theorem Equiv.Perm.lehmerBlock_idx_bound {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) (k : ℕ) (hk : k < σ.lehmerEntry i) : ↑i + σ.lehmerEntry i - 1 - k < n - 1

Helper: given k < ℓ_i(σ), the index i + ℓ_i(σ) - 1 - k is < n - 1. This ensures that all indices in the Lehmer block are valid.

def Equiv.Perm.lehmerBlock {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : Word n

The block a_i for row i: [s_{i'-1}, s_{i'-2}, ..., s_i] where i' = i + ℓ_i(σ). This is a descending sequence of simple transpositions. If ℓ_i(σ) = 0, this is the empty list.

The product of this block is the cycle (i', i'-1, ..., i) which moves element at position i to position i'.

Equations

• σ.lehmerBlock i = List.map (fun (k : Fin (σ.lehmerEntry i)) => ⟨↑i + σ.lehmerEntry i - 1 - ↑k, ⋯⟩) (List.finRange (σ.lehmerEntry i))

theorem Equiv.Perm.lehmerBlock_length {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : List.length (σ.lehmerBlock i) = σ.lehmerEntry i

The length of a Lehmer block equals the Lehmer entry.

Helper lemmas for wordProd of descending words

Key characterization lemmas for the canonical reduced word proof

def Equiv.Perm.smallerBefore {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ℕ

Number of j < i with σ(j) < σ(i). This counts positions before i with smaller values.

Equations

• σ.smallerBefore i = {j : Fin n | j < i ∧ σ j < σ i}.card

def Equiv.Perm.largerBefore {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ℕ

Number of j < i with σ(j) > σ(i). This counts inversions with i as second element.

Equations

• σ.largerBefore i = {j : Fin n | j < i ∧ σ j > σ i}.card

theorem Equiv.Perm.smallerBefore_add_largerBefore {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : σ.smallerBefore i + σ.largerBefore i = ↑i

Key identity: smallerBefore + largerBefore = i. The elements j < i are partitioned into those with σ(j) < σ(i) and those with σ(j) > σ(i).

theorem Equiv.Perm.largerBefore_eq {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : σ.largerBefore i = ↑i - σ.smallerBefore i

Corollary: largerBefore = i - smallerBefore.

theorem Equiv.Perm.sigma_eq_smallerBefore_add_lehmerEntry {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ↑(σ i) = σ.smallerBefore i + σ.lehmerEntry i

Key characterization: σ(i) = smallerBefore(σ, i) + lehmerEntry(σ, i). This is the fundamental formula connecting the permutation value to the Lehmer code.

theorem Equiv.Perm.final_position_formula {n : ℕ} (σ : Perm (Fin n)) (p : Fin n) : ↑p + σ.lehmerEntry p - σ.largerBefore p = ↑(σ p)

Key formula: The final position after applying all blocks is σ(p). This follows from p + lehmerEntry σ p - largerBefore σ p = σ(p).

theorem Equiv.Perm.lehmerEntry_range_upper {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) : ↑i + σ.lehmerEntry i = ↑(σ i) + σ.largerBefore i

Key formula: The upper bound of block i's range equals σ(i) + largerBefore(σ, i).

theorem Equiv.Perm.lehmerEntry_diff_iff_inversion {n : ℕ} (σ : Perm (Fin n)) (i : Fin n) (hi : ↑i + 1 < n) : have i' := ⟨↑i + 1, hi⟩; σ.lehmerEntry i ≥ σ.lehmerEntry i' + 1 ↔ σ i > σ i'

Key characterization: lehmerEntry(σ, i) ≥ lehmerEntry(σ, i+1) + 1 iff σ(i) > σ(i+1). This is crucial for determining when block i shifts a position.

theorem Equiv.Perm.eq_of_inversions_eq {n : ℕ} (σ τ : Perm (Fin n)) (h : ∀ (i j : Fin n), i < j → (σ j < σ i ↔ τ j < τ i)) : σ = τ

Two permutations with the same inversions are equal. This is because the inversions determine the relative order of all values, which uniquely determines the permutation.

def Equiv.Perm.canonicalReducedWord {n : ℕ} (σ : Perm (Fin n)) : Word n

Proposition prop.perm.redword-lehmer: The canonical reduced word for σ. For each i, define a_i = cyc_{i', i'-1, ..., i} = s_{i'-1} s_{i'-2} ... s_i where i' = i + ℓ_i(σ). Then σ = a_1 a_2 ... a_n.

This gives an explicit algorithm to construct a reduced word from the Lehmer code. The word is constructed by concatenating the Lehmer blocks for each position i = 0, 1, ..., n-1.

Equations

• σ.canonicalReducedWord = (List.map σ.lehmerBlock (List.finRange n)).flatten

theorem Equiv.Perm.canonicalReducedWord_length {n : ℕ} (σ : Perm (Fin n)) : List.length σ.canonicalReducedWord = σ.length

The length of the canonical reduced word equals the length of σ. This follows from the fact that each row word has length equal to the corresponding Lehmer entry, and the sum of Lehmer entries equals ℓ(σ).

theorem Equiv.Perm.canonicalReducedWord_prod {n : ℕ} (σ : Perm (Fin n)) : wordProd σ.canonicalReducedWord = σ

The canonical reduced word produces σ. This is the main content of Proposition prop.perm.redword-lehmer.

The proof uses the key insight that each lehmerBlock σ i produces a cycle that moves position i to position i + lehmerEntry σ i, while shifting intermediate positions down by 1. When composed in order from i = 0 to i = n-1, these cycles reconstruct σ.

Proof outline: For each position p, we track where it ends up after applying all blocks. The blocks are applied in the order: B_{n-1} first, then B_{n-2}, ..., then B_0.

1. Blocks n-1, ..., p+1 fix p (since p < i for all these, p is outside their ranges).
2. Block p maps p to p + lehmerEntry σ p (by wordProd_lehmerBlock_at_i).
3. For each j < p, block j shifts the current position down by 1 iff σ(j) > σ(p). This is because the condition "j < q ≤ j + lehmerEntry σ j" holds iff σ(j) > σ(p), using careful counting of elements in the Lehmer code.
4. The total number of shifts by blocks 0, ..., p-1 equals largerBefore σ p.
5. Final position = p + lehmerEntry σ p - largerBefore σ p = smallerBefore σ p + lehmerEntry σ p (since p = smallerBefore + largerBefore) = σ(p) (by sigma_eq_smallerBefore_add_lehmerEntry).

The detailed combinatorial argument is in Exercise 5.21 of detnotes.

theorem Equiv.Perm.canonicalReducedWord_isReduced {n : ℕ} (σ : Perm (Fin n)) : IsReduced σ.canonicalReducedWord

The canonical reduced word is indeed reduced.