Distinguishing numbers of group actions

A coloring c : X → Fin k of a G-set X is distinguishing if the identity is the only element of G preserving it, and the distinguishing number is the least such k. This file develops the basic API and computes the distinguishing number of the collineation group of the Fano plane acting on its seven points: it is 4. The values are those of Klavžar, Wong and Zhu; the lower bound checks all 3⁷ colorings against a list of 21 involutions with decide, and the upper bound is a structural argument from the lines.

Main definitions

• TotD.IsDistinguishing, TotD.distinguishingNumber.
• TotD.fanoGroup: the stabilizer of the seven lines of the Fano plane in Equiv.Perm (Fin 7).

Main results

• TotD.IsDistinguishing.mono, TotD.distinguishingNumber_le_card, TotD.distinguishingNumber_le_card_base_add_one: monotonicity, D ≤ #X for faithful actions, D ≤ b + 1 for a base of size b.
• TotD.fano_not_isDistinguishing_two, TotD.fano_not_isDistinguishing_three, TotD.fanoColoring_isDistinguishing.
• TotD.fano_distinguishingNumber: distinguishingNumber fanoGroup (Fin 7) = 4.

References

• M. O. Albertson, K. L. Collins, Symmetry breaking in graphs, Electron. J. Combin. 3 (1996) R18.
• S. Klavžar, T.-L. Wong, X. Zhu, Distinguishing labellings of group action on vector spaces and graphs, J. Algebra 303 (2006) 626–641.

Distinguishing colorings and the distinguishing number, in general

def TotD.IsDistinguishing (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] {k : ℕ} (c : X → Fin k) : Prop

A coloring c : X → Fin k is distinguishing for the action of G on X if the only g : G preserving the coloring is the identity (Albertson–Collins 1996; Tymoczko 2004 for arbitrary group actions).

Equations

• TotD.IsDistinguishing G c = ∀ (g : G), (∀ (x : X), c (g • x) = c x) → g = 1

noncomputable def TotD.distinguishingNumber (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] : ℕ

The distinguishing number D(G ↷ X): the least number of colors admitting a distinguishing coloring (sInf, so 0 if no coloring distinguishes — e.g. an unfaithful action of a nontrivial group on a finite set).

Equations

• TotD.distinguishingNumber G X = sInf {k : ℕ | ∃ (c : X → Fin k), TotD.IsDistinguishing G c}

theorem TotD.IsDistinguishing.mono {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {k m : ℕ} (hkm : k ≤ m) {c : X → Fin k} (hc : IsDistinguishing G c) : IsDistinguishing G fun (x : X) => ⟨↑(c x), ⋯⟩

Monotonicity: a distinguishing k-coloring yields a distinguishing m-coloring for any m ≥ k (recolor through the inclusion Fin k ↪ Fin m).

theorem TotD.exists_isDistinguishing_mono {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {k m : ℕ} (hkm : k ≤ m) (h : ∃ (c : X → Fin k), IsDistinguishing G c) : ∃ (c : X → Fin m), IsDistinguishing G c

Existence form of monotonicity: the set of color counts admitting a distinguishing coloring is upward closed.

theorem TotD.distinguishingNumber_le {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {k : ℕ} {c : X → Fin k} (hc : IsDistinguishing G c) : distinguishingNumber G X ≤ k

A distinguishing k-coloring bounds the distinguishing number: D ≤ k.

theorem TotD.lt_distinguishingNumber {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {k m : ℕ} {c : X → Fin m} (hc : IsDistinguishing G c) (hnone : ∀ (c' : X → Fin k), ¬IsDistinguishing G c') : k < distinguishingNumber G X

Lower bound: if some coloring distinguishes (so the defining set is nonempty) but no k-coloring does, then k < D.

theorem TotD.distinguishingNumber_le_card {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [Fintype X] [FaithfulSMul G X] : distinguishingNumber G X ≤ Fintype.card X

A faithful action on a finite set is distinguished by the all-distinct coloring: D ≤ |X|.

theorem TotD.distinguishingNumber_le_card_base_add_one {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [DecidableEq X] (S : Finset X) (hS : ∀ (g : G), (∀ x ∈ S, g • x = x) → g = 1) : distinguishingNumber G X ≤ S.card + 1

Bases and distinguishing colorings: a base of size b — a finite set whose pointwise stabilizer is trivial — gives D ≤ b + 1: color the base points with b distinct nonzero colors and everything else with 0.

The Fano exception: D(GL(3,2) ↷ F₂³ \ {0}) = 4

Points 0, …, 6 : Fin 7 stand for the nonzero vectors of F₂³: point i is the vector whose binary digits are those of i + 1 (so 0 ↔ (1,0,0), 1 ↔ (0,1,0), 2 ↔ (1,1,0), 3 ↔ (0,0,1), 4 ↔ (1,0,1), 5 ↔ (0,1,1), 6 ↔ (1,1,1)). A triple is a line of the Fano plane iff the corresponding vectors sum to zero, and a permutation of the points is induced by a (unique) element of GL(3,2) iff it maps lines to lines.

def TotD.fanoLines : Finset (Finset (Fin 7))

The 7 lines of the Fano plane on Fin 7 (triples whose vectors XOR to zero).

Equations

• TotD.fanoLines = {{0, 1, 2}, {0, 3, 4}, {0, 5, 6}, {1, 3, 5}, {1, 4, 6}, {2, 3, 6}, {2, 4, 5}}

def TotD.fanoGroup : Subgroup (Equiv.Perm (Fin 7))

The collineation group of the Fano plane: the stabilizer in Equiv.Perm (Fin 7) of the line set. Abstractly GL(3,2) ≅ PSL(2,7), of order 168, in its natural action on the nonzero vectors of F₂³.

Equations

• TotD.fanoGroup = MulAction.stabilizer (Equiv.Perm (Fin 7)) TotD.fanoLines

@[instance_reducible]

instance TotD.instDecidablePredPermFinOfNatNatMemSubgroupFanoGroup : DecidablePred fun (x : Equiv.Perm (Fin 7)) => x ∈ fanoGroup

Equations

• TotD.instDecidablePredPermFinOfNatNatMemSubgroupFanoGroup g = decidable_of_iff (g • TotD.fanoLines = TotD.fanoLines) ⋯

def TotD.involPerm (v : Fin 7 → Fin 7) (h : ∀ (x : Fin 7), v (v x) = x) : Equiv.Perm (Fin 7)

Build an involutive permutation of Fin 7 from its vector of images.

Equations

• TotD.involPerm v h = { toFun := v, invFun := v, left_inv := h, right_inv := h }

def TotD.fanoWitnesses : List (Equiv.Perm (Fin 7))

21 involutions of fanoGroup (the transvections of GL(3,2)), listed in greedy cover order: every 3-coloring of the 7 points is preserved by at least one of them (fanoWitnesses_cover).

Equations

• One or more equations did not get rendered due to their size.

theorem TotD.fanoWitnesses_spec (p : Equiv.Perm (Fin 7)) : p ∈ fanoWitnesses → p ∈ fanoGroup ∧ ∃ (x : Fin 7), p x ≠ x

Every witness is a nontrivial element of the collineation group. Kernel decide (the p ∈ fanoGroup checks are nested-Finset line-set equalities, too heavy for the heartbeat-bounded elaborator; only 21 items, so the kernel handles them quickly).

theorem TotD.fanoWitnesses_cover (a b c d e f g : Fin 3) : ∃ p ∈ fanoWitnesses, ∀ (x : Fin 7), ![a, b, c, d, e, f, g] (p x) = ![a, b, c, d, e, f, g] x

Kernel-checked cover: each of the 3^7 = 2187 colorings of the Fano points is preserved by at least one of the 21 witnesses. This is the entire exhaustive content of "no 3-coloring distinguishes", packed into one plain decide.

theorem TotD.fano_not_isDistinguishing_three (c : Fin 7 → Fin 3) : ¬IsDistinguishing (↥fanoGroup) c

No 3-coloring of the Fano points is distinguishing (Klavžar–Wong–Zhu 2006 for GL(3,2)).

theorem TotD.fano_not_isDistinguishing_two (c : Fin 7 → Fin 2) : ¬IsDistinguishing (↥fanoGroup) c

No 2-coloring of the Fano points is distinguishing (so D ≥ 3; in fact D = 4).

def TotD.fanoColoring : Fin 7 → Fin 4

A distinguishing 4-coloring: points 0,1,2,3 share color 0, points 4,5,6 get the unique colors 1,2,3. In vector terms the color classes are {(1,0,0), (0,1,0), (1,1,0), (0,0,1)}, {(1,0,1)}, {(0,1,1)}, {(1,1,1)}.

Equations

• TotD.fanoColoring = ![0, 0, 0, 0, 1, 2, 3]

theorem TotD.fanoColoring_isDistinguishing : IsDistinguishing (↥fanoGroup) fanoColoring

The coloring (0,0,0,0,1,2,3) is distinguishing. Structural proof from the line geometry: the unique colors pin 4, 5, 6; the lines {2,4,5}, {0,5,6}, {1,4,6} are the unique lines through their two pinned points, so 2, 0, 1 are pinned; injectivity pins 3.

theorem TotD.fano_distinguishingNumber : distinguishingNumber (↥fanoGroup) (Fin 7) = 4

The Fano exception, machine-checked (Klavžar–Wong–Zhu, J. Algebra 303 (2006), Thm 3.1, the unique D = 4 case; answers part of Chan's Question 4): the distinguishing number of GL(3,2) ≅ PSL(2,7) acting on the 7 nonzero vectors of F₂³ — equivalently, of the collineation group of the Fano plane acting on its points — is exactly 4.