Inversions and length

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

An inversion of a permutation σ ∈ S_n is a pair (i, j) of elements of [n] such that i < j and σ(i) > σ(j).

See Definition 1.3.1 (def.perm.invs) in the source.

Equations

• AlgebraicCombinatorics.Perm.inv σ = {p : Fin n × Fin n | p.1 < p.2 ∧ σ p.1 > σ p.2}

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

The length (or Coxeter length) of a permutation σ is the number of inversions of σ. This is denoted ℓ(σ) in the source.

See Definition 1.3.1 (def.perm.invs) part (b) in the source.

Equations

• AlgebraicCombinatorics.Perm.invCount σ = (AlgebraicCombinatorics.Perm.inv σ).card

theorem AlgebraicCombinatorics.Perm.invCount_le_choose {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount σ ≤ n.choose 2

For any σ ∈ S_n, we have ℓ(σ) ∈ {0, 1, ..., n choose 2}.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (a) in the source.

theorem AlgebraicCombinatorics.Perm.invCount_eq_zero_iff {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount σ = 0 ↔ σ = 1

The only permutation σ ∈ S_n with ℓ(σ) = 0 is the identity map.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (b) in the source.

@[simp]

theorem AlgebraicCombinatorics.Perm.inv_one {n : ℕ} : inv 1 = ∅

The identity permutation has no inversions.

The identity preserves order, so there cannot be a pair (i, j) with i < j and 1(i) > 1(j).

@[simp]

theorem AlgebraicCombinatorics.Perm.invCount_one {n : ℕ} : invCount 1 = 0

The identity permutation has length 0.

This follows directly from inv_one: the identity has no inversions.

theorem AlgebraicCombinatorics.Perm.invCount_inv {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount σ⁻¹ = invCount σ

The inversion count is preserved under taking inverses.

For a permutation σ, the pair (i, j) with i < j is an inversion of σ iff σ(i) > σ(j). For σ⁻¹, the pair (a, b) with a < b is an inversion iff σ⁻¹(a) > σ⁻¹(b). The map (a, b) ↦ (σ⁻¹(b), σ⁻¹(a)) gives a bijection between inversions of σ⁻¹ and σ.

theorem AlgebraicCombinatorics.Perm.invCount_mul_le {n : ℕ} (σ τ : Equiv.Perm (Fin n)) : invCount (σ * τ) ≤ invCount σ + invCount τ

The inversion count of a product is bounded by the sum of inversion counts. This is not an equality in general (the triangle inequality for inversions).

theorem AlgebraicCombinatorics.Perm.card_invCount_eq_zero {n : ℕ} : {σ : Equiv.Perm (Fin n) | invCount σ = 0}.card = 1

The number of permutations σ ∈ S_n with ℓ(σ) = 0 is 1.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (b) in the source.

def AlgebraicCombinatorics.Perm.longestElement (n : ℕ) : Equiv.Perm (Fin n)

The longest element w₀ ∈ S_n is the permutation with OLN n(n-1)(n-2)...21, i.e., the reversal permutation.

Note: This is equivalent to Fin.revPerm from Mathlib. See longestElement_eq_revPerm.

Equations

• AlgebraicCombinatorics.Perm.longestElement n = { toFun := fun (i : Fin n) => ⟨n - 1 - ↑i, ⋯⟩, invFun := fun (i : Fin n) => ⟨n - 1 - ↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem AlgebraicCombinatorics.Perm.longestElement_eq_revPerm {n : ℕ} : longestElement n = Fin.revPerm

The longest element is equal to Fin.revPerm from Mathlib.

theorem AlgebraicCombinatorics.Perm.inv_longestElement {n : ℕ} : inv (longestElement n) = {p : Fin n × Fin n | p.1 < p.2}

The set of inversions of the longest element w₀ is exactly the set of all pairs (i, j) with i < j. That is, every pair is an inversion.

@[simp]

theorem AlgebraicCombinatorics.Perm.invCount_longestElement {n : ℕ} : invCount (longestElement n) = n.choose 2

The longest element w₀ ∈ S_n has length n choose 2, the maximum possible length.

This is because every pair (i, j) with i < j is an inversion of w₀, since w₀ reverses the order of elements.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (c) in the source.

theorem AlgebraicCombinatorics.Perm.invCount_eq_choose_iff {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount σ = n.choose 2 ↔ σ = longestElement n

The only permutation σ ∈ S_n with ℓ(σ) = n choose 2 is w₀.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (c) in the source.

theorem AlgebraicCombinatorics.Perm.card_invCount_eq_choose {n : ℕ} : {σ : Equiv.Perm (Fin n) | invCount σ = n.choose 2}.card = 1

The number of permutations σ ∈ S_n with ℓ(σ) = n choose 2 is 1.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (c) in the source.

theorem AlgebraicCombinatorics.Perm.card_invCount_eq_one {n : ℕ} (hn : 1 ≤ n) : {σ : Equiv.Perm (Fin n) | invCount σ = 1}.card = n - 1

If n ≥ 1, then the number of permutations σ ∈ S_n with ℓ(σ) = 1 is n - 1. These are precisely the simple transpositions s_i.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (d) in the source.

theorem AlgebraicCombinatorics.Perm.card_invCount_eq_two {n : ℕ} (hn : 2 ≤ n) : {σ : Equiv.Perm (Fin n) | invCount σ = 2}.card = (n - 2) * (n + 1) / 2

Helper lemmas for symmetry of length distribution

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

The non-inversions of a permutation σ: pairs (i, j) with i < j and σ i < σ j.

This is the complement of inv σ within the set of ordered pairs. The non-inversions are exactly the pairs where σ preserves the order.

Equations

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

theorem AlgebraicCombinatorics.Perm.invCount_longestElement_mul {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount (longestElement n * σ) = (nonInv σ).card

The inversion count of w₀ * σ equals the number of non-inversions of σ.

This expresses a fundamental duality: multiplying by the longest element w₀ swaps inversions and non-inversions.

@[simp]

theorem AlgebraicCombinatorics.Perm.invCount_longestElement_mul' {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount (longestElement n * σ) = n.choose 2 - invCount σ

The inversion count of w₀ * σ equals n choose 2 minus the inversion count of σ.

This shows that multiplication by the longest element w₀ "complements" the length: if σ has k inversions, then w₀ * σ has (n choose 2) - k inversions.

@[simp]

theorem AlgebraicCombinatorics.Perm.longestElement_mul_self {n : ℕ} : longestElement n * longestElement n = 1

The longest element w₀ is an involution: w₀ * w₀ = 1.

This follows from the fact that w₀ = Fin.revPerm and revPerm is an involution.

@[simp]

theorem AlgebraicCombinatorics.Perm.longestElement_inv {n : ℕ} : (longestElement n)⁻¹ = longestElement n

The inverse of the longest element is itself: w₀⁻¹ = w₀.

This follows from longestElement_mul_self.

@[simp]

theorem AlgebraicCombinatorics.Perm.longestElement_apply {n : ℕ} (i : Fin n) : (longestElement n) i = ⟨n - 1 - ↑i, ⋯⟩

Explicit computation of the longest element: w₀(i) = n - 1 - i.

This shows that w₀ reverses the order of elements.

theorem AlgebraicCombinatorics.Perm.card_invCount_symm {n : ℕ} (k : ℤ) : {σ : Equiv.Perm (Fin n) | ↑(invCount σ) = k}.card = {σ : Equiv.Perm (Fin n) | ↑(invCount σ) = ↑(n.choose 2) - k}.card

The number of σ ∈ S_n with ℓ(σ) = k equals the number with ℓ(σ) = (n choose 2) - k. This is the symmetry of the length distribution.

See Proposition 1.3.3 (prop.perm.lengths-k-small-k) part (f) in the source.

Lehmer codes

The notation [m]_0 for {0, 1, ..., m}

See Definition 1.3.5 (def.perm.lehmer1) part (b) in the source.

def AlgebraicCombinatorics.Perm.Iic0 (m : ℤ) : Set ℕ

For each m ∈ ℤ, we let [m]_0 denote the set {0, 1, ..., m}. This is an empty set when m < 0.

See Definition 1.3.5 (def.perm.lehmer1) part (b) in the source.

Equations

• AlgebraicCombinatorics.Perm.Iic0 m = {n : ℕ | ↑n ≤ m}

theorem AlgebraicCombinatorics.Perm.Iic0_eq_empty_of_neg {m : ℤ} (hm : m < 0) : Iic0 m = ∅

[m]_0 is empty when m < 0

theorem AlgebraicCombinatorics.Perm.Iic0_eq_Iic_of_nonneg {m : ℤ} (hm : 0 ≤ m) : Iic0 m = Set.Iic m.toNat

[m]_0 = {0, 1, ..., m} when m ≥ 0

theorem AlgebraicCombinatorics.Perm.card_Iic0_of_nonneg {m : ℤ} (hm : 0 ≤ m) : (Iic0 m).ncard = m.toNat + 1

The cardinality of [m]_0 is m + 1 when m ≥ 0

def AlgebraicCombinatorics.Perm.Iic0Nat (m : ℕ) : Set ℕ

[m]_0 for natural numbers is just {0, 1, ..., m}

Equations

• AlgebraicCombinatorics.Perm.Iic0Nat m = Set.Iic m

theorem AlgebraicCombinatorics.Perm.Iic0Nat_eq_Iic0 (m : ℕ) : Iic0Nat m = Iic0 ↑m

[m]_0 for natural numbers equals the integer version

theorem AlgebraicCombinatorics.Perm.card_Iic0Nat (m : ℕ) : (Iic0Nat m).ncard = m + 1

The cardinality of [m]_0 for natural numbers is m + 1

theorem AlgebraicCombinatorics.Perm.mem_Iic0_iff {m : ℤ} {n : ℕ} : n ∈ Iic0 m ↔ ↑n ≤ m

Membership characterization for [m]_0

theorem AlgebraicCombinatorics.Perm.mem_Iic0Nat_iff {m n : ℕ} : n ∈ Iic0Nat m ↔ n ≤ m

Membership characterization for [m]_0 with natural numbers

Lehmer entry and Lehmer code definitions

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

For σ ∈ S_n and i ∈ [n], we define ℓ_i(σ) as the number of j > i such that σ(i) > σ(j). This counts how many elements to the right of position i are smaller than σ(i).

This is the canonical definition of Lehmer entry used throughout the project. The equivalent formulation i < j ∧ σ j < σ i is provided by lehmerEntry_eq_filter_lt.

See Definition 1.3.5 (def.perm.lehmer1) part (a) in the source.

Equations

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

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

The Lehmer code of σ ∈ S_n is the n-tuple (ℓ_1(σ), ℓ_2(σ), ..., ℓ_n(σ)).

This is the canonical definition using a function type Fin n → ℕ. For the list representation, use lehmerCode_toList.

See Definition 1.3.5 (def.perm.lehmer1) part (e) in the source.

Equations

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

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

Each entry of a Lehmer code satisfies the bound ℓ_i(σ) ≤ n - i - 1. This shows the Lehmer code map is well-defined into H_n.

See Definition 1.3.5 (def.perm.lehmer1) part (d) in the source.

theorem AlgebraicCombinatorics.Perm.invCount_eq_sum_lehmerCode {n : ℕ} (σ : Equiv.Perm (Fin n)) : invCount σ = ∑ i : Fin n, lehmerEntry σ i

The length of σ equals the sum of its Lehmer code entries: ℓ(σ) = ℓ_1(σ) + ℓ_2(σ) + ... + ℓ_n(σ).

See Proposition 1.3.6 (prop.perm.lehmer.l) in the source.

theorem AlgebraicCombinatorics.Perm.lehmerEntry_eq_filter_lt {n : ℕ} (σ : Equiv.Perm (Fin n)) (i : Fin n) : lehmerEntry σ i = {j : Fin n | i < j ∧ σ j < σ i}.card

Alternative characterization of lehmerEntry using σ j < σ i instead of σ i > σ j. These are equivalent conditions.

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

The Lehmer code as a list representation. This converts the function representation Fin n → ℕ to a List ℕ.

Equations

• AlgebraicCombinatorics.Perm.lehmerCode_toList σ = List.map (AlgebraicCombinatorics.Perm.lehmerCode σ) (List.finRange n)

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

The list representation of the Lehmer code has length n.

theorem AlgebraicCombinatorics.Perm.lehmerCode_toList_get {n : ℕ} (σ : Equiv.Perm (Fin n)) (i : Fin n) : (lehmerCode_toList σ).get ⟨↑i, ⋯⟩ = lehmerCode σ i

The i-th element of the list representation equals the function value.

The set of Lehmer codes

def AlgebraicCombinatorics.lehmerCodeSet (n : ℕ) : Set (Fin n → ℕ)

The set H_n of valid Lehmer codes. An n-tuple (j_1, ..., j_n) is in H_n if and only if j_i ≤ n - i - 1 for each i ∈ [n].

This is [n-1]_0 × [n-2]_0 × ... × [0]_0.

See Definition 1.3.5 (def.perm.lehmer1) part (c) in the source.

Equations

• AlgebraicCombinatorics.lehmerCodeSet n = {f : Fin n → ℕ | ∀ (i : Fin n), f i ≤ n - 1 - ↑i}

theorem AlgebraicCombinatorics.Perm.lehmerCode_mem_lehmerCodeSet {n : ℕ} (σ : Equiv.Perm (Fin n)) : lehmerCode σ ∈ lehmerCodeSet n

The Lehmer code of any permutation lies in H_n.

theorem AlgebraicCombinatorics.card_lehmerCodeSet (n : ℕ) : (lehmerCodeSet n).ncard = n.factorial

The set H_n has size n!.

See Definition 1.3.5 (def.perm.lehmer1) part (c) in the source.

theorem AlgebraicCombinatorics.Perm.lehmerCode_injective (n : ℕ) : Function.Injective fun (σ : Equiv.Perm (Fin n)) => lehmerCode σ

The Lehmer code map L : S_n → H_n is injective.

See Theorem 1.3.7 (thm.perm.lehmer.bij) in the source.

theorem AlgebraicCombinatorics.Perm.lehmerCode_bijective (n : ℕ) : Function.Bijective fun (σ : Equiv.Perm (Fin n)) => ⟨lehmerCode σ, ⋯⟩

The Lehmer code map L : S_n → H_n is a bijection.

See Theorem 1.3.7 (thm.perm.lehmer.bij) in the source.

Lexicographic order

def AlgebraicCombinatorics.lexLt {n : ℕ} (a b : Fin n → ℤ) : Prop

Lexicographic order on n-tuples of integers. We say (a_1, ..., a_n) <_lex (b_1, ..., b_n) if there exists k ∈ [n] such that a_k ≠ b_k and the smallest such k satisfies a_k < b_k.

Note: This is essentially Pi.Lex (· < ·) (· < ·) from Mathlib, specialized to Fin n → ℤ. We define it directly here to match the source presentation.

See Definition 1.3.8 (def.perm.lehmer.lex-ord) in the source.

Equations

• AlgebraicCombinatorics.lexLt a b = ∃ (k : Fin n), (∀ i < k, a i = b i) ∧ a k < b k

theorem AlgebraicCombinatorics.lexLt_eq_piLex {n : ℕ} (a b : Fin n → ℤ) : lexLt a b ↔ Pi.Lex (fun (x1 x2 : Fin n) => x1 < x2) (fun {x : Fin n} (x1 x2 : ℤ) => x1 < x2) a b

The lexicographic order lexLt is equivalent to Mathlib's Pi.Lex (· < ·) (· < ·).

This shows that our definition matches the standard Mathlib definition for lexicographic order on pi types.

theorem AlgebraicCombinatorics.lexLt_irrefl {n : ℕ} (a : Fin n → ℤ) : ¬lexLt a a

The lexicographic order is irreflexive: no tuple is lexicographically smaller than itself.

This is part of Definition 1.3.8 (def.perm.lehmer.lex-ord): <_lex is a strict order.

theorem AlgebraicCombinatorics.lexLt_trans {n : ℕ} {a b c : Fin n → ℤ} (hab : lexLt a b) (hbc : lexLt b c) : lexLt a c

The lexicographic order is transitive.

This is part of Definition 1.3.8 (def.perm.lehmer.lex-ord): <_lex is a strict order.

theorem AlgebraicCombinatorics.lexLt_asymm {n : ℕ} {a b : Fin n → ℤ} (hab : lexLt a b) : ¬lexLt b a

The lexicographic order is asymmetric: if a <_lex b, then not b <_lex a.

This is part of Definition 1.3.8 (def.perm.lehmer.lex-ord): <_lex is a strict order.

theorem AlgebraicCombinatorics.lexLt_trichotomous {n : ℕ} (a b : Fin n → ℤ) (hab : a ≠ b) : lexLt a b ∨ lexLt b a

If a and b are two distinct n-tuples of integers, then either a <_lex b or b <_lex a.

See Proposition 1.3.9 (prop.perm.lehmer.lex-ord.total) in the source.

theorem AlgebraicCombinatorics.lexLt_strictTotalOrder {n : ℕ} (a b : Fin n → ℤ) : a = b ∧ ¬lexLt a b ∧ ¬lexLt b a ∨ a ≠ b ∧ lexLt a b ∧ ¬lexLt b a ∨ a ≠ b ∧ ¬lexLt a b ∧ lexLt b a

The lexicographic order is a strict total order on n-tuples of integers: for any a, b, exactly one of a = b, lexLt a b, or lexLt b a holds.

This completes the proof that <_lex defines a strict total order on ℤⁿ. See Definition 1.3.8 (def.perm.lehmer.lex-ord) in the source.

theorem AlgebraicCombinatorics.Perm.lehmerEntry_eq_card_filter {n : ℕ} (σ : Equiv.Perm (Fin n)) (i : Fin n) : lehmerEntry σ i = {v : Fin n | v < σ i ∧ v ∉ Finset.image ⇑σ {x : Fin n | x < i}}.card

Alternative characterization of Lehmer entry: ℓ_i(σ) = |{v < σ(i) : v ∉ σ({0, ..., i-1})}|

This is the number of elements smaller than σ(i) that haven't been "used" yet (i.e., are not in the image of positions before i).

See the proof of Theorem 1.3.7 (thm.perm.lehmer.bij) in the source.

theorem AlgebraicCombinatorics.Perm.lehmerCode_preserves_lexLt {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (h : lexLt (fun (i : Fin n) => ↑↑(σ i)) fun (i : Fin n) => ↑↑(τ i)) : lexLt (fun (i : Fin n) => ↑(lehmerEntry σ i)) fun (i : Fin n) => ↑(lehmerEntry τ i)

If σ, τ ∈ S_n satisfy (σ(1), ..., σ(n)) <_lex (τ(1), ..., τ(n)), then L(σ) <_lex L(τ).

Proposition prop.perm.lehmer.lex from the source.

The proof uses the alternative characterization of Lehmer entries: ℓ_i(σ) counts elements smaller than σ(i) that are not in the image of positions before i. If σ and τ agree on positions below k and σ(k) < τ(k), then:

• For i < k: ℓ_i(σ) = ℓ_i(τ) (since the images below i are equal and σ(i) = τ(i))
• At k: ℓ_k(σ) < ℓ_k(τ) (since σ(k) is available for τ but not for σ)

Generating function for length

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

Helper lemma: Lehmer code entry is strictly less than n - i.

theorem AlgebraicCombinatorics.length_generating_function (n x : ℕ) : ∑ σ : Equiv.Perm (Fin n), x ^ Perm.invCount σ = ∏ i ∈ Finset.range n, ∑ j ∈ Finset.range (i + 1), x ^ j

The generating function for permutation lengths: ∑_{σ ∈ S_n} x^{ℓ(σ)} = [n]_x!

This equals the product (1+x)(1+x+x²)...(1+x+...+x^{n-1}).

See Proposition 1.3.4 (prop.perm.length.gf) in the source.