mathlib documentation

combinatorics.hales_jewett

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 #

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 #

Tags #

combinatorial line, Ramsey theory, arithmetic progession

References #

source
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 λ x, l x i is either id or constant. We require lines to be nontrivial in the sense that λ x, l x i is id for at least one i.

Formally, a line is represented by the function l.idx_fun : ι → option α which says whether λ x, l x i is id (corresponding to l.idx_fun i = none) or constantly y (corresponding to l.idx_fun i = some y).

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

Instances for combinatorics.line
source
@[protected, instance]
def combinatorics.line.has_coe_to_fun (α : Type u_1) (ι : Type u_2) :
has_coe_to_fun (combinatorics.line α ι) (λ (_x : combinatorics.line α ι), α → ι → α)
Equations
source
def combinatorics.line.is_mono {α : 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
source
def combinatorics.line.diagonal (α : Type u_1) (ι : Type u_2) [nonempty ι] :
combinatorics.line α ι

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

Equations
source
@[protected, instance]
def combinatorics.line.inhabited (α : Type u_1) (ι : Type u_2) [nonempty ι] :
inhabited (combinatorics.line α ι)
Equations
source
structure combinatorics.line.almost_mono {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → option α) → κ) :
Type (max u_1 u_2 u_3)

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

Instances for combinatorics.line.almost_mono
source
@[protected, instance]
def combinatorics.line.almost_mono.inhabited {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [nonempty ι] [inhabited κ] :
inhabited (combinatorics.line.almost_mono (λ (v : ι → option α), inhabited.default))
Equations
source
structure combinatorics.line.color_focused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → option α) → κ) :
Type (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.
Instances for combinatorics.line.color_focused
source
@[protected, instance]
def combinatorics.line.color_focused.inhabited {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → option α) → κ) :
inhabited (combinatorics.line.color_focused C)
Equations
source
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
source
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
source
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
source
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
source
theorem combinatorics.line.apply {α : Type u_1} {ι : Type u_2} (l : combinatorics.line α ι) (x : α) :
⇑l x = λ (i : ι), (l.idx_fun i).get_or_else x
source
theorem combinatorics.line.apply_none {α : Type u_1} {ι : Type u_2} (l : combinatorics.line α ι) (x : α) (i : ι) (h : l.idx_fun i = option.none) :
⇑l x i = x
source
theorem combinatorics.line.apply_of_ne_none {α : Type u_1} {ι : Type u_2} (l : combinatorics.line α ι) (x : α) (i : ι) (h : l.idx_fun i ≠ option.none) :
option.some (⇑l x i) = l.idx_fun i
source
@[simp]
theorem combinatorics.line.map_apply {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : α → α') (l : combinatorics.line α ι) (x : α) :
⇑(combinatorics.line.map f l) (f x) = f ∘ ⇑l x
source
@[simp]
theorem combinatorics.line.vertical_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ι → α) (l : combinatorics.line α ι') (x : α) :
⇑(combinatorics.line.vertical v l) x = sum.elim v (⇑l x)
source
@[simp]
theorem combinatorics.line.horizontal_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : combinatorics.line α ι) (v : ι' → α) (x : α) :
⇑(l.horizontal v) x = sum.elim (⇑l x) v
source
@[simp]
theorem combinatorics.line.prod_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : combinatorics.line α ι) (l' : combinatorics.line α ι') (x : α) :
⇑(l.prod l') x = sum.elim (⇑l x) (⇑l' x)
source
@[simp]
theorem combinatorics.line.diagonal_apply {α : Type u_1} {ι : Type u_2} [nonempty ι] (x : α) :
⇑(combinatorics.line.diagonal α ι) x = λ (i : ι), x
source
theorem combinatorics.line.exists_mono_in_high_dimension (α : Type u) [finite α] (κ : Type v) [finite κ] :
∃ (ι : Type) [_inst_3 : fintype ι], ∀ (C : (ι → α) → κ), ∃ (l : combinatorics.line α ι), combinatorics.line.is_mono 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.

source
theorem combinatorics.exists_mono_homothetic_copy {M : Type u_1} {κ : Type u_2} [add_comm_monoid M] (S : finset M) [finite κ] (C : M → κ) :
∃ (a : ℕ) (H : a > 0) (b : M) (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.