Documentation

Mathlib.Combinatorics.HalesJewett

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 progression

References #

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.

Instances For
    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 α ι) :

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

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

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

      Instances For
        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.

        Instances For
          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.
          Instances For
            instance Combinatorics.Line.instInhabitedColorFocused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ιOption α) → κ) :
            def Combinatorics.Line.map {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : αα') (l : 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.

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

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

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

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

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

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

                  Instances For
                    theorem Combinatorics.Line.apply {α : Type u_1} {ι : Type u_2} (l : Combinatorics.Line α ι) (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) :
                    @[simp]
                    theorem Combinatorics.Line.map_apply {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : αα') (l : Combinatorics.Line α ι) (x : α) :
                    @[simp]
                    theorem Combinatorics.Line.vertical_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ια) (l : Combinatorics.Line α ι') (x : α) :
                    @[simp]
                    theorem Combinatorics.Line.horizontal_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : Combinatorics.Line α ι) (v : ι'α) (x : α) :
                    @[simp]
                    theorem Combinatorics.Line.prod_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : Combinatorics.Line α ι) (l' : Combinatorics.Line α ι') (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 SC (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.