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)

• 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, Combinatorics.Line.idxFun s 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.

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.

instance Combinatorics.Line.instCoeFunLineForAll (α : Type u_1) (ι : Type u_2) : CoeFun (Combinatorics.Line α ι) fun 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.

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

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

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

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

• 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 i => Option.getD (Combinatorics.Line.idxFun s.line i) x) (some x)) = s.color

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

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

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

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

• 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 : Combinatorics.Line.AlmostMono C), p ∈ s.lines → (fun x i => Option.getD (Combinatorics.Line.idxFun p.line i) x) none = s.focus

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

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

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

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.

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

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.

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 ι ⊕ ι' → α.

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 ι ⊕ ι' → α.

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 ι ⊕ ι' → α.

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

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

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

@[simp]

theorem Combinatorics.Line.map_apply {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : α → α') (l : Combinatorics.Line α ι) (x : α) : (fun x i => Option.getD (Combinatorics.Line.idxFun (Combinatorics.Line.map f l) i) x) (f x) = f ∘ (fun x i => Option.getD (Combinatorics.Line.idxFun l i) 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 => Option.getD (Combinatorics.Line.idxFun (Combinatorics.Line.vertical v l) i) x) x = Sum.elim v ((fun x i => Option.getD (Combinatorics.Line.idxFun l i) 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 => Option.getD (Combinatorics.Line.idxFun (Combinatorics.Line.horizontal l v) i) x) x = Sum.elim ((fun x i => Option.getD (Combinatorics.Line.idxFun l i) 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 => Option.getD (Combinatorics.Line.idxFun (Combinatorics.Line.prod l l') i) x) x = Sum.elim ((fun x i => Option.getD (Combinatorics.Line.idxFun l i) x) x) ((fun x i => Option.getD (Combinatorics.Line.idxFun l' i) x) x)

@[simp]

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

theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] : ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, 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, a > 0 ∧ ∃ b c, ∀ (s : M), 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.