Lines and subspaces

Constructions on Mathlib's Combinatorics.Line and Combinatorics.Subspace used in Shelah's proof of the Hales--Jewett theorem.

Main definitions

• Combinatorics.Line.reindex: change the index type of a line.
• Combinatorics.Subspace.prodLine: the subspace spanned by a subspace and a line on disjoint sets of coordinates.
• Combinatorics.Subspace.compLine: a line of the parameter cube of a subspace, as a line of the ambient cube.

Main results

• Combinatorics.Line.exists_map_eq_of_card_le: in a cube of dimension N colored with at most N colors, some line has the same color at two given letters.

def Combinatorics.Line.reindex {α : Type u_2} {ι : Type u_3} {ι' : Type u_4} (l : Line α ι) (e : ι ≃ ι') : Line α ι'

Change the index type of a line.

Equations

• l.reindex e = { idxFun := l.idxFun ∘ ⇑e.symm, proper := ⋯ }

@[simp]

theorem Combinatorics.Line.reindex_apply {α : Type u_2} {ι : Type u_3} {ι' : Type u_4} (l : Line α ι) (e : ι ≃ ι') (x : α) : ↑(l.reindex e) x = ↑l x ∘ ⇑e.symm

theorem Combinatorics.Line.exists_map_eq_of_card_le {α : Type u_2} {κ : Type u_5} [Finite κ] {N : ℕ} (hN : Nat.card κ ≤ N) (a b : α) (C : (Fin N → α) → κ) : ∃ (l : Line α (Fin N)), C (↑l a) = C (↑l b)

If a cube of dimension N is colored with at most N colors, then for any two letters a and b some line has the same color at a and at b.

The N + 1 words that are a on an initial segment of the coordinates and b afterwards cannot have distinct colors. Two of them with the same color are the points at a and at b of the line whose wildcards are the coordinates on which they differ.

def Combinatorics.Subspace.prodLine {η : Type u_1} {α : Type u_2} {ι : Type u_3} {ι' : Type u_4} (V : Subspace η α ι) (l : Line α ι') : Subspace (Option η) α (ι ⊕ ι')

A subspace of ι → α and a line of ι' → α span a subspace of ι ⊕ ι' → α with one more dimension, none, along the line.

Equations

• V.prodLine l = { idxFun := Sum.elim (fun (i : ι) => Sum.map id some (V.idxFun i)) fun (i : ι') => (l.idxFun i).elim (Sum.inr none) Sum.inl, proper := ⋯ }

@[simp]

theorem Combinatorics.Subspace.prodLine_apply {η : Type u_1} {α : Type u_2} {ι : Type u_3} {ι' : Type u_4} (V : Subspace η α ι) (l : Line α ι') (x : Option η → α) : ↑(V.prodLine l) x = Sum.elim (↑V (x ∘ some)) (↑l (x none))

def Combinatorics.Subspace.compLine {η : Type u_1} {α : Type u_2} {ι : Type u_3} (V : Subspace η α ι) (l : Line α η) : Line α ι

A line of the parameter cube of a subspace, as a line of the ambient cube.

Equations

• V.compLine l = { idxFun := fun (i : ι) => Sum.elim some l.idxFun (V.idxFun i), proper := ⋯ }

@[simp]

theorem Combinatorics.Subspace.compLine_apply {η : Type u_1} {α : Type u_2} {ι : Type u_3} (V : Subspace η α ι) (l : Line α η) (x : α) : ↑(V.compLine l) x = ↑V (↑l x)