The Cameron–Fon-Der-Flaass IBIS theorem

For a permutation group G on a finite set Ω, the following are equivalent: all irredundant bases have the same size; irredundant bases are preserved by re-ordering; the irredundant bases are the bases of a matroid on Ω (Theorem of the Day; Cameron and Fon-Der-Flaass 1995). The key step: if P, b is an irredundant base and adding x to P shrinks its pointwise stabilizer, it shrinks it to 1 (otherwise P, x, b is an irredundant base whose re-ordering P, b, x is not), which gives the matroid basis exchange.

Main results

• IBIS.one_point_completion: under invariance by re-ordering, a point that shrinks the stabilizer of a near-base completes it
• IBIS.exchange: basis exchange for the underlying sets of irredundant bases
• IBIS.tfae: the IBIS theorem (Theorem of the Day)

References

• R. Whitty, Theorem of the Day, «The Cameron–Fon-Der-Flaass IBIS Theorem» (GroupTheory/IBIS).
• P. J. Cameron, D. G. Fon-Der-Flaass, Bases for permutation groups and matroids, European J. Combin. 16 (1995) 537–544.

def IBIS.stab {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) (A : Set Ω) : Subgroup ↥G

The pointwise stabilizer in G of a set of points.

Equations

• IBIS.stab G A = fixingSubgroup (↥G) A

def IBIS.IsIrredundantBase {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) (l : List Ω) : Prop

An irredundant base of G: a list of points whose successive pointwise stabilizers strictly decrease and end at the trivial subgroup.

Equations

• IBIS.IsIrredundantBase G l = ((∀ i < l.length, IBIS.stab G {x : Ω | x ∈ List.take (i + 1) l} < IBIS.stab G {x : Ω | x ∈ List.take i l}) ∧ IBIS.stab G {x : Ω | x ∈ l} = ⊥)

def IBIS.PrefixChain {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) (l : List Ω) : Prop

The strict-decrease part of irredundancy.

Equations

• IBIS.PrefixChain G l = ∀ i < l.length, IBIS.stab G {x : Ω | x ∈ List.take (i + 1) l} < IBIS.stab G {x : Ω | x ∈ List.take i l}

theorem IBIS.isIrr_iff {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) (l : List Ω) : IsIrredundantBase G l ↔ PrefixChain G l ∧ stab G {x : Ω | x ∈ l} = ⊥

theorem IBIS.stab_union {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) (A B : Set Ω) : stab G (A ∪ B) = stab G A ⊓ stab G B

theorem IBIS.stab_anti {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) {A B : Set Ω} (h : A ⊆ B) : stab G B ≤ stab G A

theorem IBIS.mem_stab {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) {A : Set Ω} {g : ↥G} : g ∈ stab G A ↔ ∀ y ∈ A, ↑g y = y

theorem IBIS.stab_univ {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) : stab G Set.univ = ⊥

theorem IBIS.set_append {Ω : Type u_1} (l : List Ω) (x : Ω) : {y : Ω | y ∈ l ++ [x]} = {y : Ω | y ∈ l} ∪ {x}

theorem IBIS.prefixChain_nil {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) : PrefixChain G []

theorem IBIS.prefixChain_snoc {Ω : Type u_1} (G : Subgroup (Equiv.Perm Ω)) (l : List Ω) (x : Ω) : PrefixChain G (l ++ [x]) ↔ PrefixChain G l ∧ stab G ({y : Ω | y ∈ l} ∪ {x}) < stab G {y : Ω | y ∈ l}

theorem IBIS.prefixChain_nodup {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (l : List Ω) (h : PrefixChain G l) : l.Nodup

theorem IBIS.exists_irredundant_sublist {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (l : List Ω) : ∃ (k : List Ω), k.Sublist l ∧ PrefixChain G k ∧ stab G {x : Ω | x ∈ k} = stab G {x : Ω | x ∈ l} ∧ (k.length < l.length ∨ k = l)

Pruning: every list has an irredundant sublist with the same final stabilizer, strictly shorter unless the list was already irredundant.

theorem IBIS.exists_irredundantBase {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) : ∃ (l : List Ω), IsIrredundantBase G l

theorem IBIS.length_eq_ncard {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) {l : List Ω} (h : PrefixChain G l) : l.length = {x : Ω | x ∈ l}.ncard

theorem IBIS.equal_length_implies_reorder {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (h1 : ∀ (l l' : List Ω), IsIrredundantBase G l → IsIrredundantBase G l' → l.length = l'.length) (l l' : List Ω) (hl : IsIrredundantBase G l) (hp : l.Perm l') : IsIrredundantBase G l'

(1) ⇒ (2).

theorem IBIS.one_point_completion {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (h2 : ∀ (l l' : List Ω), IsIrredundantBase G l → l.Perm l' → IsIrredundantBase G l') {P : List Ω} {b x : Ω} (hPb : IsIrredundantBase G (P ++ [b])) (hx : stab G ({y : Ω | y ∈ P} ∪ {x}) < stab G {y : Ω | y ∈ P}) : stab G ({y : Ω | y ∈ P} ∪ {x}) = ⊥

Key lemma, under invariance by re-ordering.

theorem IBIS.exchange {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (h2 : ∀ (l l' : List Ω), IsIrredundantBase G l → l.Perm l' → IsIrredundantBase G l') {B C : Set Ω} (hB : ∃ (l : List Ω), IsIrredundantBase G l ∧ {x : Ω | x ∈ l} = B) (hC : ∃ (l : List Ω), IsIrredundantBase G l ∧ {x : Ω | x ∈ l} = C) (b : Ω) : b ∈ B \ C → ∃ c ∈ C \ B, ∃ (l : List Ω), IsIrredundantBase G l ∧ {x : Ω | x ∈ l} = insert c (B \ {b})

Basis exchange for the underlying sets of irredundant bases, under re-ordering invariance.

theorem IBIS.matroid_exists {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (h2 : ∀ (l l' : List Ω), IsIrredundantBase G l → l.Perm l' → IsIrredundantBase G l') : ∃ (M : Matroid Ω), M.E = Set.univ ∧ ∀ (B : Set Ω), M.IsBase B ↔ ∃ (l : List Ω), IsIrredundantBase G l ∧ {x : Ω | x ∈ l} = B

theorem IBIS.matroid_implies_equal_length {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) (M : Matroid Ω) (hM : ∀ (B : Set Ω), M.IsBase B ↔ ∃ (l : List Ω), IsIrredundantBase G l ∧ {x : Ω | x ∈ l} = B) (l l' : List Ω) (hl : IsIrredundantBase G l) (hl' : IsIrredundantBase G l') : l.length = l'.length

theorem IBIS.tfae {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Subgroup (Equiv.Perm Ω)) : [∀ (l l' : List Ω), IsIrredundantBase G l → IsIrredundantBase G l' → l.length = l'.length, ∀ (l l' : List Ω), IsIrredundantBase G l → l.Perm l' → IsIrredundantBase G l', ∃ (M : Matroid Ω), M.E = Set.univ ∧ ∀ (B : Set Ω), M.IsBase B ↔ ∃ (l : List Ω), IsIrredundantBase G l ∧ {x : Ω | x ∈ l} = B].TFAE

The Cameron–Fon-Der-Flaass IBIS theorem. For a permutation group G on a finite set Ω the following are equivalent: (1) all irredundant bases have the same size; (2) every re-ordering of an irredundant base is an irredundant base; (3) the underlying sets of the irredundant bases are exactly the bases of a matroid on Ω.