Highly homogeneous permutation groups

DefinitionStrict betweenness#✓fully proved

Let \(\alpha\) be a type with a relation \(<\) and let \(a, b, c \in \alpha\). Then \(b\) lies strictly between \(a\) and \(c\) when either \(a < b\) and \(b < c\), or \(c < b\) and \(b < a\).

def isBetween (α : Type*) [LT α] (a b c : α) : Prop :=
  (a < b ∧ b < c) ∨ (c < b ∧ b < a)
Used by 2
Used byThe betweenness automorphism group of a linear order · The betweenness group of the rationals is closed and highly homogeneous

DefinitionThe betweenness automorphism group of a linear order#✓fully proved

Let \(\alpha\) be a linearly ordered set, and say that \(b\) lies strictly between \(a\) and \(c\) when \(a < b < c\) or \(c < b < a\). The betweenness automorphism group of \(\alpha\) is the subgroup of the group of permutations of \(\alpha\) consisting of the permutations \(\sigma\) such that, for all \(a, b, c \in \alpha\), \(b\) lies strictly between \(a\) and \(c\) if and only if \(\sigma(b)\) lies strictly between \(\sigma(a)\) and \(\sigma(c)\).

def betweennessAutSubgroup (α : Type*) [LinearOrder α] : Subgroup (Equiv.Perm α) where
  carrier := { σ | ∀ a b c : α, isBetween α a b c ↔ isBetween α (σ a) (σ b) (σ c) }
  mul_mem' := by
    intro σ τ hσ hτ a b c
    change isBetween α a b c ↔
      isBetween α (σ (τ a)) (σ (τ b)) (σ (τ c))
    exact (hτ a b c).trans (hσ (τ a) (τ b) (τ c))
  one_mem' := by
    intro a b c
    simp [Equiv.Perm.coe_one, isBetween]
  inv_mem' := by
    intro σ hσ a b c
    have h := hσ (σ⁻¹ a) (σ⁻¹ b) (σ⁻¹ c)
    simpa only [Equiv.Perm.coe_inv, Equiv.apply_symm_apply] using h.symm
Uses 1 · Used by 1
Statement usesStrict betweenness
Used byThe betweenness group of the rationals is closed and highly homogeneous

DefinitionThe automorphism group of a circular order#✓fully proved

Let \(\alpha\) be a circularly ordered set with non-strict circular betweenness relation \(\operatorname{btw}\). The automorphism group of \(\alpha\) is the subgroup of the group of permutations of \(\alpha\) consisting of the permutations \(\sigma\) such that, for all \(a, b, c \in \alpha\), \(\operatorname{btw}(a, b, c)\) holds if and only if \(\operatorname{btw}(\sigma(a), \sigma(b), \sigma(c))\) holds.

def circularOrderAutSubgroup (α : Type*) [CircularOrder α] : Subgroup (Equiv.Perm α) where
  carrier := {σ | ∀ a b c, btw a b c ↔ btw (σ a) (σ b) (σ c)}
  one_mem' a b c := by simp
  mul_mem' {σ τ} hσ hτ a b c := by
    simp only [Equiv.Perm.coe_mul, Function.comp_apply]
    exact (hτ a b c).trans (hσ _ _ _)
  inv_mem' {σ} hσ a b c := by
    have h := (hσ (σ⁻¹ a) (σ⁻¹ b) (σ⁻¹ c)).symm
    simpa [Equiv.apply_symm_apply] using h
Used by 2
Used byThe automorphism group of a countably infinite dense circular order is closed and highly homogeneous · The separation group of a countably infinite dense circular order is closed and highly homogeneous

DefinitionHighly homogeneous permutation groups#✓fully proved

Let \(G\) be a group of permutations of a set \(\alpha\). Then \(G\) is highly homogeneous when, for every natural number \(k\), it acts transitively on the \(k\)-element subsets of \(\alpha\): for any two \(k\)-element subsets \(X\) and \(Y\) of \(\alpha\) there is some \(g \in G\) with \(g(X) = Y\).

def IsHighlyHomogeneous {α : Type*} [DecidableEq α]
    (G : Subgroup (Equiv.Perm α)) : Prop :=
  ∀ k : ℕ, MulAction.IsPretransitive G ↑(Set.powersetCard α k)
Used by 6
Used byThe betweenness group of the rationals is closed and highly homogeneous · The symmetric group of the rationals is closed and highly homogeneous · The automorphism group of a countably infinite dense circular order is closed and highly homogeneous · The full symmetric group is highly homogeneous · The order-automorphism group of the rationals is closed and highly homogeneous · The separation group of a countably infinite dense circular order is closed and highly homogeneous

TheoremThe full symmetric group is highly homogeneous#✓fully proved

For every set \(\alpha\), the group of all permutations of \(\alpha\) is highly homogeneous: for every natural number \(k\), any \(k\)-element subset of \(\alpha\) can be carried to any other \(k\)-element subset of \(\alpha\) by some permutation of \(\alpha\).

theorem isHighlyHomogeneous_top {α : Type*} [DecidableEq α] :
    IsHighlyHomogeneous (⊤ : Subgroup (Equiv.Perm α))
Uses 1 · Used by 1
Statement usesHighly homogeneous permutation groups
Used byThe symmetric group of the rationals is closed and highly homogeneous

DefinitionOrder automorphism group#✓fully proved

For a type \(\alpha\) equipped with a relation \(<\), the order automorphism group of \(\alpha\) is the subgroup of the group of permutations of \(\alpha\) consisting of the permutations \(\sigma\) such that for all \(a, b \in \alpha\), \(a < b\) holds if and only if \(\sigma(a) < \sigma(b)\) holds.

def orderAutSubgroup (α : Type*) [LT α] : Subgroup (Equiv.Perm α) where
  carrier := {σ | ∀ a b, a < b ↔ σ a < σ b}
  one_mem' a b := by simp
  mul_mem' hσ hτ a b := (hτ a b).trans (hσ _ _)
  inv_mem' {σ} h a b := by simpa using (h (σ⁻¹ a) (σ⁻¹ b)).symm
Used by 1
Used byThe order-automorphism group of the rationals is closed and highly homogeneous

AbbreviationPointwise convergence topology on permutations#✓fully proved

For a type \(\alpha\), the pointwise convergence topology on the group of permutations of \(\alpha\) is the topology induced by the map sending a permutation \(\sigma\) to the underlying function \(\sigma \colon \alpha \to \alpha\), where \(\alpha\) carries the discrete topology and the space of functions \(\alpha \to \alpha\) carries the product topology.

noncomputable abbrev pointwiseTopology {α : Type*} : TopologicalSpace (Equiv.Perm α) :=
  letI : TopologicalSpace α := ⊥
  TopologicalSpace.induced (fun σ : Equiv.Perm α => ⇑σ) inferInstance
Used by 7
Used byClaim of Kourovka Problem 13.28 · Kourovka Problem 19.89: Smith's conjecture on distinguishing sets · The betweenness group of the rationals is closed and highly homogeneous · The symmetric group of the rationals is closed and highly homogeneous · The automorphism group of a countably infinite dense circular order is closed and highly homogeneous · The order-automorphism group of the rationals is closed and highly homogeneous · The separation group of a countably infinite dense circular order is closed and highly homogeneous

TheoremThe betweenness group of the rationals is closed and highly homogeneous#✓fully proved

Let \(G\) be the group of permutations \(\sigma\) of \(\mathbb{Q}\) preserving strict betweenness in both directions: for all \(a, b, c \in \mathbb{Q}\), \(b\) lies strictly between \(a\) and \(c\) (that is, \(a < b < c\) or \(c < b < a\)) if and only if \(\sigma(b)\) lies strictly between \(\sigma(a)\) and \(\sigma(c)\). Then \(G\) is closed in the topology of pointwise convergence on the permutations of \(\mathbb{Q}\), where \(\mathbb{Q}\) carries the discrete topology, and \(G\) is highly homogeneous: for every natural number \(k\) it has a single orbit on the \(k\)-element subsets of \(\mathbb{Q}\).

theorem betweennessAutSubgroup_isClosed_and_highlyHomogeneous :
    @IsClosed (Equiv.Perm ℚ) (Equiv.Perm.pointwiseTopology (α := ℚ))
      ↑(betweennessAutSubgroup ℚ) ∧
    IsHighlyHomogeneous (betweennessAutSubgroup ℚ)
Sources
  • Daniele A. Gewurz and Francesca Merola, "Sequences realized as Parker vectors of oligomorphic permutation groups," Journal of Integer Sequences 6, https://cs.uwaterloo.ca/journals/JIS/VOL6/Gewurz/gewurz22.tex, lines 331–359. The source identifies B (also ∂C*) as the rational-order permutations preserving or reversing order and calls Cameron's five representatives closed and highly homogeneous, glossed as one orbit on k-sets for all k. The source cites Peter J. Cameron, "Transitivity of permutation groups on unordered sets," Math. Z. 148 (1976), 127–139. Interpretation boundary: only the B representative is asserted, not exhaustive classification, uniqueness, or conjugacy.
Uses 4
Statement usesPointwise convergence topology on permutations · Highly homogeneous permutation groups · The betweenness automorphism group of a linear order
Proof usesStrict betweenness

TheoremThe automorphism group of a countably infinite dense circular order is closed and highly homogeneous#✓fully proved

The automorphism group of a countably infinite dense circular order is closed and highly homogeneous. Let \(\alpha\) be a countably infinite set with a circular order, and write \(\operatorname{btw}(a, b, c)\) when \(b\) lies between \(a\) and \(c\) going around from \(a\) to \(c\). Suppose the circular order is dense: for all distinct \(a, b \in \alpha\) there is some \(c \in \alpha\), different from \(a\) and \(b\), with \(\operatorname{btw}(a, c, b)\). Then the group of permutations \(\sigma\) of \(\alpha\) such that \(\operatorname{btw}(a, b, c)\) holds if and only if \(\operatorname{btw}(\sigma(a), \sigma(b), \sigma(c))\) holds, for all \(a, b, c \in \alpha\), is closed in the topology of pointwise convergence on the permutations of \(\alpha\), where \(\alpha\) carries the discrete topology, and it is highly homogeneous: for every natural number \(k\) it has a single orbit on the \(k\)-element subsets of \(\alpha\).

theorem circularOrderAutSubgroup_isClosed_and_highlyHomogeneous
    {α : Type*} [DecidableEq α] [Countable α] [Infinite α] [CircularOrder α]
    (hdense : ∀ a b : α, a ≠ b → ∃ c : α, c ≠ a ∧ c ≠ b ∧ btw a c b) :
    @IsClosed (Equiv.Perm α) (Equiv.Perm.pointwiseTopology (α := α))
      ↑(MetaMathlibExt.circularOrderAutSubgroup α) ∧
      MetaMathlibExt.IsHighlyHomogeneous (MetaMathlibExt.circularOrderAutSubgroup α)
Sources
  • Daniele A. Gewurz and Francesca Merola, "Sequences realized as Parker vectors of oligomorphic permutation groups," JIS 6, https://cs.uwaterloo.ca/journals/JIS/VOL6/Gewurz/gewurz22.tex, lines 331–359. Interpretation boundary: only Cameron group C is asserted, with standard countable dense infinite circular-order hypotheses, not exhaustive classification, uniqueness, or conjugacy.
Uses 3 · Used by 1
Statement usesPointwise convergence topology on permutations · Highly homogeneous permutation groups · The automorphism group of a circular order
Used byThe separation group of a countably infinite dense circular order is closed and highly homogeneous

TheoremThe order-automorphism group of the rationals is closed and highly homogeneous#✓fully proved

The group of order automorphisms of \(\mathbb{Q}\), that is, of the permutations \(\sigma\) of \(\mathbb{Q}\) such that \(a < b\) if and only if \(\sigma(a) < \sigma(b)\) for all \(a, b \in \mathbb{Q}\), is closed in the topology of pointwise convergence on the permutations of \(\mathbb{Q}\), where \(\mathbb{Q}\) carries the discrete topology, and it is highly homogeneous: for every natural number \(k\) it has a single orbit on the \(k\)-element subsets of \(\mathbb{Q}\).

theorem orderAutSubgroup_isClosed_and_highlyHomogeneous :
    @IsClosed (Equiv.Perm ℚ) (Equiv.Perm.pointwiseTopology (α := ℚ))
      ↑(MetaMathlibExt.orderAutSubgroup ℚ) ∧
      MetaMathlibExt.IsHighlyHomogeneous (MetaMathlibExt.orderAutSubgroup ℚ)
Sources
  • Daniele A. Gewurz and Francesca Merola, "Sequences realized as Parker vectors of oligomorphic permutation groups," JIS 6, https://cs.uwaterloo.ca/journals/JIS/VOL6/Gewurz/gewurz22.tex, lines 331-359. Primary source, cited there: Peter J. Cameron, "Transitivity of permutation groups on unordered sets," Mathematische Zeitschrift 148(2) (1976), 127--139, DOI 10.1007/BF01214702.
Uses 3
Statement usesPointwise convergence topology on permutations · Highly homogeneous permutation groups · Order automorphism group

TheoremThe symmetric group of the rationals is closed and highly homogeneous#✓fully proved

Let \(\operatorname{Sym}(\mathbb{Q})\) be the group of all permutations of the set \(\mathbb{Q}\). Then \(\operatorname{Sym}(\mathbb{Q})\) is closed in the topology of pointwise convergence on the permutations of \(\mathbb{Q}\), and it is highly homogeneous: for every natural number \(k\) it has a single orbit on the \(k\)-element subsets of \(\mathbb{Q}\).

Here \(\mathbb{Q}\) serves only as a countably infinite set; its order, its field structure and its usual topology play no role.

public theorem cameron_symmetricGroup_closed_highlyHomogeneous :
    @IsClosed (Equiv.Perm ℚ) (Equiv.Perm.pointwiseTopology (α := ℚ))
        (↑(⊤ : Subgroup (Equiv.Perm ℚ)) : Set (Equiv.Perm ℚ)) ∧
      IsHighlyHomogeneous (⊤ : Subgroup (Equiv.Perm ℚ))
Sources
  • Daniele A. Gewurz and Francesca Merola, Sequences realized as Parker vectors of oligomorphic permutation groups, Journal of Integer Sequences 6, source lines 331--359 at https://cs.uwaterloo.ca/journals/JIS/VOL6/Gewurz/gewurz22.tex. Peter J. Cameron, "Transitivity of permutation groups on unordered sets," Mathematische Zeitschrift 148(2) (1976), 127--139, DOI 10.1007/BF01214702. Scope: this proves only Cameron's representative S, not Cameron's exhaustive classification, uniqueness, conjugacy, Parker-sequence claims, or the other four representatives.
Uses 3
Statement usesPointwise convergence topology on permutations · Highly homogeneous permutation groups
Proof usesThe full symmetric group is highly homogeneous

DefinitionSeparation of pairs in a circular order#✓fully proved

Let \(\alpha\) be a circular order, and write \(\operatorname{sbtw}(x, y, z)\) for its strict betweenness relation (\(y\) lies strictly between \(x\) and \(z\) going around the circle). For \(a, b, c, d \in \alpha\), the pairs \(a, b\) and \(c, d\) separate each other when either \(\operatorname{sbtw}(a, c, b)\) and \(\operatorname{sbtw}(b, d, a)\) both hold, or \(\operatorname{sbtw}(a, d, b)\) and \(\operatorname{sbtw}(b, c, a)\) both hold.

def circularSeparates {α : Type*} [CircularOrder α] (a b c d : α) : Prop :=
  (sbtw a c b ∧ sbtw b d a) ∨ (sbtw a d b ∧ sbtw b c a)
Used by 2
Used bySeparation-preserving permutation group · The separation group of a countably infinite dense circular order is closed and highly homogeneous

DefinitionSeparation-preserving permutation group#✓fully proved

For a circular order \(\alpha\), the separation-preserving group of \(\alpha\) is the subgroup of the group of permutations of \(\alpha\) consisting of the permutations \(\sigma\) such that for all \(a, b, c, d \in \alpha\), the pairs \(a, b\) and \(c, d\) separate each other if and only if the pairs \(\sigma(a), \sigma(b)\) and \(\sigma(c), \sigma(d)\) separate each other.

def separationAutSubgroup (α : Type*) [CircularOrder α] : Subgroup (Equiv.Perm α) where
  carrier :=
    {σ | ∀ a b c d, circularSeparates a b c d ↔
      circularSeparates (σ a) (σ b) (σ c) (σ d)}
  one_mem' a b c d := by simp
  mul_mem' {σ τ} hσ hτ a b c d := by
    simp only [Equiv.Perm.coe_mul, Function.comp_apply]
    exact (hτ a b c d).trans (hσ _ _ _ _)
  inv_mem' {σ} hσ a b c d := by
    have h := (hσ (σ⁻¹ a) (σ⁻¹ b) (σ⁻¹ c) (σ⁻¹ d)).symm
    simpa [Equiv.apply_symm_apply] using h
Uses 1 · Used by 1
Statement usesSeparation of pairs in a circular order
Used byThe separation group of a countably infinite dense circular order is closed and highly homogeneous

TheoremThe separation group of a countably infinite dense circular order is closed and highly homogeneous#✓fully proved

The separation group of a countably infinite dense circular order is closed and highly homogeneous. Let \(\alpha\) be a countably infinite set with a circular order, and write \(\operatorname{btw}(a, b, c)\) when \(b\) lies between \(a\) and \(c\) going around from \(a\) to \(c\). Suppose the circular order is dense: for all distinct \(a, b \in \alpha\) there is some \(c \in \alpha\), different from \(a\) and \(b\), with \(\operatorname{btw}(a, c, b)\). Then the separation automorphism group of \(\alpha\) is closed in the topology of pointwise convergence on the permutations of \(\alpha\), where \(\alpha\) carries the discrete topology, and it is highly homogeneous: for every natural number \(k\) it has a single orbit on the \(k\)-element subsets of \(\alpha\).

public theorem separationAutSubgroup_isClosed_and_highlyHomogeneous
    {α : Type*} [DecidableEq α] [Countable α] [Infinite α] [CircularOrder α]
    (hdensity : ∀ a b : α, a ≠ b → ∃ c : α, btw a c b ∧ c ≠ a ∧ c ≠ b) :
    @IsClosed (Equiv.Perm α) (Equiv.Perm.pointwiseTopology (α := α))
        (↑(separationAutSubgroup α) : Set (Equiv.Perm α)) ∧
      IsHighlyHomogeneous (separationAutSubgroup α)
Sources
  • Daniele A. Gewurz and Francesca Merola, "Sequences realized as Parker vectors of oligomorphic permutation groups," Journal of Integer Sequences 6, https://cs.uwaterloo.ca/journals/JIS/VOL6/Gewurz/gewurz22.tex, lines 331–359. The source identifies D (also C*) as the cyclic-order permutations preserving or reversing the order and calls Cameron's five representatives closed and highly homogeneous, glossed as one orbit on k-sets for all k. The source cites Peter J. Cameron, "Transitivity of permutation groups on unordered sets," Math. Z. 148 (1976), 127–139. Interpretation boundary: only the D representative is asserted, not exhaustive classification, uniqueness, or conjugacy. The explicit countability, infinitude, and circular-density hypotheses select the intended countable dense circular order.
Uses 6
Statement usesPointwise convergence topology on permutations · Highly homogeneous permutation groups · Separation-preserving permutation group
Proof usesThe automorphism group of a countably infinite dense circular order is closed and highly homogeneous · The automorphism group of a circular order · Separation of pairs in a circular order
14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.