Chains of closed sets, layers and traces

For a graph on an uncountable vertex type V, a chain is a continuous increasing family N ξ of vertex sets indexed by ordinals, starting from ∅, each successor closed over its predecessor, each set of size below #V while ξ < (#V).ord, and covering V by then. It replaces the chain of elementary submodels of the proof, with the first model empty and with length (#V).ord in place of the cofinality of #V.

The layer of a vertex v is the ordinal ξ with v ∈ N (ξ + 1) \ N ξ, and its trace is the set of its neighbours in N ξ, which contains every neighbour in an earlier layer.

structure Erdos111.Chain {V : Type u} (G : SimpleGraph V) : Type (u + 1)

A continuous chain of closed sets covering V, each of size below #V before (#V).ord.

• N : Ordinal.{u} → Set V

  The sets of the chain.

• zero : self.N 0 = ∅
• mono : Monotone self.N
• succ (ξ : Ordinal.{u}) : ClosedOver G (self.N ξ) (self.N (ξ + 1))
• limit (o : Ordinal.{u}) : Order.IsSuccLimit o → self.N o = ⋃ (ζ : Ordinal.{u}), ⋃ (_ : ζ < o), self.N ζ
• card_lt (ξ : Ordinal.{u}) : ξ < (Cardinal.mk V).ord → Cardinal.mk ↑(self.N ξ) < Cardinal.mk V
• cover (v : V) : ∃ ξ < (Cardinal.mk V).ord, v ∈ self.N (ξ + 1)

theorem Erdos111.Chain.exists_enum {V : Type u} [Nonempty V] : ∃ (e : Ordinal.{u} → V), ∀ (v : V), ∃ ξ < (Cardinal.mk V).ord, e ξ = v

A nonempty type is enumerated by the ordinals below (#V).ord.

noncomputable def Erdos111.Chain.closure {V : Type u} (G : SimpleGraph V) (S : Set V) (x : V) : Set V

A closure of S ∪ {x} over S.

Equations

• Erdos111.Chain.closure G S x = ⋯.choose

theorem Erdos111.Chain.subset_closure {V : Type u} (G : SimpleGraph V) (S : Set V) (x : V) : S ∪ {x} ⊆ closure G S x

The closure contains S ∪ {x}.

theorem Erdos111.Chain.closedOver_closure {V : Type u} (G : SimpleGraph V) (S : Set V) (x : V) : ClosedOver G S (closure G S x)

The closure is closed over S.

theorem Erdos111.Chain.mk_closure_le {V : Type u} (G : SimpleGraph V) (S : Set V) (x : V) : Cardinal.mk ↑(closure G S x) ≤ max (Cardinal.mk ↑S + 1) Cardinal.aleph0

The closure is small.

noncomputable def Erdos111.Chain.build {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) (o : Ordinal.{u}) : Set V

The chain adding the vertices of an enumeration e one at a time.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos111.Chain.build_zero {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) : build G e 0 = ∅

The chain starts from ∅.

theorem Erdos111.Chain.build_add_one {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) (ξ : Ordinal.{u}) : build G e (ξ + 1) = closure G (build G e ξ) (e ξ)

A successor set closes its predecessor with the next vertex.

theorem Erdos111.Chain.build_limit {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) : build G e o = ⋃ (ζ : Ordinal.{u}), ⋃ (_ : ζ < o), build G e ζ

A limit set is the union of the earlier sets.

theorem Erdos111.Chain.build_subset_build {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) (η ξ : Ordinal.{u}) : ξ ≤ η → build G e ξ ⊆ build G e η

The chain is increasing.

theorem Erdos111.Chain.build_mono {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) : Monotone (build G e)

The chain is monotone.

theorem Erdos111.Chain.mk_build_le {V : Type u} (G : SimpleGraph V) (e : Ordinal.{u} → V) (ξ : Ordinal.{u}) : Cardinal.mk ↑(build G e ξ) ≤ max ξ.card Cardinal.aleph0

The ξ-th set has at most max ξ.card ℵ₀ vertices.

theorem Erdos111.exists_chain {V : Type u} (G : SimpleGraph V) (hV : Cardinal.aleph0 < Cardinal.mk V) : Nonempty (Chain G)

Every graph on an uncountable vertex type has a chain.

noncomputable def Erdos111.Chain.layer {V : Type u} {G : SimpleGraph V} (c : Chain G) (v : V) : Ordinal.{u}

The layer of v: the ordinal ξ with v ∈ N (ξ + 1) \ N ξ.

Equations

• c.layer v = sInf {ξ : Ordinal.{?u.1} | v ∈ c.N (ξ + 1)}

def Erdos111.Chain.trace {V : Type u} {G : SimpleGraph V} (c : Chain G) (v : V) : Set V

The trace of v: its neighbours in the set preceding its layer.

Equations

• c.trace v = {u : V | G.Adj v u ∧ u ∈ c.N (c.layer v)}

theorem Erdos111.Chain.mem_N_iff {V : Type u} {G : SimpleGraph V} (c : Chain G) {v : V} {ξ : Ordinal.{u}} : v ∈ c.N ξ ↔ c.layer v < ξ

A vertex lies in N ξ exactly when its layer is below ξ.

theorem Erdos111.Chain.layer_lt_ord {V : Type u} {G : SimpleGraph V} (c : Chain G) (v : V) : c.layer v < (Cardinal.mk V).ord

Every layer is below (#V).ord.

theorem Erdos111.Chain.card_layer_lt {V : Type u} {G : SimpleGraph V} (c : Chain G) (hV : Cardinal.aleph0 ≤ Cardinal.mk V) (ξ : Ordinal.{u}) : Cardinal.mk { v : V // c.layer v = ξ } < Cardinal.mk V

Every layer has fewer than #V vertices, when V is infinite.

theorem Erdos111.Chain.mem_trace_of_layer_lt {V : Type u} {G : SimpleGraph V} (c : Chain G) {u v : V} (h : G.Adj v u) (hl : c.layer u < c.layer v) : u ∈ c.trace v

A neighbour in an earlier layer lies in the trace.