Closure over a set: replication of finite extensions

The proof uses elementary submodels only through replication: a finite configuration whose new vertices lie outside the previous model has a copy, with the same diagram over its roots, inside the next model. ClosedOver G M N states exactly this property of the next model N over the previous model M, with an additional finite set D ⊆ N to avoid, so that copies can be chosen pairwise disjoint.

A closure of M ∪ X over M is built in ω rounds, adding one witness for each finite diagram over finite sets of roots and avoided vertices, so its size is at most max (#M + #X) ℵ₀.

def Erdos111.SameDiagram {V : Type u_1} (G : SimpleGraph V) (R : Finset V) {m : ℕ} (f g : Fin m → V) : Prop

g realizes over R the same finite diagram as f: the same adjacencies among the new vertices and between the new vertices and the roots.

Equations

• Erdos111.SameDiagram G R f g = ((∀ (i j : Fin m), G.Adj (f i) (f j) ↔ G.Adj (g i) (g j)) ∧ ∀ (i : Fin m), ∀ r ∈ R, G.Adj (f i) r ↔ G.Adj (g i) r)

def Erdos111.ClosedOver {V : Type u_1} (G : SimpleGraph V) (M N : Set V) : Prop

N is closed over M: it contains M, and every finite configuration with roots R ⊆ N whose new vertices avoid M, a finite D ⊆ N and R has a copy with the same diagram over R inside N, still avoiding M, D and R.

Equations

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

@[reducible, inline]

abbrev Erdos111.Closure.Request {V : Type u_1} (S : Set V) : Type u_1

A request over S: finite sets of roots and of avoided vertices in S, and the number of new vertices.

Equations

• Erdos111.Closure.Request S = (Finset ↑S × Finset ↑S × ℕ)

@[reducible, inline]

abbrev Erdos111.Closure.Diagram {V : Type u_1} {S : Set V} (p : Request S) : Type u_1

A finite diagram for a request: the adjacencies among the new vertices and between the new vertices and the roots.

Equations

• Erdos111.Closure.Diagram p = ((Fin p.2.2 → Fin p.2.2 → Bool) × (Fin p.2.2 → ↥p.1 → Bool))

def Erdos111.Closure.Realizes {V : Type u_1} (G : SimpleGraph V) (M : Set V) {S : Set V} (p : Request S) (d : Diagram p) (g : Fin p.2.2 → V) : Prop

g realizes the diagram d of the request p, with new vertices avoiding M, the avoided vertices and the roots.

Equations

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

noncomputable def Erdos111.Closure.witness {V : Type u_1} (G : SimpleGraph V) (M : Set V) {S : Set V} (p : Request S) (d : Diagram p) : Set V

The new vertices of one realization of the diagram d, when there is one.

Equations

• Erdos111.Closure.witness G M p d = if h : ∃ (g : Fin p.2.2 → V), Erdos111.Closure.Realizes G M p d g then Set.range h.choose else ∅

theorem Erdos111.Closure.witness_finite {V : Type u_1} (G : SimpleGraph V) (M : Set V) {S : Set V} (p : Request S) (d : Diagram p) : (witness G M p d).Finite

A witness is finite.

theorem Erdos111.Closure.exists_realizes_subset_witness {V : Type u_1} {G : SimpleGraph V} {M S : Set V} {p : Request S} {d : Diagram p} (h : ∃ (g : Fin p.2.2 → V), Realizes G M p d g) : ∃ (g : Fin p.2.2 → V), Realizes G M p d g ∧ Set.range g ⊆ witness G M p d

A realizable diagram has a realization inside its witness.

noncomputable def Erdos111.Closure.step {V : Type u_1} (G : SimpleGraph V) (M S : Set V) : Set V

One round over S: add a realization of every realizable diagram over S.

Equations

• Erdos111.Closure.step G M S = S ∪ ⋃ (p : Erdos111.Closure.Request S), ⋃ (d : Erdos111.Closure.Diagram p), Erdos111.Closure.witness G M p d

noncomputable def Erdos111.Closure.rounds {V : Type u_1} (G : SimpleGraph V) (M X : Set V) : ℕ → Set V

The rounds of the closure of M ∪ X over M.

Equations

• Erdos111.Closure.rounds G M X 0 = M ∪ X
• Erdos111.Closure.rounds G M X n.succ = Erdos111.Closure.step G M (Erdos111.Closure.rounds G M X n)

theorem Erdos111.Closure.mk_step_le {V : Type u_1} (G : SimpleGraph V) (M : Set V) {S : Set V} {κ : Cardinal.{u_1}} (hκ : Cardinal.aleph0 ≤ κ) (hS : Cardinal.mk ↑S ≤ κ) : Cardinal.mk ↑(step G M S) ≤ κ

A round keeps a set of size at most an infinite κ of size at most κ.

theorem Erdos111.exists_closedOver {V : Type u_1} (G : SimpleGraph V) (M X : Set V) : ∃ (N : Set V), M ∪ X ⊆ N ∧ ClosedOver G M N ∧ Cardinal.mk ↑N ≤ max (Cardinal.mk ↑M + Cardinal.mk ↑X) Cardinal.aleph0

Every M ∪ X lies in a set closed over M of size at most max (#M + #X) ℵ₀.