Erdős Problem 918

References:

• erdosproblems.com/918
• [ErHa68b] Erdős, P. and Hajnal, A., On chromatic number of infinite graphs. (1968), 83--98.
• [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35.

theorem Erdos918.erdos_918.parts.i : (∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph 1 → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0) ↔ sorry

Is there a graph with $\aleph_2$ vertices and chromatic number $\aleph_2$ such that every subgraph on $\aleph_1$ vertices has chromatic number $\leq\aleph_0$?

theorem Erdos918.erdos_918.parts.ii (ω : Ordinal.{u}) : (∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph (ω + 1) ∧ G.chromaticCardinal = Cardinal.aleph 1 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph ω → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0) ↔ sorry

Is there a graph with $\aleph_{\omega+1}$ vertices and chromatic number $\aleph_1$ such that every subgraph on $\aleph_\omega$ vertices has chromatic number $\leq\aleph_0$?

theorem Erdos918.erdos_918.variants.all_subgraphs.parts.i : (∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (H : G.Subgraph), Cardinal.mk ↑H.verts = Cardinal.aleph 1 → H.coe.chromaticCardinal ≤ Cardinal.aleph0) ↔ sorry

Is there a graph with $\aleph_2$ vertices and chromatic number $\aleph_2$ such that every subgraph on $\aleph_1$ vertices has chromatic number $\leq\aleph_0$?

theorem Erdos918.erdos_918.variants.all_subgraphs.parts.ii (ω : Ordinal.{u}) : (∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph (ω + 1) ∧ G.chromaticCardinal = Cardinal.aleph 1 ∧ ∀ (H : G.Subgraph), Cardinal.mk ↑H.verts = Cardinal.aleph ω → H.coe.chromaticCardinal ≤ Cardinal.aleph0) ↔ sorry

Is there a graph with $\aleph_{\omega+1}$ vertices and chromatic number $\aleph_1$ such that every subgraph on $\aleph_\omega$ vertices has chromatic number $\leq\aleph_0$?

theorem Erdos918.erdos_918.variants.erdos_hajnal (k : ℕ) : ∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph ↑k ∧ G.chromaticCardinal = Cardinal.aleph 1 ∧ ∀ (W : Set V), Cardinal.mk ↑W < Cardinal.aleph ↑k → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0

A question of Erd\H{o}s and Hajnal [ErHa68b], who proved that for every finite $k$ there is a graph with chromatic number $\aleph_1$ and $\aleph_k$ vertices where each subgraph on less than $\aleph_k$ vertices has chromatic number $\leq \aleph_0$.

theorem Erdos918.erdos_918.variants.eq_aleph_0.parts.i : ¬∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph 1 → (SimpleGraph.induce W G).chromaticCardinal = Cardinal.aleph0

In [ErHa69] the questions are stated with $= \aleph_0$ rather than $\leq\aleph_0$. This is a likely typo since it can be shown that no such graph exists in this case.

This is the first question with induced subgraphs.

theorem Erdos918.erdos_918.variants.eq_aleph_0_all_subgraphs.parts.i : ¬∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (H : G.Subgraph), Cardinal.mk ↑H.verts = Cardinal.aleph 1 → H.coe.chromaticCardinal = Cardinal.aleph0

In [ErHa69] the questions are stated with $= \aleph_0$ rather than $\leq\aleph_0$. This is a likely typo since it can be shown that no such graph exists in this case.

This is the first question with all subgraphs.

theorem Erdos918.erdos_918.variants.eq_aleph_0.parts.ii (ω : Ordinal.{u}) : ¬∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph (ω + 1) ∧ G.chromaticCardinal = Cardinal.aleph 1 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph ω → (SimpleGraph.induce W G).chromaticCardinal = Cardinal.aleph0

In [ErHa69] the questions are stated with $= \aleph_0$ rather than $\leq\aleph_0$. This is a likely typo since it can be shown that no such graph exists in this case.

This is the second question with induced subgraphs.

theorem Erdos918.erdos_918.variants.eq_aleph_0_all_subgraphs.parts.ii (ω : Ordinal.{u}) : ¬∃ (V : Type u) (G : SimpleGraph V), Cardinal.mk V = Cardinal.aleph (ω + 1) ∧ G.chromaticCardinal = Cardinal.aleph 1 ∧ ∀ (H : G.Subgraph), Cardinal.mk ↑H.verts = Cardinal.aleph ω → H.coe.chromaticCardinal = Cardinal.aleph0

In [ErHa69] the questions are stated with $= \aleph_0$ rather than $\leq\aleph_0$. This is a likely typo since it can be shown that no such graph exists in this case.

This is the second question with all subgraphs.