Limit Laws and Automorphism Groups of Nonrigid Structures

Ove Ahlman and Vera Koponen

The first sentence of the introduction reads as follows.

"[...] it has been shown that for any finite relational vocabulary (also called signature), the proportion of labelled n-element structures which are rigid, ie have no nontrivial automorphism, approaches 1 as n approaches infinity"

While their paper is about nonrigid structures, here we show that there exists a rigid 2-element structure, namely Fin 2 under addition.

def automorphism_of_fin_2 (f : Fin 2 → Fin 2) : Prop

Equations

• automorphism_of_fin_2 f = (Function.Bijective f ∧ ∀ (x y : Fin 2), f x + f y = f (x + y))

theorem fin2 (x : Fin 2) : x = 0 ∨ x = 1

theorem fin2_rigid (f : Fin 2 → Fin 2) (hf : automorphism_of_fin_2 f) : f = id

Fin 2 is rigid as an additive structure.

def automorphism_of_fin_k (k : ℕ) (f : Fin k → Fin k) : Prop

Equations

• automorphism_of_fin_k k f = (Function.Bijective f ∧ ∀ (x y : Fin k), f x + f y = f (x + y))

def is_rigid (k : ℕ) : Prop

Equations

• is_rigid k = ∀ (g : Fin k → Fin k), automorphism_of_fin_k k g → g = id