Erdős Problem 593

References:

• erdosproblems.com/593
• [EGH75] Erdős, Paul and Galvin, Fred and Hajnal, András, On set-systems having large chromatic number and not containing prescribed subsystems. Infinite and finite sets (Colloq., Keszthely, 1973; dedicated to P. Erdős on his 60th birthday), Vol. I. Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 425–513.
• [Er95d] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) 47 (1992), no. 2, 231–240 (1995).

theorem Erdos593.erdos_593 : True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorable

Erdős Problem 593 ($500): Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$.

A natural conjectural characterization, recorded here, is that the obligatory finite 3-uniform hypergraphs are exactly the 2-colorable ones (Property B). The forward direction (IsObligatory → IsTwoColorable) and converse (IsTwoColorable → IsObligatory) are stated as separate variants below; in the graph case ($r = 2$), Erdős–Galvin–Hajnal [EGH75] proved the analogous result (obligatory ⇔ bipartite).

theorem Erdos593.erdos_593.variants.obligatory_implies_two_colorable : True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorable

Erdős Problem 593 — Necessary direction: Every obligatory finite 3-uniform hypergraph is 2-colorable.

This is the natural necessary condition for the conjectural characterization in erdos_593: if a finite 3-uniform hypergraph F is not 2-colorable, one expects to construct a hypergraph with large chromatic number that contains no copy of F.

theorem Erdos593.erdos_593.variants.two_colorable_implies_obligatory : True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F

Erdős Problem 593 — Sufficient direction: Every finite 2-colorable 3-uniform hypergraph is obligatory.

This is the converse direction of the erdos_593 characterization: if 2-colorability matches the graph-case characterization (bipartite ⇔ obligatory), then every 2-colorable finite 3-uniform hypergraph must appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$.

Together with erdos_593.variants.obligatory_implies_two_colorable, this implies erdos_593.

theorem Erdos593.erdos_593.variants.implications_combine (h₁ : ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorable) (h₂ : ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F) (W : Type) [Fintype W] (F : ThreeUniformHypergraph W) : IsObligatory F ↔ F.IsTwoColorable

Conjunction of the two open implications gives the conjectured characterization: if both obligatory_implies_two_colorable and two_colorable_implies_obligatory hold, then the characterization conjectured in erdos_593 (IsObligatory F ↔ F.IsTwoColorable) follows by elementary Iff manipulation.

theorem Erdos593.erdos_593.variants.graph_case_bipartite_obligatory : True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → Nonempty (F ↪g G)

Graph analogue — bipartite graphs are obligatory (Erdős–Galvin–Hajnal [EGH75]): For the 2-uniform (graph) case, a graph of chromatic cardinal $> \aleph_0$ must contain all finite bipartite graphs. Specifically, for every finite bipartite graph F and every graph G with chromatic cardinal $> \aleph_0$, there is a graph embedding from F into G.

This uses Nonempty (F ↪g G) (graph embedding), aligned with the injective vertex map used in the hypergraph Appears definition.

theorem Erdos593.erdos_593.variants.graph_case_no_odd_cycle : True ↔ ∀ (k : ℕ), Odd k → 3 ≤ k → ∃ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 ∧ IsEmpty (SimpleGraph.cycleGraph k →g G)

Graph analogue — no odd cycle is obligatory (Erdős–Galvin–Hajnal [EGH75]): For every odd $k \geq 3$, there exists a graph with chromatic cardinal $\aleph_1$ that contains no cycle of length $k$. This shows the class of obligatory graphs is strictly smaller than all finite graphs.

theorem Erdos593.erdos_593.variants.uncountable_vertices_if_large_chromatic {V : Type} (H : ThreeUniformHypergraph V) (hχ : Cardinal.aleph0 < H.chromaticCardinal) : ¬Countable V

Vertices must be uncountable: Every 3-uniform hypergraph with chromatic cardinal $> \aleph_0$ must have an uncountable vertex set.

Proof: If V is countable, there exists an injection φ : V → ℕ. Using distinct natural numbers as colors gives a proper coloring, so $\chi(H) \leq \#\mathbb{N} = \aleph_0$, contradicting $\chi(H) > \aleph_0$.

theorem Erdos593.erdos_593.variants.nonempty_edges_if_large_chromatic {V : Type} (H : ThreeUniformHypergraph V) (hχ : Cardinal.aleph0 < H.chromaticCardinal) : H.edges.Nonempty

No hyperedges implies chromatic cardinal ≤ 1: A 3-uniform hypergraph with no edges can be properly colored with a single color, so its chromatic cardinal is at most 1. In particular, $\chi(H) > \aleph_0$ implies H has at least one hyperedge.

theorem Erdos593.erdos_593.variants.obligatory_monotone {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] [DecidableEq W₂] {F₁ : ThreeUniformHypergraph W₁} {F₂ : ThreeUniformHypergraph W₂} (h12 : F₁.Appears F₂) (hObl : IsObligatory F₂) : IsObligatory F₁

Monotonicity of the obligatory property: If F₁ appears in F₂ and F₂ is obligatory, then F₁ is also obligatory.

Proof: For any H with $\chi(H) > \aleph_0$, since F₂ is obligatory, F₂ appears in H via some injection φ₂. Since F₁ appears in F₂ via φ₁, the composition φ₂ ∘ φ₁ witnesses that F₁ appears in H.

theorem Erdos593.erdos_593.variants.empty_hypergraph_obligatory : IsObligatory { edges := ∅, uniform := ⋯ }

The empty hypergraph is trivially obligatory: The 3-uniform hypergraph on PEmpty (no vertices, no edges) appears in every hypergraph via the empty injection.

This degenerate case confirms the definition is well-formed.