Hindman's theorem on finite sums #
We prove Hindman's theorem on finite sums, using idempotent ultrafilters.
Given an infinite sequence a₀, a₁, a₂, …
of positive integers, the set FS(a₀, …)
is the set
of positive integers that can be expressed as a finite sum of aᵢ
's, without repetition. Hindman's
theorem asserts that whenever the positive integers are finitely colored, there exists a sequence
a₀, a₁, a₂, …
such that FS(a₀, …)
is monochromatic. There is also a stronger version, saying
that whenever a set of the form FS(a₀, …)
is finitely colored, there exists a sequence
b₀, b₁, b₂, …
such that FS(b₀, …)
is monochromatic and contained in FS(a₀, …)
. We prove both
these versions for a general semigroup M
instead of ℕ+
since it is no harder, although this
special case implies the general case.
The idea of the proof is to extend the addition (+) : M → M → M
to addition (+) : βM → βM → βM
on the space βM
of ultrafilters on M
. One can prove that if U
is an idempotent ultrafilter,
i.e. U + U = U
, then any U
-large subset of M
contains some set FS(a₀, …)
(see
exists_FS_of_large
). And with the help of a general topological argument one can show that any set
of the form FS(a₀, …)
is U
-large according to some idempotent ultrafilter U
(see
exists_idempotent_ultrafilter_le_FS
). This is enough to prove the theorem since in any finite
partition of a U
-large set, one of the parts is U
-large.
Main results #
FS_partition_regular
: the strong form of Hindman's theoremexists_FS_of_finite_cover
: the weak form of Hindman's theorem
Tags #
Ramsey theory, ultrafilter
Addition of ultrafilters given by ∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m')
.
Equations
Instances For
Multiplication of ultrafilters given by ∀ᶠ m in U*V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m*m')
.
Equations
Instances For
Additive semigroup structure on Ultrafilter M
induced by an additive semigroup
structure on M
.
Equations
- Ultrafilter.addSemigroup = AddSemigroup.mk ⋯
Instances For
Semigroup structure on Ultrafilter M
induced by a semigroup structure on M
.
Equations
- Ultrafilter.semigroup = Semigroup.mk ⋯
Instances For
FS a
is the set of finite sums in a
, i.e. m ∈ FS a
if m
is the sum of a nonempty
subsequence of a
. We give a direct inductive definition instead of talking about subsequences.
- head: ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M), Hindman.FS a a.head
- tail: ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (m : M), Hindman.FS a.tail m → Hindman.FS a m
- cons: ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (m : M), Hindman.FS a.tail m → Hindman.FS a (a.head + m)
Instances For
FP a
is the set of finite products in a
, i.e. m ∈ FP a
if m
is the product of a nonempty
subsequence of a
. We give a direct inductive definition instead of talking about subsequences.
- head: ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M), Hindman.FP a a.head
- tail: ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → Hindman.FP a m
- cons: ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → Hindman.FP a (a.head * m)
Instances For
If m
and m'
are finite sums in M
, then so is m + m'
, provided that m'
is obtained from a subsequence of M
starting sufficiently late.
If m
and m'
are finite products in M
, then so is m * m'
, provided that m'
is obtained
from a subsequence of M
starting sufficiently late.
The strong form of Hindman's theorem: in any finite cover of an FS-set, one the parts contains an FS-set.
The strong form of Hindman's theorem: in any finite cover of an FP-set, one the parts contains an FP-set.
The weak form of Hindman's theorem: in any finite cover of a nonempty additive semigroup, one of the parts contains an FS-set.
The weak form of Hindman's theorem: in any finite cover of a nonempty semigroup, one of the parts contains an FP-set.