Erdős Problem 1167

Reference: erdosproblems.com/1167

The original Erdős–Hajnal problem list gives the additional conditions $\gamma \geq 2$, $r < \omega$, and $\kappa_\alpha > r$. Without $\gamma \geq 2$, the statement is false: taking $\gamma = 1$ and $\kappa_0 = \aleph_1$ with $\lambda = \aleph_0$ gives a counterexample, since the partition relation with one color degenerates to a cardinality comparison (see erdos_1167.unrestricted_is_false).

theorem Erdos1167.erdos_1167 : sorry ↔ ∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), Cardinal.aleph0 ≤ lam → ∀ (γ : Ordinal.{u}), 2 ≤ γ → ∀ (κ : γ.ToType → Cardinal.{u}), (Combinatorics.cardinalPartitionRel (2 ^ lam) (r + 1) γ fun (α : γ.ToType) => κ α + 1) → Combinatorics.cardinalPartitionRel lam r γ κ

Erdős Problem 1167. Let $r \geq 2$ be finite, $\gamma \geq 2$, and $\lambda$ be an infinite cardinal. Let $\kappa_\alpha$ be cardinals for all $\alpha < \gamma$. Is it true that $$2^\lambda \to (\kappa_\alpha + 1)_{\alpha < \gamma}^{r+1}$$ implies $$\lambda \to (\kappa_\alpha)_{\alpha < \gamma}^r?$$ Here $+$ means cardinal addition, so that $\kappa_\alpha + 1 = \kappa_\alpha$ if $\kappa_\alpha$ is infinite.

A problem of Erdős, Hajnal, and Rado.

theorem Erdos1167.erdos_1167.variants.finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : Cardinal.aleph0 ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) : (Combinatorics.cardinalPartitionRel (2 ^ lam) (r + 1) γ fun (α : γ.ToType) => ↑(n α) + 1) → Combinatorics.cardinalPartitionRel lam r γ fun (α : γ.ToType) => ↑(n α)

Finite-target case. When all $\kappa_\alpha$ are finite, $\kappa_\alpha + 1$ is the ordinary natural-number successor. Special case of erdos_1167.

theorem Erdos1167.erdos_1167.variants.binary_colors (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : Cardinal.aleph0 ≤ lam) (κ : Ordinal.ToType 2 → Cardinal.{u}) : (Combinatorics.cardinalPartitionRel (2 ^ lam) (r + 1) 2 fun (α : Ordinal.ToType 2) => κ α + 1) → Combinatorics.cardinalPartitionRel lam r 2 κ

Binary-color case. The $\gamma = 2$ specialization (two color classes).

theorem Erdos1167.erdos_1167.variants.infinite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : Cardinal.aleph0 ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ (i : γ.ToType), Cardinal.aleph0 ≤ κ i) (hκ_le : ∀ (i : γ.ToType), κ i ≤ lam) : Combinatorics.cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → Combinatorics.cardinalPartitionRel lam r γ κ

Infinite-target case. When all $\kappa_\alpha \geq \aleph_0$ are infinite and bounded by $\lambda$, $\kappa_\alpha + 1 = \kappa_\alpha$, so the hypothesis simplifies to a "pure" stepping-down lemma: $$2^\lambda \to (\kappa_\alpha)_{\alpha<\gamma}^{r+1} \implies \lambda \to (\kappa_\alpha)_{\alpha<\gamma}^r.$$ The condition $\kappa_\alpha \leq \lambda$ is needed to avoid a size obstruction: without it, the conclusion would require a subset of $\lambda$ of size $\kappa_\alpha > \lambda$, which is impossible (see infinite_targets_needs_bound).

theorem Erdos1167.erdos_1167.variants.r_eq_two (lam : Cardinal.{u}) (hlam : Cardinal.aleph0 ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) : (Combinatorics.cardinalPartitionRel (2 ^ lam) 3 γ fun (α : γ.ToType) => κ α + 1) → Combinatorics.cardinalPartitionRel lam 2 γ κ

$r = 2$ case. The stepping-down from 3-uniform to 2-uniform partition relations: $2^\lambda \to (\kappa_\alpha + 1)_{\alpha<\gamma}^3$ implies $\lambda \to (\kappa_\alpha)_{\alpha<\gamma}^2$. Generalises the classical Erdős–Rado stepping-up/down theorem for pairs.

noncomputable def Erdos1167.i0 : Ordinal.ToType 1

A canonical element of the type (1 : Ordinal).ToType.

Equations

• Erdos1167.i0 = default

theorem Erdos1167.cardinalPartitionRel_one (μ : Cardinal.{u}) (r : ℕ) (ν : Ordinal.ToType 1 → Cardinal.{u}) : Combinatorics.cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν i0

The partition relation $\mu \to (\nu)^r_1$ with a single color is equivalent to $\nu \le \mu$.

theorem Erdos1167.erdos_1167.unrestricted_is_false : ¬∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), Cardinal.aleph0 ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (Combinatorics.cardinalPartitionRel (2 ^ lam) (r + 1) γ fun (α : γ.ToType) => κ α + 1) → Combinatorics.cardinalPartitionRel lam r γ κ

The unrestricted version of Erdős Problem 1167 (without the condition $\gamma \geq 2$ from the original Erdős–Hajnal list) is false. Taking $\gamma = 1$, $\kappa_0 = \aleph_1$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (\aleph_1 + 1)^3_1$ holds since $2^{\aleph_0} \geq \aleph_1$, but the conclusion $\aleph_0 \to (\aleph_1)^2_1$ fails since $\aleph_0 < \aleph_1$.

theorem Erdos1167.erdos_1167.variants.infinite_targets_needs_bound : ¬∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), Cardinal.aleph0 ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), Cardinal.aleph0 ≤ κ i) → Combinatorics.cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → Combinatorics.cardinalPartitionRel lam r γ κ

The infinite_targets variant without the bound $\kappa_\alpha \leq \lambda$ is false. Taking $\gamma = 1$, $\kappa_0 = 2^{\aleph_0}$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (2^{\aleph_0})^3_1$ holds since $2^{\aleph_0} \leq 2^{\aleph_0}$, but the conclusion $\aleph_0 \to (2^{\aleph_0})^2_1$ fails by Cantor's theorem.