Permutation stability

DefinitionNormalized Hamming distance#✓fully proved

For a natural number \(n\) and permutations \(\sigma\), \(\tau\) of \(\{0, \dots, n-1\}\), the normalized Hamming distance \(d_n(\sigma, \tau)\) is the number of points \(i < n\) with \(\sigma(i) \ne \tau(i)\), divided by \(n\), as a real number. For \(n = 0\) it is \(0\); this single value does not affect statements about limits as \(n \to \infty\).

noncomputable def normalizedHammingDistance (n : ℕ) (σ τ : Equiv.Perm (Fin n)) : ℝ :=
  (hammingDist (fun i => σ i) (fun i => τ i) : ℝ) / n

Used by 2

Used byAlmost-homomorphisms to symmetric groups · Closeness to homomorphisms

DefinitionAlmost-homomorphisms to symmetric groups#✓fully proved

Let \(G\) be a group and, for each natural number \(n\), let \(f_n \colon G \to S_n\) be an arbitrary map, where \(S_n\) is the group of permutations of \(\{0, \dots, n-1\}\). The sequence \((f_n)\) is an almost-homomorphism when for all \(g, h \in G\) the normalized Hamming distance \(d_n(f_n(g) f_n(h), f_n(gh))\) tends to \(0\) as \(n \to \infty\).

Following the source, no condition such as \(f_n(1) = 1\) is imposed.

def IsAlmostHomomorphism {G : Type*} [Group G]
    (f : ∀ n : ℕ, G → Equiv.Perm (Fin n)) : Prop :=
  ∀ g h : G, Filter.Tendsto
    (fun n => normalizedHammingDistance n (f n g * f n h) (f n (g * h)))
    Filter.atTop (nhds 0)

Uses 1 · Used by 2

Statement usesNormalized Hamming distance

Used byFlexible permutation stability · Permutation stability

DefinitionCloseness to homomorphisms#✓fully proved

Let \(G\) be a group and let \(f_n \colon G \to S_n\) (\(n \in \mathbb{N}\)) be maps into the symmetric groups \(S_n\) of permutations of \(\{0, \dots, n-1\}\). The sequence \((f_n)\) is close to homomorphisms when there are group homomorphisms \(\rho_n \colon G \to S_n\) such that for every \(g \in G\) the normalized Hamming distance \(d_n(\rho_n(g), f_n(g))\) tends to \(0\) as \(n \to \infty\).

def IsCloseToHomomorphisms {G : Type*} [Group G]
    (f : ∀ n : ℕ, G → Equiv.Perm (Fin n)) : Prop :=
  ∃ ρ : ∀ n : ℕ, G →* Equiv.Perm (Fin n), ∀ g : G, Filter.Tendsto
    (fun n => normalizedHammingDistance n (ρ n g) (f n g))
    Filter.atTop (nhds 0)

Uses 1 · Used by 1

Statement usesNormalized Hamming distance

Used byPermutation stability

DefinitionPermutation stability#✓fully proved

A group \(G\) is permutation stable when every almost-homomorphism \((f_n)\) from \(G\) to the symmetric groups \(S_n\) is close to homomorphisms.

def PermutationStable (G : Type*) [Group G] : Prop :=
  ∀ f : ∀ n : ℕ, G → Equiv.Perm (Fin n),
    IsAlmostHomomorphism f → IsCloseToHomomorphisms f

Uses 2

Statement usesAlmost-homomorphisms to symmetric groups · Closeness to homomorphisms

DefinitionFlexible Hamming distance#✓fully proved

Let \(n \le m\) be natural numbers, \(\sigma\) a permutation of \(\{0, \dots, n-1\}\) and \(\tau\) a permutation of \(\{0, \dots, m-1\}\). The flexible Hamming distance of \(\sigma\) and \(\tau\) is the real number

\[ d^{\mathrm{flex}}_n(\sigma, \tau) = \frac{\#\{i < n : \sigma(i) \ne \tau(i)\} + (m - n)}{n}. \]

For \(n = 0\) this quotient is taken to be \(0\); this single value does not affect statements about limits as \(n \to \infty\).

noncomputable def flexibleHammingDistance {n m : ℕ} (h : n ≤ m)
    (σ : Equiv.Perm (Fin n)) (τ : Equiv.Perm (Fin m)) : ℝ :=
  ((hammingDist (fun i => Fin.castLE h (σ i))
      (fun i => τ (Fin.castLE h i)) + (m - n) : ℕ) : ℝ) / n

Sources

• Kourovka Notebook 21.84. The source is internally inconsistent about the argument order: it first defines the distance with the small permutation first, d_n^flex(σ, τ) for σ ∈ S_n, τ ∈ S_m, but later writes the convergence expression with ρ_n(g) first. This formalization follows the definition site (small first), which is also the type-correct order for the embedding Fin n → Fin m.

Used by 1

Used byFlexible closeness to homomorphisms

DefinitionFlexible closeness to homomorphisms#✓fully proved

Let \(G\) be a group and let \(f_n \colon G \to S_n\) (\(n \in \mathbb{N}\)) be maps into the symmetric groups \(S_n\) of permutations of \(\{0, \dots, n-1\}\). The sequence \((f_n)\) is flexibly close to homomorphisms when there are natural numbers \(m_n \ge n\) and group homomorphisms \(\rho_n \colon G \to S_{m_n}\) such that for every \(g \in G\) the flexible Hamming distance \(d^{\mathrm{flex}}_n(f_n(g), \rho_n(g))\) tends to \(0\) as \(n \to \infty\).

def IsFlexiblyCloseToHomomorphisms {G : Type*} [Group G]
    (f : ∀ n : ℕ, G → Equiv.Perm (Fin n)) : Prop :=
  ∃ m : ℕ → ℕ, ∃ h : ∀ n : ℕ, n ≤ m n,
    ∃ ρ : ∀ n : ℕ, G →* Equiv.Perm (Fin (m n)), ∀ g : G, Filter.Tendsto
      (fun n => flexibleHammingDistance (h n) (f n g) (ρ n g))
      Filter.atTop (nhds 0)

Uses 1 · Used by 1

Statement usesFlexible Hamming distance

Used byFlexible permutation stability

DefinitionFlexible permutation stability#✓fully proved

A group \(G\) is flexibly permutation stable when every almost-homomorphism \((f_n)\) from \(G\) to the symmetric groups is flexibly close to homomorphisms.

def FlexiblePermutationStable (G : Type*) [Group G] : Prop :=
  ∀ f : ∀ n : ℕ, G → Equiv.Perm (Fin n),
    IsAlmostHomomorphism f → IsFlexiblyCloseToHomomorphisms f

Uses 2

Statement usesAlmost-homomorphisms to symmetric groups · Flexible closeness to homomorphisms

DefinitionMetabelian groups#✓fully proved

Let \(G\) be a group and let \(G' = [G, G]\) be its commutator subgroup. Then \(G\) is metabelian when its second derived subgroup \(G'' = [G', G']\) is trivial.

def Metabelian (G : Type*) [Group G] : Prop :=
  derivedSeries G 2 = ⊥

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.