Groups as automorphism groups of relations

DefinitionFull automorphism group of a binary relation#✓fully proved

Let \(G\) be a group, \(Z\) a set and \(X \subseteq Z \times Z\) a binary relation on \(Z\). Then \(G\) is the full automorphism group of \(X\) when there is an injective group homomorphism \(\varphi\) from \(G\) to the group of permutations of \(Z\) whose image is exactly the set of permutations \(f\) of \(Z\) with \((x, y) \in X \iff (f(x), f(y)) \in X\) for all \(x, y \in Z\).

def IsAutomorphismGroupOf (G : Type u) [Group G] (Z : Type u) (X : Set (Z × Z)) :
    Prop :=
  ∃ φ : G → Equiv.Perm Z, Function.Injective φ ∧
    (∀ g h : G, φ (g * h) = φ g * φ h) ∧
    (∀ g : G, ∀ x y : Z, (x, y) ∈ X ↔ (φ g x, φ g y) ∈ X) ∧
    ∀ f : Equiv.Perm Z, (∀ x y : Z, (x, y) ∈ X ↔ (f x, f y) ∈ X) → ∃ g : G, φ g = f

Used by 1

Used byBirkhoff's theorem: every group is the automorphism group of a binary relation

TheoremBirkhoff's theorem: every group is the automorphism group of a binary relation#●ready to prove

For every group \(G\) there are a set \(Z\) and a binary relation \(X \subseteq Z \times Z\) such that \(G\) is the full automorphism group of \(X\): there is an injective group homomorphism \(\varphi\) from \(G\) to the group of permutations of \(Z\) whose image is exactly the set of permutations \(f\) of \(Z\) with \((x, y) \in X \iff (f(x), f(y)) \in X\) for all \(x, y \in Z\).

The set \(Z\) lies in the same universe as \(G\).

theorem_wanted everyGroupIsAutomorphismGroupOfBinaryRelation :
    ∀ (G : Type u) [Group G], ∃ (Z : Type u) (X : Set (Z × Z)),
      IsAutomorphismGroupOf G Z X

Sources

• S. Ulam, Problem 142 of the Scottish Book, headed "Problem (Ulam) - Theorem (Garrett Birkhoff)"; the representation is Birkhoff's theorem.

Uses 1

Statement usesFull automorphism group of a binary relation

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.