The Hales-Jewett theorem

We prove the Hales-Jewett theorem and deduce Van der Waerden's theorem as a corollary.

The Hales-Jewett theorem is a result in Ramsey theory dealing with combinatorial lines. Given an 'alphabet' α : Type* and a b : α, an example of a combinatorial line in α^5 is { (a, x, x, b, x) | x : α }. See Combinatorics.Line for a precise general definition. The Hales-Jewett theorem states that for any fixed finite types α and κ, there exists a (potentially huge) finite type ι such that whenever ι → α is κ-colored (i.e. for any coloring C : (ι → α) → κ), there exists a monochromatic line. We prove the Hales-Jewett theorem using the idea of color focusing and a product argument. See the proof of Combinatorics.Line.exists_mono_in_high_dimension' for details.

The version of Van der Waerden's theorem in this file states that whenever a commutative monoid M is finitely colored and S is a finite subset, there exists a monochromatic homothetic copy of S. This follows from the Hales-Jewett theorem by considering the map (ι → S) → M sending v to ∑ i : ι, v i, which sends a combinatorial line to a homothetic copy of S.

Main results

• Combinatorics.Line.exists_mono_in_high_dimension: the Hales-Jewett theorem.
• Combinatorics.exists_mono_homothetic_copy: a generalization of Van der Waerden's theorem.

Implementation details

For convenience, we work directly with finite types instead of natural numbers. That is, we write α, ι, κ for (finite) types where one might traditionally use natural numbers n, H, c. This allows us to work directly with α, Option α, (ι → α) → κ, and ι ⊕ ι' instead of Fin n, Fin (n+1), Fin (c^(n^H)), and Fin (H + H').

Todo

• Prove a finitary version of Van der Waerden's theorem (either by compactness or by modifying the current proof).

• One could reformulate the proof of Hales-Jewett to give explicit upper bounds on the number of coordinates needed.

Tags

combinatorial line, Ramsey theory, arithmetic progression

References

• https://en.wikipedia.org/wiki/Hales%E2%80%93Jewett_theorem

structure Combinatorics.Line (α : Type u_1) (ι : Type u_2) : Type (max u_1 u_2)

The type of combinatorial lines. A line l : Line α ι in the hypercube ι → α defines a function α → ι → α from α to the hypercube, such that for each coordinate i : ι, the function fun x ↦ l x i is either id or constant. We require lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one i.

Formally, a line is represented by a word l.idxFun : ι → Option α which says whether fun x ↦ l x i is id (corresponding to l.idxFun i = none) or constantly y (corresponding to l.idxFun i = some y).

When α has size 1 there can be many elements of Line α ι defining the same function.

• idxFun : ι → Option α

  The word representing a combinatorial line. l.idxfun i = none means that l x i = x for all x and l.idxfun i = some y means that l x i = y.

• proper : ∃ (i : ι), self.idxFun i = none

  We require combinatorial lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one coordinate i.

theorem Combinatorics.Line.proper {α : Type u_1} {ι : Type u_2} (self : Combinatorics.Line α ι) : ∃ (i : ι), self.idxFun i = none

We require combinatorial lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one coordinate i.

instance Combinatorics.Line.instCoeFunForallForall (α : Type u_1) (ι : Type u_2) : CoeFun (Combinatorics.Line α ι) fun (x : Combinatorics.Line α ι) => α → ι → α

Equations

• Combinatorics.Line.instCoeFunForallForall α ι = { coe := fun (l : Combinatorics.Line α ι) (x : α) (i : ι) => (l.idxFun i).getD x }

def Combinatorics.Line.IsMono {α : Type u_1} {ι : Type u_2} {κ : Sort u_3} (C : (ι → α) → κ) (l : Combinatorics.Line α ι) : Prop

A line is monochromatic if all its points are the same color.

Equations

• Combinatorics.Line.IsMono C l = ∃ (c : κ), ∀ (x : α), C ((fun (x : α) (i : ι) => (l.idxFun i).getD x) x) = c

def Combinatorics.Line.diagonal (α : Type u_1) (ι : Type u_2) [Nonempty ι] : Combinatorics.Line α ι

The diagonal line. It is the identity at every coordinate.

Equations

• Combinatorics.Line.diagonal α ι = { idxFun := fun (x : ι) => none, proper := ⋯ }

instance Combinatorics.Line.instInhabitedOfNonempty (α : Type u_1) (ι : Type u_2) [Nonempty ι] : Inhabited (Combinatorics.Line α ι)

Equations

• Combinatorics.Line.instInhabitedOfNonempty α ι = { default := Combinatorics.Line.diagonal α ι }

structure Combinatorics.Line.AlmostMono {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → Option α) → κ) : Type (max (max u_1 u_2) u_3)

The type of lines that are only one color except possibly at their endpoints.

• line : Combinatorics.Line (Option α) ι

  The underlying line of an almost monochromatic line, where the coordinate dimension α is extended by an additional symbol none, thought to be marking the endpoint of the line.

• color : κ

  The main color of an almost monochromatic line.

• has_color : ∀ (x : α), C ((fun (x : Option α) (i : ι) => (self.line.idxFun i).getD x) (some x)) = self.color

  The proposition that the underlying line of an almost monochromatic line assumes its main color except possibly at the endpoints.

theorem Combinatorics.Line.AlmostMono.has_color {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {C : (ι → Option α) → κ} (self : Combinatorics.Line.AlmostMono C) (x : α) : C ((fun (x : Option α) (i : ι) => (self.line.idxFun i).getD x) (some x)) = self.color

The proposition that the underlying line of an almost monochromatic line assumes its main color except possibly at the endpoints.

instance Combinatorics.Line.instInhabitedAlmostMonoDefaultOfNonempty {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [Nonempty ι] [Inhabited κ] : Inhabited (Combinatorics.Line.AlmostMono fun (x : ι → Option α) => default)

Equations

• Combinatorics.Line.instInhabitedAlmostMonoDefaultOfNonempty = { default := { line := default, color := default, has_color := ⋯ } }

structure Combinatorics.Line.ColorFocused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → Option α) → κ) : Type (max (max u_1 u_2) u_3)

The type of collections of lines such that

• each line is only one color except possibly at its endpoint
• the lines all have the same endpoint
• the colors of the lines are distinct. Used in the proof exists_mono_in_high_dimension.

• lines : Multiset (Combinatorics.Line.AlmostMono C)

  The underlying multiset of almost monochromatic lines of a color-focused collection.

• focus : ι → Option α

  The common endpoint of the lines in the color-focused collection.

• is_focused : ∀ p ∈ self.lines, (fun (x : Option α) (i : ι) => (p.line.idxFun i).getD x) none = self.focus

  The proposition that all lines in a color-focused collection have the same endpoint.

• distinct_colors : (Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup

  The proposition that all lines in a color-focused collection of lines have distinct colors.

theorem Combinatorics.Line.ColorFocused.is_focused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {C : (ι → Option α) → κ} (self : Combinatorics.Line.ColorFocused C) (p : Combinatorics.Line.AlmostMono C) : p ∈ self.lines → (fun (x : Option α) (i : ι) => (p.line.idxFun i).getD x) none = self.focus

The proposition that all lines in a color-focused collection have the same endpoint.

theorem Combinatorics.Line.ColorFocused.distinct_colors {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {C : (ι → Option α) → κ} (self : Combinatorics.Line.ColorFocused C) : (Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup

The proposition that all lines in a color-focused collection of lines have distinct colors.

instance Combinatorics.Line.instInhabitedColorFocused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → Option α) → κ) : Inhabited (Combinatorics.Line.ColorFocused C)

Equations

• Combinatorics.Line.instInhabitedColorFocused C = { default := { lines := 0, focus := fun (x : ι) => none, is_focused := ⋯, distinct_colors := ⋯ } }

def Combinatorics.Line.map {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : α → α') (l : Combinatorics.Line α ι) : Combinatorics.Line α' ι

A function f : α → α' determines a function line α ι → line α' ι. For a coordinate i, l.map f is the identity at i if l is, and constantly f y if l is constantly y at i.

Equations

• Combinatorics.Line.map f l = { idxFun := fun (i : ι) => Option.map f (l.idxFun i), proper := ⋯ }

def Combinatorics.Line.vertical {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ι → α) (l : Combinatorics.Line α ι') : Combinatorics.Line α (ι ⊕ ι')

A point in ι → α and a line in ι' → α determine a line in ι ⊕ ι' → α.

Equations

• Combinatorics.Line.vertical v l = { idxFun := Sum.elim (some ∘ v) l.idxFun, proper := ⋯ }

def Combinatorics.Line.horizontal {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : Combinatorics.Line α ι) (v : ι' → α) : Combinatorics.Line α (ι ⊕ ι')

A line in ι → α and a point in ι' → α determine a line in ι ⊕ ι' → α.

Equations

• l.horizontal v = { idxFun := Sum.elim l.idxFun (some ∘ v), proper := ⋯ }

def Combinatorics.Line.prod {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : Combinatorics.Line α ι) (l' : Combinatorics.Line α ι') : Combinatorics.Line α (ι ⊕ ι')

One line in ι → α and one in ι' → α together determine a line in ι ⊕ ι' → α.

Equations

• l.prod l' = { idxFun := Sum.elim l.idxFun l'.idxFun, proper := ⋯ }

theorem Combinatorics.Line.apply {α : Type u_1} {ι : Type u_2} (l : Combinatorics.Line α ι) (x : α) : (fun (x : α) (i : ι) => (l.idxFun i).getD x) x = fun (i : ι) => (l.idxFun i).getD x

theorem Combinatorics.Line.apply_none {α : Type u_1} {ι : Type u_2} (l : Combinatorics.Line α ι) (x : α) (i : ι) (h : l.idxFun i = none) : (fun (x : α) (i : ι) => (l.idxFun i).getD x) x i = x

theorem Combinatorics.Line.apply_of_ne_none {α : Type u_1} {ι : Type u_2} (l : Combinatorics.Line α ι) (x : α) (i : ι) (h : l.idxFun i ≠ none) : some ((fun (x : α) (i : ι) => (l.idxFun i).getD x) x i) = l.idxFun i

@[simp]

theorem Combinatorics.Line.map_apply {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : α → α') (l : Combinatorics.Line α ι) (x : α) : (fun (x : α') (i : ι) => ((Combinatorics.Line.map f l).idxFun i).getD x) (f x) = f ∘ (fun (x : α) (i : ι) => (l.idxFun i).getD x) x

@[simp]

theorem Combinatorics.Line.vertical_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ι → α) (l : Combinatorics.Line α ι') (x : α) : (fun (x : α) (i : ι ⊕ ι') => ((Combinatorics.Line.vertical v l).idxFun i).getD x) x = Sum.elim v ((fun (x : α) (i : ι') => (l.idxFun i).getD x) x)

@[simp]

theorem Combinatorics.Line.horizontal_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : Combinatorics.Line α ι) (v : ι' → α) (x : α) : (fun (x : α) (i : ι ⊕ ι') => ((l.horizontal v).idxFun i).getD x) x = Sum.elim ((fun (x : α) (i : ι) => (l.idxFun i).getD x) x) v

@[simp]

theorem Combinatorics.Line.prod_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : Combinatorics.Line α ι) (l' : Combinatorics.Line α ι') (x : α) : (fun (x : α) (i : ι ⊕ ι') => ((l.prod l').idxFun i).getD x) x = Sum.elim ((fun (x : α) (i : ι) => (l.idxFun i).getD x) x) ((fun (x : α) (i : ι') => (l'.idxFun i).getD x) x)

@[simp]

theorem Combinatorics.Line.diagonal_apply {α : Type u_1} {ι : Type u_2} [Nonempty ι] (x : α) : (fun (x : α) (i : ι) => ((Combinatorics.Line.diagonal α ι).idxFun i).getD x) x = fun (x_1 : ι) => x

theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] : ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Combinatorics.Line α ι), Combinatorics.Line.IsMono C l

The Hales-Jewett theorem: for any finite types α and κ, there exists a finite type ι such that whenever the hypercube ι → α is κ-colored, there is a monochromatic combinatorial line.

theorem Combinatorics.exists_mono_homothetic_copy {M : Type u_1} {κ : Type u_2} [AddCommMonoid M] (S : Finset M) [Finite κ] (C : M → κ) : ∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c

A generalization of Van der Waerden's theorem: if M is a finitely colored commutative monoid, and S is a finite subset, then there exists a monochromatic homothetic copy of S.