Basic definitions, transpositions, cycles and involutions

This file formalizes the basic definitions of permutations, transpositions, cycles, and involutions from the Algebraic Combinatorics textbook.

Main definitions

• Equiv.Perm: The type of permutations of a set (from Mathlib)
• Equiv.swap: The transposition swapping two elements (from Mathlib)
• cyc: The k-cycle cyc_{i₁, i₂, ..., iₖ} that cyclically permutes elements (def.perm.cycs)
• Equiv.Perm.IsCycle: Predicate for a permutation being a cycle (from Mathlib)
• simpleTransposition: The simple transposition swapping i and i+1
• IsInvolution: Predicate for a permutation being an involution

Main results

• symmetricGroup_card: The symmetric group has n! elements
• symmetricGroup_conj_iso: Bijections induce isomorphisms of symmetric groups
• transposition_apply_left: t_{i,j}(i) = j (def.perm.tij)
• transposition_apply_right: t_{i,j}(j) = i (def.perm.tij)
• transposition_apply_of_ne_of_ne: t_{i,j}(x) = x for x ≠ i, j (def.perm.tij)
• transposition_symm: Transpositions are symmetric: t_{i,j} = t_{j,i}
• transposition_sq_eq_one: Transpositions are involutions: t_{i,j}² = id
• num_transpositions: The number of transpositions in S_X is C(|X|, 2)
• simpleTransposition_eq_transposition: s_i = t_{i,i+1} (def.perm.si)
• simpleTransposition_apply_self: s_i(i) = i+1 (def.perm.si)
• simpleTransposition_apply_succ: s_i(i+1) = i (def.perm.si)
• simpleTransposition_apply_of_ne: s_i(k) = k for k ≠ i, i+1 (def.perm.si)
• simpleTransposition_support: support of s_i is {i, i+1} (def.perm.si)
• simpleTransposition_isSwap: s_i is a swap (def.perm.si)
• simpleTransposition_isCycle: s_i is a 2-cycle (def.perm.si)
• simpleTransposition_sq_eq_one: Simple transpositions satisfy s_i² = id
• simpleTransposition_comm: Simple transpositions commute when |i-j| > 1
• simpleTransposition_braid: The braid relation s_i s_{i+1} s_i = s_{i+1} s_i s_{i+1}
• cyc_pair: 2-cycles are exactly transpositions: cyc [i, j] = swap i j
• cyc_rotate: Cyclic rotation doesn't change the cycle
• cyc_apply_getElem: The cycle sends l[j] to l[(j+1) % l.length]
• cycle_eq_transposition: 2-cycles are exactly transpositions
• num_kCycles_formula: The number of k-cycles in S_n is C(n,k) * (k-1)!

References

See AlgebraicCombinatorics/tex/Permutations/Basics.tex for the LaTeX source.

Design note: simpleTransposition duplication

The simpleTransposition function is defined in this file (AlgebraicCombinatorics.simpleTransposition) and also in Inversions2.lean (Equiv.Perm.simpleTransposition). Both definitions produce the same permutation (proven by Equiv.Perm.simpleTransposition_eq_canonical).

Which to use:

• Use AlgebraicCombinatorics.simpleTransposition (this file) for basic properties of simple transpositions as swaps/cycles
• Use Equiv.Perm.simpleTransposition (Inversions2.lean) when working with reduced words, length functions, and Coxeter-style arguments

Tags

permutation, symmetric group, transposition, cycle, involution

Basic definitions (def.perm.perm)

This section formalizes Definition def.perm.perm from the textbook:

(a) A permutation of X means a bijection from X to X. In Mathlib, this is Equiv.Perm X := X ≃ X.

(b) The set of all permutations of X is a group under composition, called the symmetric group of X, denoted S_X. Its neutral element is id_X, and its size is |X|!. In Mathlib, Equiv.Perm X has a Group instance automatically.

(c) We write αβ for composition α ∘ β when α, β ∈ S_X. This sends each x ∈ X to α(β(x)). In Mathlib, (α * β) x = α (β x).

(d) If α ∈ S_X and i ∈ ℤ, then α^i denotes the i-th power of α in the group S_X.

• α^i = α ∘ α ∘ ⋯ ∘ α (i times) if i ≥ 0
• α^0 = id_X
• α^(-1) is the inverse of α

@[reducible, inline]

abbrev AlgebraicCombinatorics.Permutation (X : Type u_1) : Type u_1

A permutation of a type X is a bijection from X to itself. (def.perm.perm (a))

In Mathlib, this is Equiv.Perm X := X ≃ X, i.e., the type of equivalences from X to X.

Equations

• AlgebraicCombinatorics.Permutation X = Equiv.Perm X

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricGroup (X : Type u_1) : Type u_1

The symmetric group of a type X is the group of all permutations of X. (def.perm.perm (b))

In Mathlib, this is Equiv.Perm X with its natural Group instance.

Equations

• AlgebraicCombinatorics.SymmetricGroup X = Equiv.Perm X

The n-th symmetric group (def.perm.Sn-iven)

In the textbook, [n] denotes the set {1, 2, ..., n}, which is an n-element set for n ≥ 0 and empty for n ≤ 0.

In Lean/Mathlib, we use Fin n = {0, 1, ..., n-1} instead, which is also an n-element set. This is a standard convention difference (0-indexed vs 1-indexed), but the symmetric groups are isomorphic since both are n-element sets.

The symmetric group S_[n] (denoted S_n) is the group of all permutations of [n]. Its size is n! when n ≥ 0.

@[reducible, inline]

abbrev AlgebraicCombinatorics.bracketN (n : ℕ) : Type

The set [n] from the textbook is represented by Fin n in Lean.

In the textbook (def.perm.Sn-iven), [n] denotes {1, 2, ..., n}. In Lean, Fin n represents {0, 1, ..., n-1}.

Both are n-element sets for n ≥ 0, so their symmetric groups are isomorphic. We use Fin n as it is the standard representation in Mathlib.

Equations

• AlgebraicCombinatorics.bracketN n = Fin n

@[reducible, inline]

abbrev AlgebraicCombinatorics.Sn (n : ℕ) : Type

The n-th symmetric group S_n is the group of permutations of [n]. (def.perm.Sn-iven)

In the textbook, S_n is defined as S_[n], the symmetric group of [n] = {1, 2, ..., n}. In Lean, we represent this as Equiv.Perm (Fin n), the group of permutations of Fin n = {0, 1, ..., n-1}.

The size of S_n is n! (see sn_card).

Equations

• AlgebraicCombinatorics.Sn n = Equiv.Perm (Fin n)

theorem AlgebraicCombinatorics.symmetricGroup_card (X : Type u_1) [Fintype X] [DecidableEq X] : Fintype.card (Equiv.Perm X) = (Fintype.card X).factorial

The symmetric group of a finite type has |X|! elements. (def.perm.perm (b))

theorem AlgebraicCombinatorics.sn_card (n : ℕ) : Fintype.card (Sn n) = n.factorial

The symmetric group S_n has n! elements. (def.perm.Sn-iven)

This is the key cardinality result: |S_n| = n!

theorem AlgebraicCombinatorics.sn_zero_card : Fintype.card (Sn 0) = 1

S_0 is trivial (has exactly one element, the identity).

theorem AlgebraicCombinatorics.sn_one_card : Fintype.card (Sn 1) = 1

S_1 is trivial (has exactly one element, the identity).

theorem AlgebraicCombinatorics.sn_two_card : Fintype.card (Sn 2) = 2

S_2 has exactly 2 elements.

theorem AlgebraicCombinatorics.sn_three_card : Fintype.card (Sn 3) = 6

S_3 has exactly 6 elements.

theorem AlgebraicCombinatorics.bracketN_card (n : ℕ) : Fintype.card (bracketN n) = n

[n] has exactly n elements.

instance AlgebraicCombinatorics.sn_fintype (n : ℕ) : Fintype (Sn n)

S_n is a finite group.

Equations

• AlgebraicCombinatorics.sn_fintype n = inferInstance

instance AlgebraicCombinatorics.sn_decidableEq (n : ℕ) : DecidableEq (Sn n)

S_n has decidable equality.

Equations

• AlgebraicCombinatorics.sn_decidableEq n = inferInstance

Composition notation (def.perm.perm (c))

In the textbook, αβ denotes the composition α ∘ β, which sends x to α(β(x)). In Mathlib, this is the group multiplication α * β.

theorem AlgebraicCombinatorics.perm_mul_apply {X : Type u_1} (α β : Equiv.Perm X) (x : X) : (α * β) x = α (β x)

The composition α * β sends x to α(β(x)). (def.perm.perm (c))

theorem AlgebraicCombinatorics.perm_mul_assoc {X : Type u_1} (α β γ : Equiv.Perm X) : α * β * γ = α * (β * γ)

Composition is associative: (αβ)γ = α(βγ).

theorem AlgebraicCombinatorics.perm_one_mul {X : Type u_1} (α : Equiv.Perm X) : 1 * α = α

The identity permutation is the neutral element: id * α = α.

theorem AlgebraicCombinatorics.perm_mul_one {X : Type u_1} (α : Equiv.Perm X) : α * 1 = α

The identity permutation is the neutral element: α * id = α.

Powers of permutations (def.perm.perm (d))

The i-th power α^i is defined for any integer i.

theorem AlgebraicCombinatorics.perm_pow_zero {X : Type u_1} (α : Equiv.Perm X) : α ^ 0 = 1

α^0 = id. (def.perm.perm (d))

theorem AlgebraicCombinatorics.perm_zpow_zero {X : Type u_1} (α : Equiv.Perm X) : α ^ 0 = 1

α^0 = id for integer exponents. (def.perm.perm (d))

theorem AlgebraicCombinatorics.perm_pow_one {X : Type u_1} (α : Equiv.Perm X) : α ^ 1 = α

α^1 = α.

theorem AlgebraicCombinatorics.perm_pow_succ {X : Type u_1} (α : Equiv.Perm X) (n : ℕ) : α ^ (n + 1) = α ^ n * α

For i ≥ 0, α^i = α ∘ α ∘ ⋯ ∘ α (i times). (def.perm.perm (d))

theorem AlgebraicCombinatorics.perm_pow_succ' {X : Type u_1} (α : Equiv.Perm X) (n : ℕ) : α ^ (n + 1) = α * α ^ n

Alternative form: α^(n+1) = α * α^n.

theorem AlgebraicCombinatorics.perm_zpow_neg_one {X : Type u_1} (α : Equiv.Perm X) : α ^ (-1) = α⁻¹

α^(-1) is the inverse of α. (def.perm.perm (d))

theorem AlgebraicCombinatorics.perm_mul_inv {X : Type u_1} (α : Equiv.Perm X) : α * α⁻¹ = 1

The inverse satisfies α * α⁻¹ = id.

theorem AlgebraicCombinatorics.perm_inv_mul {X : Type u_1} (α : Equiv.Perm X) : α⁻¹ * α = 1

The inverse satisfies α⁻¹ * α = id.

theorem AlgebraicCombinatorics.perm_pow_apply {X : Type u_1} (α : Equiv.Perm X) (n : ℕ) (x : X) : (α ^ n) x = (⇑α)^[n] x

Applying α^n to x gives the n-fold application of α.

theorem AlgebraicCombinatorics.perm_zpow_neg {X : Type u_1} (α : Equiv.Perm X) (n : ℕ) : α ^ (-↑n) = α⁻¹ ^ n

For integer powers, α^(-n) applies the inverse n times.

Conjugation isomorphism (prop.perm.Sf)

If f : X ≃ Y is a bijection, then the map σ ↦ f ∘ σ ∘ f⁻¹ is a group isomorphism from S_X to S_Y.

def AlgebraicCombinatorics.symmetricGroup_conj_iso {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) : Equiv.Perm X ≃* Equiv.Perm Y

Given a bijection f : X ≃ Y, conjugation by f gives a group isomorphism from Perm X to Perm Y. (prop.perm.Sf)

For each permutation σ of X, the map f ∘ σ ∘ f⁻¹ : Y → Y is a permutation of Y. Furthermore, the map S_f : S_X → S_Y, σ ↦ f ∘ σ ∘ f⁻¹ is a group isomorphism.

Equations

• AlgebraicCombinatorics.symmetricGroup_conj_iso f = f.permCongrHom

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_apply {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) (σ : Equiv.Perm X) : (symmetricGroup_conj_iso f) σ = f.permCongr σ

The conjugation isomorphism sends σ to f ∘ σ ∘ f⁻¹.

theorem AlgebraicCombinatorics.symmetricGroup_conj_isPerm {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) (σ : Equiv.Perm X) : ∃ (τ : Equiv.Perm Y), ∀ (y : Y), τ y = f (σ (f.symm y))

For each permutation σ of X, the map f ∘ σ ∘ f⁻¹ : Y → Y is a permutation of Y. This is the first part of prop.perm.Sf.

@[simp]

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_apply_val {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) (σ : Equiv.Perm X) (y : Y) : ((symmetricGroup_conj_iso f) σ) y = f (σ (f.symm y))

The conjugation map explicitly: S_f(σ)(y) = f(σ(f⁻¹(y))).

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_bijective {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) : Function.Bijective ⇑(symmetricGroup_conj_iso f)

The conjugation isomorphism is bijective (part of being an isomorphism).

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_mul {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) (σ τ : Equiv.Perm X) : (symmetricGroup_conj_iso f) (σ * τ) = (symmetricGroup_conj_iso f) σ * (symmetricGroup_conj_iso f) τ

The conjugation isomorphism is a group homomorphism (part of being an isomorphism).

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_one {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) : (symmetricGroup_conj_iso f) 1 = 1

The conjugation isomorphism preserves identity.

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_symm {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) : (symmetricGroup_conj_iso f).symm = symmetricGroup_conj_iso f.symm

The inverse of the conjugation isomorphism is conjugation by f⁻¹.

theorem AlgebraicCombinatorics.symmetricGroup_iso_of_equiv {X : Type u_1} {Y : Type u_2} (f : X ≃ Y) : Nonempty (Equiv.Perm X ≃* Equiv.Perm Y)

Symmetric groups of bijective sets are isomorphic. (Conclusion of prop.perm.Sf)

theorem AlgebraicCombinatorics.symmetricGroup_conj_iso_self {X : Type u_1} (f σ : Equiv.Perm X) : (symmetricGroup_conj_iso f) σ = f * σ * f⁻¹

If Y = X in prop.perm.Sf, then S_f is conjugation by f in the group S_X. (Remark after prop.perm.Sf)

Permutation notations (def.perm.notations)

This section formalizes Definition def.perm.notations from the textbook, which introduces three notations for representing permutations:

(a) A two-line notation of σ is a 2×n-array where the top row contains elements of [n] in some order, and the bottom row contains their images under σ.

(b) The one-line notation (OLN) of σ is the n-tuple (σ(1), σ(2), ..., σ(n)).

(c) The cycle digraph of σ is a directed graph with vertices 1, 2, ..., n and arcs i → σ(i) for all i ∈ [n].

In Lean, we formalize these as follows:

• Two-line notation: a function that maps each element to its image (essentially the permutation itself)
• One-line notation: a Fin n → Fin n function, or equivalently a Vector (Fin n) n
• Cycle digraph: a SimpleGraph with edges determined by the permutation

Two-line notation (def.perm.notations (a))

A two-line notation of σ ∈ S_n is a 2×n-array where:

• The top row contains the elements p₁, p₂, ..., pₙ of [n] in some order
• The bottom row contains σ(p₁), σ(p₂), ..., σ(pₙ)

The most common form uses pᵢ = i, giving the array: ⎛ 1 2 ... n ⎞ ⎝ σ(1) σ(2) ... σ(n) ⎠

In Lean, a permutation σ : Equiv.Perm (Fin n) already encodes this information: the "two-line notation" is essentially the graph of σ as a function.

def AlgebraicCombinatorics.twoLineNotation {n : ℕ} (σ : Sn n) : List (Fin n × Fin n)

The two-line notation of a permutation σ ∈ S_n, represented as a list of pairs [(1, σ(1)), (2, σ(2)), ..., (n, σ(n))].

This corresponds to the standard two-line notation: ⎛ 1 2 ... n ⎞ ⎝ σ(1) σ(2) ... σ(n) ⎠

(def.perm.notations (a))

Equations

• AlgebraicCombinatorics.twoLineNotation σ = List.map (fun (i : Fin n) => (i, σ i)) (List.finRange n)

theorem AlgebraicCombinatorics.twoLineNotation_length {n : ℕ} (σ : Sn n) : (twoLineNotation σ).length = n

The two-line notation has length n.

theorem AlgebraicCombinatorics.twoLineNotation_getElem {n : ℕ} (σ : Sn n) (i : ℕ) (hi : i < n) : (twoLineNotation σ)[i] = (⟨i, hi⟩, σ ⟨i, hi⟩)

The i-th entry of the two-line notation is (i, σ(i)).

theorem AlgebraicCombinatorics.twoLineNotation_fst {n : ℕ} (σ : Sn n) : List.map Prod.fst (twoLineNotation σ) = List.finRange n

The first components of the two-line notation are exactly 0, 1, ..., n-1.

theorem AlgebraicCombinatorics.twoLineNotation_snd {n : ℕ} (σ : Sn n) : List.map Prod.snd (twoLineNotation σ) = List.map (⇑σ) (List.finRange n)

The second components of the two-line notation are σ(0), σ(1), ..., σ(n-1).

theorem AlgebraicCombinatorics.eq_iff_twoLineNotation_eq {n : ℕ} (σ τ : Sn n) : σ = τ ↔ twoLineNotation σ = twoLineNotation τ

Two permutations are equal iff their two-line notations are equal.

One-line notation (def.perm.notations (b))

The one-line notation (OLN) of σ ∈ S_n is the n-tuple (σ(1), σ(2), ..., σ(n)).

In Lean, a permutation σ : Sn n = Equiv.Perm (Fin n) is already essentially its OLN, since we can evaluate σ at any index. We provide explicit conversions.

def AlgebraicCombinatorics.oneLineNotation {n : ℕ} (σ : Sn n) : List (Fin n)

The one-line notation of a permutation σ ∈ S_n, as a list [σ(0), σ(1), ..., σ(n-1)].

Note: We use 0-indexing (Fin n starts at 0), so this is [σ(0), σ(1), ..., σ(n-1)] rather than [σ(1), σ(2), ..., σ(n)] as in the textbook.

(def.perm.notations (b))

Equations

• AlgebraicCombinatorics.oneLineNotation σ = List.map (⇑σ) (List.finRange n)

theorem AlgebraicCombinatorics.oneLineNotation_length {n : ℕ} (σ : Sn n) : (oneLineNotation σ).length = n

The one-line notation has length n.

theorem AlgebraicCombinatorics.oneLineNotation_getElem {n : ℕ} (σ : Sn n) (i : ℕ) (hi : i < n) : (oneLineNotation σ)[i] = σ ⟨i, hi⟩

The i-th entry of the one-line notation is σ(i).

theorem AlgebraicCombinatorics.oneLineNotation_nodup {n : ℕ} (σ : Sn n) : (oneLineNotation σ).Nodup

The one-line notation contains no duplicates.

theorem AlgebraicCombinatorics.eq_iff_oneLineNotation_eq {n : ℕ} (σ τ : Sn n) : σ = τ ↔ oneLineNotation σ = oneLineNotation τ

Two permutations are equal iff their one-line notations are equal.

noncomputable def AlgebraicCombinatorics.oneLineNotationToPerm {n : ℕ} (l : List (Fin n)) (hl : l.length = n) (hnodup : l.Nodup) : Sn n

Convert a list to a permutation, if it's a valid one-line notation. Returns the permutation represented by the list.

Equations

• AlgebraicCombinatorics.oneLineNotationToPerm l hl hnodup = Equiv.ofBijective (fun (i : Fin n) => l[↑i]) ⋯

theorem AlgebraicCombinatorics.oneLineNotationToPerm_oneLineNotation {n : ℕ} (σ : Sn n) : oneLineNotationToPerm (oneLineNotation σ) ⋯ ⋯ = σ

Round-trip: converting a permutation to OLN and back gives the original permutation.

Cycle digraph (def.perm.notations (c))

The cycle digraph of σ ∈ S_n is a directed graph with:

• Vertices: 1, 2, ..., n (or 0, 1, ..., n-1 in 0-indexed form)
• Arcs: i → σ(i) for all i ∈ [n]

In Lean, we represent this as a SimpleGraph where there's an edge between i and j iff σ(i) = j (and i ≠ j to avoid self-loops in the SimpleGraph sense).

Note: The cycle digraph is naturally a directed graph, but for simplicity we can also consider the underlying undirected graph structure.

def AlgebraicCombinatorics.cycleDigraph {n : ℕ} (σ : Sn n) : SimpleGraph (Fin n)

The cycle digraph of a permutation σ, as an undirected simple graph.

There is an edge between i and j iff σ(i) = j or σ(j) = i (and i ≠ j). This captures the "orbit structure" of the permutation.

(def.perm.notations (c))

Equations

• AlgebraicCombinatorics.cycleDigraph σ = { Adj := fun (i j : Fin n) => i ≠ j ∧ (σ i = j ∨ σ j = i), symm := ⋯, loopless := ⋯ }

theorem AlgebraicCombinatorics.cycleDigraph_adj_iff {n : ℕ} (σ : Sn n) (i j : Fin n) : (cycleDigraph σ).Adj i j ↔ i ≠ j ∧ (σ i = j ∨ σ j = i)

Two vertices are adjacent in the cycle digraph iff one maps to the other under σ.

theorem AlgebraicCombinatorics.cycleDigraph_adj_of_apply {n : ℕ} (σ : Sn n) {i j : Fin n} (h : σ i = j) (hne : i ≠ j) : (cycleDigraph σ).Adj i j

If σ(i) = j and i ≠ j, then i and j are adjacent in the cycle digraph.

theorem AlgebraicCombinatorics.cycleDigraph_connected_iff {n : ℕ} (σ : Sn n) (i j : Fin n) : (cycleDigraph σ).Reachable i j ↔ ∃ (k : ℤ), (σ ^ k) i = j

The connected components of the cycle digraph correspond to the orbits of σ.

theorem AlgebraicCombinatorics.cycleDigraph_one {n : ℕ} : cycleDigraph 1 = ⊥

The identity permutation has a cycle digraph with no edges.

theorem AlgebraicCombinatorics.cycleDigraph_swap_adj_iff {n : ℕ} (i j : Fin n) (hij : i ≠ j) (a b : Fin n) : (cycleDigraph (Equiv.swap i j)).Adj a b ↔ a = i ∧ b = j ∨ a = j ∧ b = i

A transposition creates an edge between the swapped elements.

Transpositions (def.perm.tij)

A transposition t_{i,j} swaps i and j and fixes all other elements.

From the textbook (def.perm.tij):

Let i and j be two distinct elements of a set X. Then, the transposition t_{i,j} is the permutation of X that sends i to j, sends j to i, and leaves all other elements of X unchanged.

In Mathlib, this is Equiv.swap i j.

@[reducible, inline]

abbrev AlgebraicCombinatorics.transposition {X : Type u_1} [DecidableEq X] (i j : X) : Equiv.Perm X

The transposition swapping i and j. In Mathlib, this is Equiv.swap i j. (def.perm.tij)

A transposition t_{i,j} is the permutation of X that:

• sends i to j (see transposition_apply_left)
• sends j to i (see transposition_apply_right)
• leaves all other elements unchanged (see transposition_apply_of_ne_of_ne)

Equations

• AlgebraicCombinatorics.transposition i j = Equiv.swap i j

@[simp]

theorem AlgebraicCombinatorics.transposition_apply_left {X : Type u_1} [DecidableEq X] (i j : X) : (transposition i j) i = j

The transposition t_{i,j} sends i to j. (def.perm.tij)

@[simp]

theorem AlgebraicCombinatorics.transposition_apply_right {X : Type u_1} [DecidableEq X] (i j : X) : (transposition i j) j = i

The transposition t_{i,j} sends j to i. (def.perm.tij)

theorem AlgebraicCombinatorics.transposition_apply_of_ne_of_ne {X : Type u_1} [DecidableEq X] {i j x : X} (hi : x ≠ i) (hj : x ≠ j) : (transposition i j) x = x

The transposition t_{i,j} leaves all other elements unchanged. (def.perm.tij)

theorem AlgebraicCombinatorics.transposition_symm {X : Type u_1} [DecidableEq X] (i j : X) : transposition i j = transposition j i

Transpositions are symmetric: t_{i,j} = t_{j,i}.

theorem AlgebraicCombinatorics.transposition_inv {X : Type u_1} [DecidableEq X] (i j : X) : (transposition i j)⁻¹ = transposition i j

A transposition is its own inverse: t_{i,j}⁻¹ = t_{i,j}.

theorem AlgebraicCombinatorics.transposition_sq_eq_one {X : Type u_1} [DecidableEq X] (i j : X) : transposition i j * transposition i j = 1

A transposition squared is the identity: t_{i,j}² = id.

theorem AlgebraicCombinatorics.num_transpositions (X : Type u_1) [DecidableEq X] [Fintype X] : ∃ (S : Finset (Equiv.Perm X)), (∀ σ ∈ S, σ.IsSwap) ∧ (∀ (σ : Equiv.Perm X), σ.IsSwap → σ ∈ S) ∧ S.card = (Fintype.card X).choose 2

The number of transpositions (2-cycles) in S_X is C(|X|, 2). This follows from the fact that each 2-element subset {i,j} of X gives rise to exactly one transposition t_{i,j}. (Example after def.perm.cycs in source)

Simple transpositions (def.perm.si)

The simple transposition s_i swaps i and i+1.

def AlgebraicCombinatorics.simpleTransposition {n : ℕ} (i : Fin (n - 1)) : Sn n

The simple transposition s_i swaps i and i+1 in Fin n. Here i : Fin (n - 1) ensures i+1 < n. (def.perm.si)

This is the canonical definition for simple transpositions in the codebase.

Equivalent definition in Inversions2.lean: Equiv.Perm.simpleTransposition in Inversions2.lean defines the same permutation using a slightly different construction (with castSucc/succ). The equivalence is proven by Equiv.Perm.simpleTransposition_eq_canonical.

See the equivalence lemmas simpleTransposition_eq_swap_* below for other formulations.

Equations

• AlgebraicCombinatorics.simpleTransposition i = Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

def AlgebraicCombinatorics.«termS[_]» : Lean.ParserDescr

Notation for simple transposition.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.simpleTransposition_eq_transposition {n : ℕ} (i : Fin (n - 1)) : simpleTransposition i = transposition ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

Simple transposition s_i equals the transposition t_{i,i+1}. (def.perm.si)

@[simp]

theorem AlgebraicCombinatorics.simpleTransposition_apply_self {n : ℕ} (i : Fin (n - 1)) : (simpleTransposition i) ⟨↑i, ⋯⟩ = ⟨↑i + 1, ⋯⟩

Simple transposition s_i sends i to i+1. (def.perm.si)

@[simp]

theorem AlgebraicCombinatorics.simpleTransposition_apply_succ {n : ℕ} (i : Fin (n - 1)) : (simpleTransposition i) ⟨↑i + 1, ⋯⟩ = ⟨↑i, ⋯⟩

Simple transposition s_i sends i+1 to i. (def.perm.si)

theorem AlgebraicCombinatorics.simpleTransposition_apply_of_ne {n : ℕ} (i : Fin (n - 1)) (k : Fin n) (hi : ↑k ≠ ↑i) (hi1 : ↑k ≠ ↑i + 1) : (simpleTransposition i) k = k

Simple transposition s_i fixes any k ≠ i, i+1. (def.perm.si)

theorem AlgebraicCombinatorics.simpleTransposition_support {n : ℕ} (i : Fin (n - 1)) : Equiv.Perm.support (simpleTransposition i) = {⟨↑i, ⋯⟩, ⟨↑i + 1, ⋯⟩}

The support of a simple transposition is exactly {i, i+1}. (def.perm.si)

theorem AlgebraicCombinatorics.simpleTransposition_isSwap {n : ℕ} (i : Fin (n - 1)) : Equiv.Perm.IsSwap (simpleTransposition i)

Simple transpositions are swaps (i.e., 2-cycles). (def.perm.si)

theorem AlgebraicCombinatorics.simpleTransposition_isCycle {n : ℕ} (i : Fin (n - 1)) : Equiv.Perm.IsCycle (simpleTransposition i)

Simple transpositions are cycles (2-cycles). (def.perm.si)

theorem AlgebraicCombinatorics.simpleTransposition_support_card {n : ℕ} (i : Fin (n - 1)) : (Equiv.Perm.support (simpleTransposition i)).card = 2

The support of a simple transposition has cardinality 2. (def.perm.si)

theorem AlgebraicCombinatorics.simpleTransposition_ne_one {n : ℕ} (i : Fin (n - 1)) : simpleTransposition i ≠ 1

Simple transposition is not the identity (for n ≥ 2). (def.perm.si)

Properties of simple transpositions (prop.perm.si.rules)

theorem AlgebraicCombinatorics.simpleTransposition_sq_eq_one {n : ℕ} (i : Fin (n - 1)) : simpleTransposition i * simpleTransposition i = 1

Simple transpositions are involutions: s_i² = id. (prop.perm.si.rules (a))

theorem AlgebraicCombinatorics.simpleTransposition_inv {n : ℕ} (i : Fin (n - 1)) : (simpleTransposition i)⁻¹ = simpleTransposition i

Simple transpositions are self-inverse: s_i⁻¹ = s_i. (prop.perm.si.rules (a))

theorem AlgebraicCombinatorics.simpleTransposition_comm {n : ℕ} (i j : Fin (n - 1)) (h : ↑i + 1 < ↑j ∨ ↑j + 1 < ↑i) : simpleTransposition i * simpleTransposition j = simpleTransposition j * simpleTransposition i

Simple transpositions commute when |i - j| > 1. (prop.perm.si.rules (b))

theorem AlgebraicCombinatorics.simpleTransposition_braid {n : ℕ} (i : Fin (n - 2)) : have i' := ⟨↑i, ⋯⟩; have i1 := ⟨↑i + 1, ⋯⟩; simpleTransposition i' * simpleTransposition i1 * simpleTransposition i' = simpleTransposition i1 * simpleTransposition i' * simpleTransposition i1

The braid relation: s_i s_{i+1} s_i = s_{i+1} s_i s_{i+1}. (prop.perm.si.rules (c))

Equivalence lemmas for simpleTransposition

The simpleTransposition function is the canonical definition for the simple transposition s_i that swaps i and i+1 in Fin n. Other files may define local versions with slightly different signatures. These lemmas establish the equivalence between formulations.

Alternative formulations in the codebase:

1. Equiv.Perm.simpleTransposition in Inversions2.lean - uses castSucc/succ pattern
2. simpleTransposition in SymmetricFunctions/Definitions.lean - uses Nat.lt_of_lt_pred
3. simpleTransposition in SchurBasics.lean - takes Fin N with explicit proof hk : k.val + 1 < N

All these definitions compute the same permutation: Equiv.swap k (k+1).

theorem AlgebraicCombinatorics.simpleTransposition_eq_swap {n : ℕ} (i : Fin (n - 1)) : simpleTransposition i = Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

The canonical simpleTransposition equals Equiv.swap on the appropriate Fin elements. This is the fundamental characterization used to prove equivalence with other formulations.

theorem AlgebraicCombinatorics.simpleTransposition_eq_swap_castSucc_succ {n : ℕ} (i : Fin (n - 1)) (hn : n > 0) : simpleTransposition i = Equiv.swap (Fin.castLE ⋯ i.castSucc) (Fin.castLE ⋯ i.succ)

Alternative characterization: simpleTransposition using castSucc and succ. This matches the formulation in Inversions2.lean.

theorem AlgebraicCombinatorics.simpleTransposition_eq_swap_explicit {N : ℕ} (k : Fin N) (hk : ↑k + 1 < N) : have i := ⟨↑k, ⋯⟩; simpleTransposition i = Equiv.swap k ⟨↑k + 1, hk⟩

Alternative characterization: when given k : Fin N and a proof hk : k.val + 1 < N, this equals Equiv.swap k ⟨k.val + 1, hk⟩. This matches the formulation in SchurBasics.lean.

theorem AlgebraicCombinatorics.simpleTransposition_eq_swap_with_proofs {N : ℕ} (i : Fin (N - 1)) : simpleTransposition i = Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

Conversion from Fin (N - 1) index to explicit proof form. Given i : Fin (N - 1), we can express simpleTransposition i as a swap with explicit bounds proofs. This matches the formulation in Definitions.lean.

Cycles (def.perm.cycs)

A k-cycle is a permutation that cyclically permutes k elements and fixes all others.

The textbook defines cyc_{i₁, i₂, ..., iₖ} as the permutation that sends

• i₁ ↦ i₂
• i₂ ↦ i₃
• ...
• iₖ₋₁ ↦ iₖ
• iₖ ↦ i₁ and fixes all other elements.

In Mathlib, this is List.formPerm. The predicate Equiv.Perm.IsCycle captures when a permutation is a cycle.

def AlgebraicCombinatorics.cyc {X : Type u_1} [DecidableEq X] (l : List X) : Equiv.Perm X

The k-cycle cyc_{i₁, i₂, ..., iₖ} is the permutation that sends i₁ ↦ i₂ ↦ i₃ ↦ ... ↦ iₖ ↦ i₁ and fixes all other elements. (def.perm.cycs)

This is the constructive definition from the textbook. In Mathlib, this is List.formPerm.

Equations

• AlgebraicCombinatorics.cyc l = l.formPerm

theorem AlgebraicCombinatorics.cyc_pair {X : Type u_1} [DecidableEq X] (i j : X) : cyc [i, j] = Equiv.swap i j

The cycle cyc [i, j] equals the transposition swap i j. This shows that 2-cycles are exactly transpositions.

@[simp]

theorem AlgebraicCombinatorics.cyc_nil {X : Type u_1} [DecidableEq X] : cyc [] = 1

The cycle cyc [] is the identity.

@[simp]

theorem AlgebraicCombinatorics.cyc_singleton {X : Type u_1} [DecidableEq X] (x : X) : cyc [x] = 1

The cycle cyc [x] is the identity.

theorem AlgebraicCombinatorics.cyc_apply_of_not_mem {X : Type u_1} [DecidableEq X] {l : List X} {x : X} (h : x ∉ l) : (cyc l) x = x

The cycle applied to an element not in the list returns the element unchanged. This is the "otherwise" case in def.perm.cycs.

theorem AlgebraicCombinatorics.cyc_apply_cons_cons {X : Type u_1} [DecidableEq X] (x y : X) (l : List X) : cyc (x :: y :: l) = Equiv.swap x y * cyc (y :: l)

A cycle sends each element to the next in the list.

theorem AlgebraicCombinatorics.cyc_isCycle {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) (hn : 2 ≤ l.length) : (cyc l).IsCycle

If the list has no duplicates and length ≥ 2, then cyc l is a cycle in the sense of IsCycle.

theorem AlgebraicCombinatorics.cyc_apply_eq_next {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) {x : X} (hx : x ∈ l) : (cyc l) x = l.next x hx

For a list with no duplicates and x in the list, cyc l x is the next element in the list (wrapping around at the end).

theorem AlgebraicCombinatorics.cyc_support_subset {X : Type u_1} [DecidableEq X] [Fintype X] {l : List X} : (cyc l).support ⊆ l.toFinset

The support of cyc l is contained in l.toFinset.

theorem AlgebraicCombinatorics.cyc_support_eq_toFinset {X : Type u_1} [DecidableEq X] [Fintype X] {l : List X} (hl : l.Nodup) (hn : 2 ≤ l.length) : (cyc l).support = l.toFinset

For a nodup list with length ≥ 2, the support of cyc l equals l.toFinset.

theorem AlgebraicCombinatorics.cyc_rotate {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) (n : ℕ) : cyc (l.rotate n) = cyc l

Cyclic rotation of the list doesn't change the cycle. This formalizes the textbook statement that cyc_{i₁,i₂,...,iₖ} = cyc_{i₂,i₃,...,iₖ,i₁} = ... = cyc_{iₖ,i₁,...,iₖ₋₁}.

theorem AlgebraicCombinatorics.cyc_rotate_one {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) : cyc (l.rotate 1) = cyc l

The cycle cyc [i₁, i₂, ..., iₖ] equals cyc [i₂, ..., iₖ, i₁].

theorem AlgebraicCombinatorics.cyc_apply_getElem {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) (j : ℕ) (hj : j < l.length) : (cyc l) l[j] = l[(j + 1) % l.length]

The cycle sends l[j] to l[(j+1) % l.length] for a nodup list. This is the formal statement of def.perm.cycs from the textbook: "cyc_{i₁,...,iₖ}(p) = i_{j+1} if p = i_j for some j ∈ {1,...,k}"

theorem AlgebraicCombinatorics.cyc_eq_cyc_iff_isRotated {X : Type u_1} [DecidableEq X] {l l' : List X} (hl : l.Nodup) (hl' : l'.Nodup) (hlen : 2 ≤ l.length) (_hlen' : 2 ≤ l'.length) : cyc l = cyc l' ↔ l ~r l'

For k-cycles with k ≥ 2 distinct elements, the cycle uniquely determines the elements up to cyclic rotation. This is stated in the solution to exe.perm.cyc.how-many-kcyc.

@[reducible, inline]

abbrev AlgebraicCombinatorics.IsCycle {X : Type u_1} (σ : Equiv.Perm X) : Prop

A permutation is a cycle if any two non-fixed points are related by repeated application of the permutation.

Equations

• AlgebraicCombinatorics.IsCycle σ = σ.IsCycle

@[reducible, inline]

abbrev AlgebraicCombinatorics.cycleSupport {X : Type u_1} [DecidableEq X] [Fintype X] (σ : Equiv.Perm X) : Finset X

The support of a cycle (the set of elements it moves).

Equations

• AlgebraicCombinatorics.cycleSupport σ = σ.support

theorem AlgebraicCombinatorics.cycle_eq_transposition {X : Type u_1} [DecidableEq X] [Fintype X] {σ : Equiv.Perm X} (hσ : σ.IsCycle) (hcard : σ.support.card = 2) : ∃ (i : X) (j : X), i ≠ j ∧ σ = Equiv.swap i j

A 2-cycle is exactly a transposition. (Example after def.perm.cycs)

Counting k-cycles (exe.perm.cyc.how-many-kcyc)

The number of k-cycles in S_n (for k > 1) is n(n-1)...(n-k+1)/k = C(n,k) * (k-1)!.

theorem AlgebraicCombinatorics.num_kCycles_formula (n k : ℕ) (hk : 1 < k) (hkn : k ≤ n) : ∃ (S : Finset (Sn n)), (∀ σ ∈ S, Equiv.Perm.IsCycle σ ∧ (Equiv.Perm.support σ).card = k) ∧ (∀ (σ : Sn n), Equiv.Perm.IsCycle σ → (Equiv.Perm.support σ).card = k → σ ∈ S) ∧ S.card = n.choose k * (k - 1).factorial

The number of k-cycles in S_n is C(n,k) * (k-1)! for k > 1. (exe.perm.cyc.how-many-kcyc)

The formula counts the number of ways to choose k elements from n (giving C(n,k)) and then arrange them in a cycle (giving (k-1)! since cyclic rotations are equivalent).

theorem AlgebraicCombinatorics.no_1Cycles_isCycle (n : ℕ) (σ : Sn n) (hσ : Equiv.Perm.IsCycle σ) : 2 ≤ (Equiv.Perm.support σ).card

For k = 1, the only "1-cycle" would be the identity, but IsCycle excludes the identity. So there are no 1-cycles satisfying IsCycle.

Involutions (def.perm.invol)

An involution is a permutation equal to its own inverse.

def AlgebraicCombinatorics.IsInvolution {X : Type u_1} (σ : Equiv.Perm X) : Prop

A permutation is an involution if σ ∘ σ = id. (def.perm.invol)

From the textbook:

An involution of X means a map f: X → X that satisfies f ∘ f = id. Clearly, an involution is always a permutation, and equals its own inverse.

Equivalent characterizations:

• IsInvolution σ ↔ σ * σ = 1 (definition)
• IsInvolution σ ↔ σ⁻¹ = σ (see isInvolution_iff_eq_inv)
• IsInvolution σ ↔ Function.Involutive σ (see isInvolution_iff_involutive)
• IsInvolution σ ↔ ∀ x, σ (σ x) = x (see isInvolution_iff_forall)

Equations

• AlgebraicCombinatorics.IsInvolution σ = (σ * σ = 1)

instance AlgebraicCombinatorics.instDecidableIsInvolution {X : Type u_1} [Fintype X] [DecidableEq X] (σ : Equiv.Perm X) : Decidable (IsInvolution σ)

Decidable instance for IsInvolution on finite types.

Equations

• AlgebraicCombinatorics.instDecidableIsInvolution σ = inferInstanceAs (Decidable (σ * σ = 1))

theorem AlgebraicCombinatorics.IsInvolution.eq_inv {X : Type u_1} {σ : Equiv.Perm X} (h : IsInvolution σ) : σ⁻¹ = σ

An involution is equal to its own inverse.

theorem AlgebraicCombinatorics.isInvolution_iff_eq_inv {X : Type u_1} {σ : Equiv.Perm X} : IsInvolution σ ↔ σ⁻¹ = σ

Characterization: σ is an involution iff σ⁻¹ = σ.

theorem AlgebraicCombinatorics.isInvolution_iff_involutive {X : Type u_1} {σ : Equiv.Perm X} : IsInvolution σ ↔ Function.Involutive ⇑σ

Characterization: σ is an involution iff it is involutive as a function.

theorem AlgebraicCombinatorics.isInvolution_iff_forall {X : Type u_1} {σ : Equiv.Perm X} : IsInvolution σ ↔ ∀ (x : X), σ (σ x) = x

Characterization: σ is an involution iff σ(σ(x)) = x for all x.

theorem AlgebraicCombinatorics.IsInvolution.apply_apply {X : Type u_1} {σ : Equiv.Perm X} (h : IsInvolution σ) (x : X) : σ (σ x) = x

An involution applied twice is the identity.

theorem AlgebraicCombinatorics.isInvolution_one {X : Type u_1} : IsInvolution 1

The identity is an involution.

theorem AlgebraicCombinatorics.isInvolution_transposition {X : Type u_1} [DecidableEq X] (i j : X) : IsInvolution (transposition i j)

Any transposition is an involution.

theorem AlgebraicCombinatorics.isInvolution_simpleTransposition {n : ℕ} (i : Fin (n - 1)) : IsInvolution (simpleTransposition i)

Simple transpositions are involutions.

theorem AlgebraicCombinatorics.IsInvolution.orderOf_dvd_two {X : Type u_1} [Fintype X] {σ : Equiv.Perm X} (h : IsInvolution σ) : orderOf σ ∣ 2

The order of an involution divides 2.

theorem AlgebraicCombinatorics.IsInvolution.orderOf_le_two {X : Type u_1} [Fintype X] {σ : Equiv.Perm X} (h : IsInvolution σ) : orderOf σ ≤ 2

An involution has order 1 or 2.

theorem AlgebraicCombinatorics.IsInvolution.eq_one_iff_orderOf_eq_one {X : Type u_1} {σ : Equiv.Perm X} (_h : IsInvolution σ) : σ = 1 ↔ orderOf σ = 1

An involution is the identity iff its order is 1.

theorem AlgebraicCombinatorics.IsInvolution.orderOf_eq_two_of_ne_one {X : Type u_1} [Fintype X] {σ : Equiv.Perm X} (h : IsInvolution σ) (hne : σ ≠ 1) : orderOf σ = 2

A nontrivial involution has order exactly 2.

theorem AlgebraicCombinatorics.not_isInvolution_of_cycle_gt_two {X : Type u_1} [DecidableEq X] [Fintype X] {σ : Equiv.Perm X} (hσ : σ.IsCycle) (hcard : 2 < σ.support.card) : ¬IsInvolution σ

A k-cycle with k > 2 is never an involution.

theorem AlgebraicCombinatorics.isInvolution_of_disjoint_transpositions {X : Type u_1} [DecidableEq X] {pairs : List (X × X)} (hdisjoint : List.Pairwise (fun (p q : X × X) => p.1 ≠ q.1 ∧ p.1 ≠ q.2 ∧ p.2 ≠ q.1 ∧ p.2 ≠ q.2) pairs) (hdistinct : ∀ p ∈ pairs, p.1 ≠ p.2) : IsInvolution (List.map (fun (p : X × X) => transposition p.1 p.2) pairs).prod

Products of disjoint transpositions are involutions. (This is stated informally in the source after def.perm.invol)

theorem AlgebraicCombinatorics.involution_cycle_structure {X : Type u_1} [DecidableEq X] [Fintype X] {σ : Equiv.Perm X} (h : IsInvolution σ) (c : Equiv.Perm X) : c ∈ σ.cycleFactorsFinset → c.support.card ≤ 2

The cycle digraph of an involution consists of 1-cycles and 2-cycles. (Stated informally at the end of the source)

theorem AlgebraicCombinatorics.involution_is_product_of_disjoint_transpositions {X : Type u_1} [DecidableEq X] [Fintype X] {σ : Equiv.Perm X} (h : IsInvolution σ) : ∃ (pairs : List (X × X)), List.Pairwise (fun (p q : X × X) => p.1 ≠ q.1 ∧ p.1 ≠ q.2 ∧ p.2 ≠ q.1 ∧ p.2 ≠ q.2) pairs ∧ (∀ p ∈ pairs, p.1 ≠ p.2) ∧ σ = (List.map (fun (p : X × X) => transposition p.1 p.2) pairs).prod

An involution of a finite set is a product of disjoint transpositions. (Stated informally in the source)