3-Uniform Hypergraphs

This file defines the basic combinatorial infrastructure for 3-uniform hypergraphs used in formalizations of Erdős problems (e.g., Problem 593, Problem 1177).

Note: Mathlib does not yet have a general hypergraph API. The definitions here fill that gap for the special case of 3-uniform hypergraphs (every edge has exactly 3 vertices).

Main definitions

• ThreeUniformHypergraph V : a set of 3-element Finsets on a vertex type V
• ThreeUniformHypergraph.IsProperColoring : vertex coloring with no monochromatic edge
• ThreeUniformHypergraph.chromaticCardinal : minimum cardinality of a color type admitting a proper coloring (a Cardinal-valued chromatic number, distinguishing infinite values)
• ThreeUniformHypergraph.Appears : sub-hypergraph embedding (injective vertex map carrying edges to edges)
• ThreeUniformHypergraph.IsTwoColorable : vertex set has a 2-coloring with no monochromatic edge (also called Property B); the 3-uniform analogue of bipartiteness for graphs
• IsObligatory : a finite hypergraph appears in every hypergraph of chromatic cardinal > ℵ₀

References

• Erdős, Galvin, Hajnal, On set-systems having large chromatic number and not containing prescribed subsystems, Infinite and finite sets, 1975.

structure ThreeUniformHypergraph (V : Type) : Type

A 3-uniform hypergraph on vertex type V is a set of 3-element Finsets. Each element of edges is a hyperedge, and uniform ensures each has exactly 3 vertices.

Note: Mathlib does not yet have a general hypergraph API; this fills that gap for the 3-uniform case relevant to Erdős problems 593 and 1177.

• edges : Set (Finset V)

  The set of hyperedges: each edge is a 3-element finset of vertices.

• uniform (e : Finset V) : e ∈ self.edges → e.card = 3

  Every hyperedge has exactly 3 vertices.

def ThreeUniformHypergraph.IsProperColoring {V : Type} (H : ThreeUniformHypergraph V) {C : Type} (f : V → C) : Prop

A proper coloring of a 3-uniform hypergraph H by a color type C is a vertex coloring such that no hyperedge is monochromatic (all three vertices receive the same color).

Equations

• H.IsProperColoring f = ∀ e ∈ H.edges, ∃ u ∈ e, ∃ v ∈ e, f u ≠ f v

noncomputable def ThreeUniformHypergraph.chromaticCardinal {V : Type} (H : ThreeUniformHypergraph V) : Cardinal.{0}

The chromatic cardinal of a 3-uniform hypergraph H is the infimum of cardinalities of color types admitting a proper coloring.

In contrast to a ℕ∞-valued chromatic number, this Cardinal-valued definition distinguishes between different infinite chromatic numbers (e.g., ℵ₀ vs. ℵ₁). We work at Type (universe 0) throughout to avoid universe metavariable issues.

Equations

• H.chromaticCardinal = sInf {κ : Cardinal.{0} | ∃ (C : Type), Cardinal.mk C = κ ∧ ∃ (f : V → C), H.IsProperColoring f}

def ThreeUniformHypergraph.Appears {W V : Type} [DecidableEq V] (F : ThreeUniformHypergraph W) (H : ThreeUniformHypergraph V) : Prop

A finite 3-uniform hypergraph F appears in H (as a sub-hypergraph) if there exists an injective vertex map φ : W → V that sends every hyperedge of F to a hyperedge of H.

Equations

• F.Appears H = ∃ (φ : W → V), Function.Injective φ ∧ ∀ e ∈ F.edges, Finset.image φ e ∈ H.edges

def ThreeUniformHypergraph.IsTwoColorable {V : Type} (F : ThreeUniformHypergraph V) : Prop

A 3-uniform hypergraph F is 2-colorable (has Property B) if there exists a 2-coloring of its vertices with no monochromatic edge.

This is the hypergraph analogue of bipartiteness for graphs: a graph is bipartite iff it is 2-colorable as a graph. For 3-uniform hypergraphs, 2-colorability is a necessary condition for being obligatory (every obligatory finite 3-uniform hypergraph is 2-colorable).

Equations

• F.IsTwoColorable = ∃ (f : V → Fin 2), F.IsProperColoring f

def IsObligatory {W : Type} [Fintype W] (F : ThreeUniformHypergraph W) : Prop

A finite 3-uniform hypergraph F on a Fintype vertex type is obligatory if it appears in every 3-uniform hypergraph (on a Type-valued vertex set) whose chromatic cardinal exceeds ℵ₀.

Equations

• IsObligatory F = ∀ (V : Type) [inst : DecidableEq V] (H : ThreeUniformHypergraph V), Cardinal.aleph0 < H.chromaticCardinal → F.Appears H