Tilings of the symmetric group by transpositions

8 fully proved1 ready to prove

Fang Xia Tiling Problem

DefinitionTiling of a group by two subsets#✓fully proved

For subsets \(X\) and \(Y\) of a group \(G\), the pair \((X, Y)\) is a tiling (or factorisation) of \(G\) if every \(g \in G\) can be written as \(g = xy\) with \(x \in X\) and \(y \in Y\) for exactly one pair \((x, y)\).

def IsTiling {G : Type*} [Group G] (X Y : Set G) : Prop :=
  ∀ g : G, ∃! p : X × Y, (p.1 : G) * (p.2 : G) = g

Used by 1

Used byFang–Xia: tilings by transpositions and λ-transitivity

DefinitionThe identity and the transpositions#✓fully proved

\(T_n\) is the set of permutations of \(\{0, \dots, n-1\}\) consisting of the identity and all transpositions \((i\ j)\) with \(i \ne j\).

def transpositionsWithOne (n : ℕ) : Set (Equiv.Perm (Fin n)) :=
  {σ | σ = 1 ∨ ∃ i j : Fin n, i ≠ j ∧ σ = Equiv.swap i j}

Used by 1

Used byFang–Xia: tilings by transpositions and λ-transitivity

StructureInteger partition as a list of row lengths#✓fully proved

A partition of \(n\) is encoded as a list \((\lambda_0, \lambda_1, \dots, \lambda_{k-1})\) of positive integers with \(\lambda_0 \ge \lambda_1 \ge \dots \ge \lambda_{k-1}\) and \(\lambda_0 + \dots + \lambda_{k-1} = n\); the \(\lambda_i\) are its row lengths.

structure PartitionShape (n : ℕ) where
  parts : List ℕ
  sorted : parts.Pairwise (· ≥ ·)
  positive : ∀ a ∈ parts, 0 < a
  sum_eq : parts.sum = n

Used by 5

Used byTwice the content sum of a partition · Fang–Xia: tilings by transpositions and λ-transitivity · λ-transitive sets of permutations · Ordered set partition of shape λ · Permutation sending one ordered set partition to another

Partition Shape

DefinitionShifted row-length sum#✓fully proved

For a natural number \(i\) and a list of natural numbers \(a_0, \dots, a_{k-1}\), this is the integer \(\sum_{j=0}^{k-1} a_j\,(a_j - 2(i + j) - 1)\); the empty list gives \(0\).

With \(i = 0\) and the row lengths of a partition, this is twice the content sum of the partition.

def contentSumAux : ℕ → List ℕ → ℤ
  | _, [] => 0
  | i, a :: as => (a : ℤ) * ((a : ℤ) - 2 * (i : ℤ) - 1) + contentSumAux (i + 1) as

Used by 1

Used byTwice the content sum of a partition

DefinitionTwice the content sum of a partition#✓fully proved

For a partition \(\lambda\) of \(n\) with row lengths \(\lambda_0 \ge \lambda_1 \ge \dots \ge \lambda_{k-1}\), this is the integer \(\sum_{i=0}^{k-1} \lambda_i\,(\lambda_i - 2i - 1)\).

This is twice the content sum \(\sum_{(i,j) \in \lambda} (j - i)\) of the Young diagram of \(\lambda\) (rows \(i\) and columns \(j\) counted from \(0\)), so it is nonnegative exactly when the content sum is. It is the row-length formula from the remark after Theorem 1.4 of Fang–Xia, whose one-indexed terms are \(\lambda_i\,(\lambda_i - 2i + 1)\).

def contentSum {n : ℕ} (lam : PartitionShape n) : ℤ :=
  contentSumAux 0 lam.parts

Uses 2 · Used by 1

Statement usesInteger partition as a list of row lengths · Shifted row-length sum

Used byFang–Xia: tilings by transpositions and λ-transitivity

Fang Xia Tiling Problem

StructureOrdered set partition of shape λ#✓fully proved

Let \(\lambda\) be a partition of \(n\) with row lengths \(\lambda_0 \ge \dots \ge \lambda_{k-1}\). An ordered set partition of \(\{0, \dots, n-1\}\) of shape \(\lambda\) is a sequence \((B_0, \dots, B_{k-1})\) of pairwise disjoint subsets of \(\{0, \dots, n-1\}\) whose union is \(\{0, \dots, n-1\}\) and with \(|B_i| = \lambda_i\) for every \(i\).

structure OrderedSetPartition {n : ℕ} (lam : PartitionShape n) where
  block : Fin lam.parts.length → Finset (Fin n)
  card_block : ∀ i : Fin lam.parts.length, (block i).card = lam.parts.get i
  pairwise_disjoint :
    Pairwise fun i j : Fin lam.parts.length => Disjoint (block i) (block j)
  union_eq_univ : (Finset.univ.biUnion block) = Finset.univ

Uses 1 · Used by 2

Statement usesInteger partition as a list of row lengths

Used byλ-transitive sets of permutations · Permutation sending one ordered set partition to another

DefinitionPermutation sending one ordered set partition to another#✓fully proved

Let \(\lambda\) be a partition of \(n\) and let \(P = (P_0, \dots, P_{k-1})\) and \(Q = (Q_0, \dots, Q_{k-1})\) be ordered set partitions of \(\{0, \dots, n-1\}\) of shape \(\lambda\). A permutation \(\sigma\) of \(\{0, \dots, n-1\}\) sends \(P\) to \(Q\) if \(\sigma(P_i) = Q_i\) for every \(i\).

def SendsPartition {n : ℕ} (σ : Equiv.Perm (Fin n)) {lam : PartitionShape n}
    (P Q : OrderedSetPartition lam) : Prop :=
  ∀ i : Fin lam.parts.length, (P.block i).image σ = Q.block i

Uses 2 · Used by 1

Statement usesOrdered set partition of shape λ · Integer partition as a list of row lengths

Used byλ-transitive sets of permutations

Definitionλ-transitive sets of permutations#✓fully proved

Let \(\lambda\) be a partition of \(n\) with row lengths \(\lambda_0 \ge \dots \ge \lambda_{k-1}\). A set \(Y\) of permutations of \(\{0, \dots, n-1\}\) is \(\lambda\)-transitive, in the sense of Martin and Sagan, if there is a positive integer \(r\) such that for any two ordered set partitions \(P = (P_0, \dots, P_{k-1})\) and \(Q = (Q_0, \dots, Q_{k-1})\) of \(\{0, \dots, n-1\}\) of shape \(\lambda\), exactly \(r\) permutations \(\sigma \in Y\) satisfy \(\sigma(P_i) = Q_i\) for every \(i\).

def IsPartitionTransitive {n : ℕ} (Y : Set (Equiv.Perm (Fin n)))
    (lam : PartitionShape n) : Prop :=
  ∃ r : ℕ, 0 < r ∧
    ∀ P Q : OrderedSetPartition lam,
      {σ : Equiv.Perm (Fin n) | σ ∈ Y ∧ SendsPartition σ P Q}.ncard = r

Uses 3 · Used by 1

Statement usesOrdered set partition of shape λ · Integer partition as a list of row lengths · Permutation sending one ordered set partition to another

Used byFang–Xia: tilings by transpositions and λ-transitivity

TheoremFang–Xia: tilings by transpositions and λ-transitivity#●ready to prove

Let \(S_n\) be the symmetric group on \(\{0, \dots, n-1\}\), let \(T_n \subseteq S_n\) consist of the identity and all transpositions, and let \(Y \subseteq S_n\) be such that \((T_n, Y)\) is a tiling of \(S_n\): every \(g \in S_n\) can be written as \(g = xy\) with \(x \in T_n\) and \(y \in Y\) for exactly one pair \((x, y)\). Let \(\lambda\) be a partition of \(n\) with row lengths \(\lambda_0 \ge \dots \ge \lambda_{k-1}\) such that \(\sum_{i=0}^{k-1} \lambda_i\,(\lambda_i - 2i - 1) \ge 0\) (equivalently, the content sum of the Young diagram of \(\lambda\) is nonnegative). Then \(Y\) is \(\lambda\)-transitive: there is a positive integer \(r\) such that for any two ordered set partitions \(P = (P_0, \dots, P_{k-1})\) and \(Q = (Q_0, \dots, Q_{k-1})\) of \(\{0, \dots, n-1\}\) with \(|P_i| = |Q_i| = \lambda_i\) for every \(i\), exactly \(r\) permutations \(\sigma \in Y\) satisfy \(\sigma(P_i) = Q_i\) for every \(i\).

public theorem_wanted fang_xia_partition_transitive_of_tiling
    {n : ℕ} {Y : Set (Equiv.Perm (Fin n))}
    (_h : IsTiling (transpositionsWithOne n) Y) :
    ∀ lam : PartitionShape n, 0 ≤ lam.contentSum → IsPartitionTransitive Y lam

Sources

• T. Fang and B. Xia, 'Tiling the symmetric group by transpositions', Bull. London Math. Soc. 58(5) (2026); DOI 10.1112/blms.70366; arXiv:2506.00360. The λ-transitivity notion in the statement is due to Martin–Sagan. Problem fang_xia_tiling_partition_transitive of the lean-eval benchmark.

Uses 5

Statement usesλ-transitive sets of permutations · Tiling of a group by two subsets · Integer partition as a list of row lengths · Twice the content sum of a partition · The identity and the transpositions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.