Bases and Saxl adjacency

Foundational definitions for ordered tuple bases, ordinary and generalized Saxl adjacency, exact base size, and common neighbours.

def Saxl.IsBaseTuple (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] {n : ℕ} (x : Fin n → Ω) : Prop

An ordered tuple whose pointwise stabilizer in G is trivial.

Equations

• Saxl.IsBaseTuple G Ω x = ∀ (g : G), (∀ (i : Fin n), g • x i = x i) → g = 1

def Saxl.IsSetBaseTuple (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] {n : ℕ} (x : Fin n → Ω) : Prop

An injective ordered tuple corresponding literally to a base as a set.

Equations

• Saxl.IsSetBaseTuple G Ω x = (Function.Injective x ∧ Saxl.IsBaseTuple G Ω x)

def Saxl.Adjacent (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] (x y : Ω) : Prop

Base-two adjacency: the displayed ordered pair has trivial stabilizer.

Equations

• Saxl.Adjacent G Ω x y = Saxl.IsBaseTuple G Ω (Fin.cons x (Fin.cons y Fin.elim0))

def Saxl.GeneralizedAdjacent (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] (tail : ℕ) (x y : Ω) : Prop

Two vertices extend to an injective base of size tail + 2.

Equations

• Saxl.GeneralizedAdjacent G Ω tail x y = ∃ (z : Fin tail → Ω), Saxl.IsSetBaseTuple G Ω (Fin.cons x (Fin.cons y z))

def Saxl.HasCommonNeighbour (Ω : Type u_2) (R : Ω → Ω → Prop) (x y : Ω) : Prop

Two vertices have a common neighbour for a relation R.

Equations

• Saxl.HasCommonNeighbour Ω R x y = ∃ (z : Ω), R x z ∧ R z y

def Saxl.ExactBaseSize (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] (n : ℕ) : Prop

Exact base size n, stated without a global minimum operator.

Equations

• Saxl.ExactBaseSize G Ω n = ((∃ (x : Fin n → Ω), Saxl.IsSetBaseTuple G Ω x) ∧ ∀ m < n, ¬∃ (x : Fin m → Ω), Saxl.IsSetBaseTuple G Ω x)

def Saxl.tupleStabilizer (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] {n : ℕ} (x : Fin n → Ω) : Subgroup G

The pointwise stabilizer of all entries of an ordered tuple.

Equations

• Saxl.tupleStabilizer G Ω x = ⨅ (i : Fin n), MulAction.stabilizer G (x i)

@[simp]

theorem Saxl.mem_tupleStabilizer_iff (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] {n : ℕ} (x : Fin n → Ω) (g : G) : g ∈ tupleStabilizer G Ω x ↔ ∀ (i : Fin n), g • x i = x i

theorem Saxl.isBaseTuple_iff_tupleStabilizer_eq_bot (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] {n : ℕ} (x : Fin n → Ω) : IsBaseTuple G Ω x ↔ tupleStabilizer G Ω x = ⊥

A tuple is a base exactly when its pointwise stabilizer is trivial.

theorem Saxl.adjacent_iff_pair_stabilizer_eq_bot (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] (x y : Ω) : Adjacent G Ω x y ↔ MulAction.stabilizer G x ⊓ MulAction.stabilizer G y = ⊥

The stabilizer characterization of ordinary Saxl adjacency.

theorem Saxl.isBaseTuple_singleton_iff_stabilizer_eq_bot (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] (x : Ω) : (IsBaseTuple G Ω fun (x_1 : Fin 1) => x) ↔ MulAction.stabilizer G x = ⊥

A one-entry tuple is a base exactly when that point has trivial stabilizer.

theorem Saxl.exactBaseSize_two_iff (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] : ExactBaseSize G Ω 2 ↔ (∃ (x : Ω) (y : Ω), x ≠ y ∧ Adjacent G Ω x y) ∧ ∀ (x : Ω), MulAction.stabilizer G x ≠ ⊥

Exact set-base size two means that a distinct adjacent pair exists, but no single point has trivial stabilizer.

theorem Saxl.noCommonNeighbour (Ω : Type u_2) {R : Ω → Ω → Prop} {x y : Ω} (h : ∀ (z : Ω), R x z → R z y → False) : ¬HasCommonNeighbour Ω R x y

To rule out a common neighbour it suffices to rule out every possible witness, one vertex at a time.