The Hales-Jewett theorem

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

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.

Combinatorial subspaces are higher-dimensional analogues of combinatorial lines. See Combinatorics.Subspace. The multidimensional Hales-Jewett theorem generalises the statement above from combinatorial lines to combinatorial subspaces of a fixed dimension.

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.Subspace.exists_mono_in_high_dimension: The multidimensional 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.Subspace (η : Type u_5) (α : Type u_6) (ι : Type u_7) : Type (max (max u_5 u_6) u_7)

The type of combinatorial subspaces. A subspace l : Subspace η α ι in the hypercube ι → α defines a function (η → α) → ι → α from η → α to the hypercube, such that for each coordinate i : ι and direction e : η, the function fun x ↦ l x i is either fun x ↦ x e for some direction e : η or constant. We require subspaces to be non-degenerate in the sense that, for every e : η, fun x ↦ l x i is fun x ↦ x e for at least one i.

Formally, a subspace is represented by a word l.idxFun : ι → α ⊕ η which says whether fun x ↦ l x i is fun x ↦ x e (corresponding to l.idxFun i = Sum.inr e) or constantly a (corresponding to l.idxFun i = Sum.inl a).

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

• idxFun : ι → α ⊕ η

  The word representing a combinatorial subspace. l.idxfun i = Sum.inr e means that l x i = x e for all x and l.idxfun i = some a means that l x i = a for all x.

• proper (e : η) : ∃ (i : ι), self.idxFun i = Sum.inr e

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

theorem Combinatorics.Subspace.ext_iff {η : Type u_5} {α : Type u_6} {ι : Type u_7} {x y : Subspace η α ι} : x = y ↔ x.idxFun = y.idxFun

theorem Combinatorics.Subspace.ext {η : Type u_5} {α : Type u_6} {ι : Type u_7} {x y : Subspace η α ι} (idxFun : x.idxFun = y.idxFun) : x = y

instance Combinatorics.Subspace.instInhabited {α : Type u_6} {ι : Type u_7} : Inhabited (Subspace ι α ι)

The combinatorial subspace corresponding to the identity embedding (ι → α) → (ι → α).

Equations

• Combinatorics.Subspace.instInhabited = { default := { idxFun := Sum.inr, proper := ⋯ } }

def Combinatorics.Subspace.toFun {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Subspace η α ι) (x : η → α) (i : ι) : α

Consider a subspace l : Subspace η α ι as a function (η → α) → ι → α.

Equations

• ↑l x i = Sum.elim id x (l.idxFun i)

instance Combinatorics.Subspace.instCoeFun {η : Type u_5} {α : Type u_6} {ι : Type u_7} : CoeFun (Subspace η α ι) fun (x : Subspace η α ι) => (η → α) → ι → α

Equations

• Combinatorics.Subspace.instCoeFun = { coe := Combinatorics.Subspace.toFun }

theorem Combinatorics.Subspace.coe_apply {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Subspace η α ι) (x : η → α) (i : ι) : ↑l x i = Sum.elim id x (l.idxFun i)

theorem Combinatorics.Subspace.coe_injective {η : Type u_5} {α : Type u_6} {ι : Type u_7} [Nontrivial α] : Function.Injective toFun

theorem Combinatorics.Subspace.apply_def {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Subspace η α ι) (x : η → α) (i : ι) : ↑l x i = Sum.elim id x (l.idxFun i)

theorem Combinatorics.Subspace.apply_inl {η : Type u_5} {α : Type u_6} {ι : Type u_7} {l : Subspace η α ι} {x : η → α} {i : ι} {a : α} (h : l.idxFun i = Sum.inl a) : ↑l x i = a

theorem Combinatorics.Subspace.apply_inr {η : Type u_5} {α : Type u_6} {ι : Type u_7} {l : Subspace η α ι} {x : η → α} {i : ι} {e : η} (h : l.idxFun i = Sum.inr e) : ↑l x i = x e

def Combinatorics.Subspace.IsMono {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} (C : (ι → α) → κ) (l : Subspace η α ι) : Prop

Given a coloring C of ι → α and a combinatorial subspace l of ι → α, l.IsMono C means that l is monochromatic with regard to C.

Equations

• Combinatorics.Subspace.IsMono C l = ∃ (c : κ), ∀ (x : η → α), C (↑l x) = c

def Combinatorics.Subspace.reindex {η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') : Subspace η' α' ι'

Change the index types of a subspace.

Equations

• l.reindex eη eα eι = { idxFun := fun (i : ι') => Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm i)), proper := ⋯ }

@[simp]

theorem Combinatorics.Subspace.reindex_apply {η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') (x : η' → α') (i : ι') : ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

@[simp]

theorem Combinatorics.Subspace.reindex_isMono {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} {l : Subspace η α ι} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι' → α') → κ} : IsMono C (l.reindex eη eα eι) ↔ IsMono (fun (x : ι → α) => C (⇑eα ∘ x ∘ ⇑eι.symm)) l

theorem Combinatorics.Subspace.IsMono.reindex {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} {l : Subspace η α ι} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι → α) → κ} (hl : IsMono C l) : IsMono (fun (x : ι' → α') => C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)

structure Combinatorics.Line (α : Type u_5) (ι : Type u_6) : Type (max u_5 u_6)

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.ext_iff {α : Type u_5} {ι : Type u_6} {x y : Line α ι} : x = y ↔ x.idxFun = y.idxFun

theorem Combinatorics.Line.ext {α : Type u_5} {ι : Type u_6} {x y : Line α ι} (idxFun : x.idxFun = y.idxFun) : x = y

def Combinatorics.Line.toFun {α : Type u_2} {ι : Type u_3} (l : Line α ι) (x : α) (i : ι) : α

Consider a line l : Line α ι as a function α → ι → α.

Equations

• ↑l x i = (l.idxFun i).getD x

instance Combinatorics.Line.instCoeFun {α : Type u_2} {ι : Type u_3} : CoeFun (Line α ι) fun (x : Line α ι) => α → ι → α

Equations

• Combinatorics.Line.instCoeFun = { coe := Combinatorics.Line.toFun }

@[simp]

theorem Combinatorics.Line.coe_apply {α : Type u_2} {ι : Type u_3} (l : Line α ι) (x : α) (i : ι) : ↑l x i = (l.idxFun i).getD x

theorem Combinatorics.Line.coe_injective {α : Type u_2} {ι : Type u_3} [Nontrivial α] : Function.Injective toFun

def Combinatorics.Line.IsMono {α : Type u_5} {ι : Type u_6} {κ : Sort u_7} (C : (ι → α) → κ) (l : Line α ι) : Prop

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

Equations

• Combinatorics.Line.IsMono C l = ∃ (c : κ), ∀ (x : α), C (↑l x) = c

def Combinatorics.Line.toSubspaceUnit {α : Type u_2} {ι : Type u_3} (l : Line α ι) : Subspace Unit α ι

Consider a line as a one-dimensional subspace.

Equations

• l.toSubspaceUnit = { idxFun := fun (i : ι) => (l.idxFun i).elim (Sum.inr ()) Sum.inl, proper := ⋯ }

@[simp]

theorem Combinatorics.Line.toSubspaceUnit_apply {α : Type u_2} {ι : Type u_3} (l : Line α ι) (a : Unit → α) : ↑l.toSubspaceUnit a = ↑l (a ())

@[simp]

theorem Combinatorics.Line.toSubspaceUnit_isMono {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Line α ι} {C : (ι → α) → κ} : Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l

theorem Combinatorics.Line.IsMono.toSubspaceUnit {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Line α ι} {C : (ι → α) → κ} : IsMono C l → Subspace.IsMono C l.toSubspaceUnit

Alias of the reverse direction of Combinatorics.Line.toSubspaceUnit_isMono.

def Combinatorics.Line.toSubspace {η : Type u_1} {α : Type u_2} {ι : Type u_3} (l : Line (η → α) ι) : Subspace η α (ι × η)

Consider a line in ι → η → α as a η-dimensional subspace in ι × η → α.

Equations

• l.toSubspace = { idxFun := fun (ie : ι × η) => (l.idxFun ie.1).elim (Sum.inr ie.2) fun (f : η → α) => Sum.inl (f ie.2), proper := ⋯ }

@[simp]

theorem Combinatorics.Line.toSubspace_apply {η : Type u_1} {α : Type u_2} {ι : Type u_3} (l : Line (η → α) ι) (a : η → α) (ie : ι × η) : ↑l.toSubspace a ie = ↑l a ie.1 ie.2

@[simp]

theorem Combinatorics.Line.toSubspace_isMono {η : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Line (η → α) ι} {C : (ι × η → α) → κ} : Subspace.IsMono C l.toSubspace ↔ IsMono (fun (x : ι → η → α) => C fun (x_1 : ι × η) => match x_1 with | (i, e) => x i e) l

theorem Combinatorics.Line.IsMono.toSubspace {η : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Line (η → α) ι} {C : (ι × η → α) → κ} : IsMono (fun (x : ι → η → α) => C fun (x_1 : ι × η) => match x_1 with | (i, e) => x i e) l → Subspace.IsMono C l.toSubspace

Alias of the reverse direction of Combinatorics.Line.toSubspace_isMono.

def Combinatorics.Line.diagonal (α : Type u_5) (ι : Type u_6) [Nonempty ι] : 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_5) (ι : Type u_6) [Nonempty ι] : Inhabited (Line α ι)

Equations

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

structure Combinatorics.Line.AlmostMono {α : Type u_5} {ι : Type u_6} {κ : Type u_7} (C : (ι → Option α) → κ) : Type (max (max u_5 u_6) u_7)

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

• line : 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 (↑self.line (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_5} {ι : Type u_6} {κ : Type u_7} [Nonempty ι] [Inhabited κ] : Inhabited (AlmostMono fun (x : ι → Option α) => default)

Equations

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

structure Combinatorics.Line.ColorFocused {α : Type u_5} {ι : Type u_6} {κ : Type u_7} (C : (ι → Option α) → κ) : Type (max (max u_5 u_6) u_7)

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 (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 : AlmostMono C) : p ∈ self.lines → ↑p.line none = self.focus

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

• distinct_colors : (Multiset.map 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_5} {ι : Type u_6} {κ : Type u_7} (C : (ι → Option α) → κ) : Inhabited (ColorFocused C)

Equations

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

def Combinatorics.Line.map {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : α → α') (l : Line α ι) : 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_5} {ι : Type u_6} {ι' : Type u_7} (v : ι → α) (l : Line α ι') : 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_5} {ι : Type u_6} {ι' : Type u_7} (l : Line α ι) (v : ι' → α) : 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_5} {ι : Type u_6} {ι' : Type u_7} (l : Line α ι) (l' : Line α ι') : 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_def {α : Type u_2} {ι : Type u_3} (l : Line α ι) (x : α) : ↑l x = fun (i : ι) => (l.idxFun i).getD x

theorem Combinatorics.Line.apply_none {α : Type u_5} {ι : Type u_6} (l : Line α ι) (x : α) (i : ι) (h : l.idxFun i = none) : ↑l x i = x

theorem Combinatorics.Line.apply_some {α : Type u_2} {ι : Type u_3} {l : Line α ι} {i : ι} {a x : α} (h : l.idxFun i = some a) : ↑l x i = a

@[simp]

theorem Combinatorics.Line.map_apply {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : α → α') (l : Line α ι) (x : α) : ↑(map f l) (f x) = f ∘ ↑l x

@[simp]

theorem Combinatorics.Line.vertical_apply {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (v : ι → α) (l : Line α ι') (x : α) : ↑(vertical v l) x = Sum.elim v (↑l x)

@[simp]

theorem Combinatorics.Line.horizontal_apply {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Line α ι) (v : ι' → α) (x : α) : ↑(l.horizontal v) x = Sum.elim (↑l x) v

@[simp]

theorem Combinatorics.Line.prod_apply {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Line α ι) (l' : Line α ι') (x : α) : ↑(l.prod l') x = Sum.elim (↑l x) (↑l' x)

@[simp]

theorem Combinatorics.Line.diagonal_apply {α : Type u_5} {ι : Type u_6} [Nonempty ι] (x : α) : ↑(diagonal α ι) x = fun (x_1 : ι) => x

theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] : ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : 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_5} {κ : Type u_6} [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.

theorem Combinatorics.Subspace.exists_mono_in_high_dimension (α : Type u_5) (κ : Type u_6) (η : Type u_7) [Finite α] [Finite κ] [Finite η] : ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Subspace η α ι), IsMono C l

The multidimensional Hales-Jewett theorem, aka extended 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 subspace of dimension η.

theorem Combinatorics.Subspace.exists_mono_in_high_dimension_fin (α : Type u_5) (κ : Type u_6) (η : Type u_7) [Finite α] [Finite κ] [Finite η] : ∃ (n : ℕ), ∀ (C : (Fin n → α) → κ), ∃ (l : Subspace η α (Fin n)), IsMono C l

A variant of the extended Hales-Jewett theorem exists_mono_in_high_dimension where the returned type is some Fin n instead of a general fintype.