Melody Chan's theorem on distinguishing GL_n(F)

For a field F, infinite or finite with |F| > n + 1, the vectors of Fⁿ can be coloured Green or Blue so that every invertible n × n matrix other than the identity sends some Green vector to a Blue one (Theorem of the Day; Chan 2006). Construction: take α with α^r ≠ 1 for 1 ≤ r ≤ n (a generator of F^×, or an element avoiding the roots of unity of order ≤ n), and colour Blue the vectors α^i e_j, 0 ≤ i < j ≤ n; a matrix preserving this set fixes every basis vector.

Main results

• Chan.blue_stable_eq_one: an invertible matrix preserving Chan Blue set is the identity
• Chan.exists_blue: Chan: a Green/Blue colouring of Fⁿ that no non-identity invertible matrix respects

References

• R. Whitty, Theorem of the Day, «A Theorem of Melody Chan on Group Actions» (GroupTheory/MChan).
• M. Chan, The maximum distinguishing number of a group, Electron. J. Combin. 13 (2006) R70.

theorem Chan.exists_alpha (F : Type u_1) [Field F] (n : ℕ) (hF : Infinite F ∨ ∃ (x : Fintype F), n + 1 < Fintype.card F) : ∃ (α : F), α ≠ 0 ∧ ∀ (r : ℕ), 1 ≤ r → r ≤ n → α ^ r ≠ 1

Existence of α of multiplicative order > n.

def Chan.Blue (F : Type u_1) [Field F] (n : ℕ) (α : F) : Set (Fin n → F)

The Blue set.

Equations

• Chan.Blue F n α = {v : Fin n → F | ∃ (j : Fin n), ∃ i < ↑j + 1, v = Pi.single j (α ^ i)}

theorem Chan.single_inj {F : Type u_1} [Field F] {n : ℕ} {j j' : Fin n} {a b : F} (ha : a ≠ 0) (h : Pi.single j a = Pi.single j' b) : j = j' ∧ a = b

theorem Chan.pow_inj {F : Type u_1} [Field F] {n : ℕ} {α : F} (hα : ∀ (r : ℕ), 1 ≤ r → r ≤ n → α ^ r ≠ 1) (h0 : α ≠ 0) {r i : ℕ} (hr : r ≤ n) (hi : i ≤ n) (h : α ^ r = α ^ i) : r = i

theorem Chan.single_mem_iff {F : Type u_1} [Field F] {n : ℕ} {α : F} (hα : ∀ (r : ℕ), 1 ≤ r → r ≤ n → α ^ r ≠ 1) (h0 : α ≠ 0) (j : Fin n) {r : ℕ} (hr : r ≤ n) : Pi.single j (α ^ r) ∈ Blue F n α ↔ r < ↑j + 1

theorem Chan.inv_not_mem {F : Type u_1} [Field F] {n : ℕ} {α : F} (hα : ∀ (r : ℕ), 1 ≤ r → r ≤ n → α ^ r ≠ 1) (h0 : α ≠ 0) (j : Fin n) : Pi.single j α⁻¹ ∉ Blue F n α

theorem Chan.smul_single {F : Type u_1} [Field F] {n : ℕ} (j : Fin n) (c a : F) : c • Pi.single j a = Pi.single j (c * a)

theorem Chan.smul_single_one {F : Type u_1} [Field F] {n : ℕ} (j : Fin n) (a : F) : a • Pi.single j 1 = Pi.single j a

theorem Chan.mulVec_single_smul {F : Type u_1} [Field F] {n : ℕ} (B : Matrix (Fin n) (Fin n) F) (k : Fin n) (a : F) : B.mulVec (Pi.single k a) = a • B.mulVec (Pi.single k 1)

theorem Chan.blue_stable_eq_one {F : Type u_1} [Field F] {n : ℕ} {α : F} (hα : ∀ (r : ℕ), 1 ≤ r → r ≤ n → α ^ r ≠ 1) (h0 : α ≠ 0) (B : GL (Fin n) F) (hB : ∀ (v : Fin n → F), v ∈ Blue F n α ↔ (↑B).mulVec v ∈ Blue F n α) : B = 1

An invertible matrix preserving the Blue set is the identity.

theorem Chan.blue_finite (F : Type u_2) [Field F] (n : ℕ) (α : F) : (Blue F n α).Finite

theorem Chan.exists_blue (F : Type u_1) [Field F] (n : ℕ) (hF : Infinite F ∨ ∃ (x : Fintype F), n + 1 < Fintype.card F) : ∃ (Blue : Set (Fin n → F)), ∀ (B : GL (Fin n) F), B ≠ 1 → ∃ v ∉ Blue, (↑B).mulVec v ∈ Blue

Melody Chan's theorem. Let F be a field, infinite or finite with |F| > n + 1. Then the vectors of Fⁿ can be coloured Green or Blue (Blue a set, Green its complement) so that for every invertible n × n matrix B other than the identity there is a Green vector v with B v Blue.