2-better-quasi-orders (2-BQO)

A formalization of 2-better-quasi-orders, following Pequignot, Towards better: A motivated introduction to better-quasi-orders, EMS Surveys 2017. A 2-BQO is a strengthening of well-quasi-order (WQO) phrased via pair-sequences f : ∀ m n, m < n → α instead of plain sequences: r is 2-BQO if every pair-sequence has a good triple m < n < l with r (f m n) (f n l).

2-BQO implies WQO (TwoBQO.wellQuasiOrdered), and unlike WQO it is closed under several constructions that WQO alone is not known to be closed under, most importantly forming an infinite sum indexed by a 2-BQO (TwoBQO.lexSigmaQO) and passing to sequences under a suitable embedding relation (TwoBQO.embedForAll_wqo).

Main definitions

• PairSeq α: a pair-sequence, assigning a value to every pair m < n of naturals.
• TwoBQO r: r is 2-BQO if every pair-sequence has a good triple.
• DomOrder r X Y: X dominates into Y, i.e. every element of X is r-below some element of Y.
• EmbedForAll r: the pointwise-embedding preorder on sequences ℕ → α induced by r.
• TwoBQO.LexSumRelQO r s t: the lexicographic sum of quasi-orders t i on s i, ordered along r on the index type.

Main results

• TwoBQO.wellQuasiOrdered: 2-BQO implies WQO.
• TwoBQO.of_finite_coloring: a preorder with a finite partial order quotient is 2-BQO.
• TwoBQO.of_wellFoundedLT: well-founded linear orders are 2-BQO.
• Ordinal.isTwoBQO: ordinals are 2-BQO.
• TwoBQO.comap, TwoBQO.mono: 2-BQO is closed under monotone preimage and relation weakening.
• TwoBQO.union: closure under covering by two 2-BQO parts.
• TwoBQO.prod, TwoBQO.pi: closure under finite products.
• TwoBQO.lexSigmaQO: closure under lexicographic sum along a 2-BQO index.
• TwoBQO.dom_twoBQO: the domination order on subsets of a 2-BQO is WQO.
• TwoBQO.embedForAll_wqo: EmbedForAll r is WQO on ℕ → Q whenever r is 2-BQO on Q.

Bad pair-sequences and 2-BQO

@[reducible, inline]

abbrev PairSeq (α : Type u_1) : Type u_1

A pair-sequence in α assigns a value to every pair (m, n) with m < n.

Equations

• PairSeq α = ((m n : ℕ) → m < n → α)

def PairSeq.restrict {α : Type u_1} (f : PairSeq α) (e : ℕ → ℕ) (he_mono : StrictMono e) : PairSeq α

Restrict a pair-sequence along a strictly monotone reindexing.

Equations

• f.restrict e he_mono m n hmn = f (e m) (e n) ⋯

def PairSeq.IsBad {α : Type u_1} (r : α → α → Prop) (f : PairSeq α) : Prop

A pair-sequence f is bad for r if f (m, n) and f (n, l) are never r-related.

Equations

• PairSeq.IsBad r f = ∀ (m n l : ℕ) (hmn : m < n) (hnl : n < l), ¬r (f m n hmn) (f n l hnl)

def PairSeq.IsPerfect {α : Type u_1} (r : α → α → Prop) (f : PairSeq α) : Prop

A pair-sequence f is perfect for r if f (m, n) and f (n, l) are always r-related.

Equations

• PairSeq.IsPerfect r f = ∀ (m n l : ℕ) (hmn : m < n) (hnl : n < l), r (f m n hmn) (f n l hnl)

theorem PairSeq.perfect_or_bad {α : Type u_1} (r : α → α → Prop) (f : PairSeq α) : ∃ (e : ℕ → ℕ) (he_mono : StrictMono e), IsPerfect r (f.restrict e he_mono) ∨ IsBad r (f.restrict e he_mono)

Every pair-sequence has a restriction that is perfect or bad for r: colour each triple h < i < j by whether r (f h i) (f i j) holds and apply infinite_ramsey_triples.

def TwoBQON {α : Type u_1} (r : α → α → Prop) : Prop

r is 2-BQO if there is no bad pair-sequence for r.

Equations

• TwoBQON r = ¬∃ (f : PairSeq α), PairSeq.IsBad r f

def TwoBQO {α : Type u_1} (r : α → α → Prop) : Prop

r is 2-BQO if every pair-sequence has a good triple m < n < l, i.e. r (f m n) (f n l).

Equations

• TwoBQO r = ∀ (f : PairSeq α), ∃ (m : ℕ) (n : ℕ) (l : ℕ) (hmn : m < n) (hnl : n < l), r (f m n hmn) (f n l hnl)

theorem TwoBQO.iff_noBad {α : Type u_1} (r : α → α → Prop) : TwoBQO r ↔ TwoBQON r

2-BQO implies WQO

theorem TwoBQO.wellQuasiOrdered {α : Type u_1} {r : α → α → Prop} (h : TwoBQO r) : WellQuasiOrdered r

2-BQO implies WQO. Given a sequence g : ℕ → α, apply 2-BQO to the pair-sequence (m, n, _) ↦ g m. A good triple m < n < l yields r (g m) (g n).

Finite preorders are TwoBQO

theorem TwoBQO.of_finite_coloring {α : Type u_1} {κ : Type u_2} [Finite κ] (r : α → α → Prop) (c : α → κ) (hc : ∀ (a b : α), c a = c b → r a b) : TwoBQO r

A preorder with a finite partial order quotient is 2-BQO. If c : α → κ with κ finite and same colour ⟹ r-related, then r is 2-BQO: colour pairs by c (f m n), Ramsey-for-pairs (infinite_ramsey_pairs) makes the restriction monochromatic, so any triple is good. In particular, if r is a preorder whose induced partial order on r-equivalence classes has finitely many classes, taking c to be the quotient map gives TwoBQO r.

Well-orders are 2-BQO

theorem TwoBQO.of_wellFoundedLT {α : Type u_1} [LinearOrder α] [WellFoundedLT α] : TwoBQO fun (x1 x2 : α) => x1 ≤ x2

Well-orders are 2-BQO. If f is bad for a well-order <, the sequence n ↦ f (n, n+1) is strictly decreasing, contradicting well-foundedness.

theorem Ordinal.isTwoBQO : TwoBQO fun (x1 x2 : Ordinal.{u_1}) => x1 ≤ x2

Ordinals are 2-BQO with respect to ≤.

Closure properties

Monotone preimage (downward closure)

theorem TwoBQO.comap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (h : TwoBQO r) (φ : β → α) : TwoBQO fun (a b : β) => r (φ a) (φ b)

2-BQO is closed under monotone preimage: if φ : β → α is monotone and r on α is 2-BQO, then the pullback of r along φ is 2-BQO.

theorem TwoBQO.subtype {α : Type u_1} {r : α → α → Prop} (h : TwoBQO r) (p : α → Prop) : TwoBQO fun (a b : Subtype p) => r ↑a ↑b

Subtype closure.

theorem TwoBQO.mono {α : Type u_1} {r s : α → α → Prop} (h : TwoBQO r) (hincl : ∀ (a b : α), r a b → s a b) : TwoBQO s

Union of two parts

Rests on Ramsey for pairs (infinite_ramsey_pairs): a 2-colouring of pairs by which part the single value f m n lands in has an infinite homogeneous restriction, on which the relevant 2-BQO gives a good triple.

theorem TwoBQO.union {α : Type u_1} (r : α → α → Prop) (p q : α → Prop) (hcover : ∀ (a : α), p a ∨ q a) (hp : TwoBQO fun (a b : { x : α // p x }) => r ↑a ↑b) (hq : TwoBQO fun (a b : { x : α // q x }) => r ↑a ↑b) : TwoBQO r

Union of two 2-BQO parts is 2-BQO. If p, q cover α and r is 2-BQO on each sub-part {x // p x} and {x // q x}, then r is 2-BQO on α.

2-colour each pair (m,n) by whether p (f m n) holds; Ramsey-for-pairs gives an infinite restriction landing wholly in one part, where the corresponding 2-BQO supplies a good triple.

Finite products (Dickson's lemma for 2-BQO)

theorem TwoBQO.prod {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (hr : TwoBQO r) (hs : TwoBQO s) : TwoBQO fun (x y : α × β) => r x.1 y.1 ∧ s x.2 y.2

Product closure (Dickson's lemma for 2-BQO). If r on α and s on β are 2-BQO, then the componentwise product fun (a₁,b₁) (a₂,b₂) => r a₁ a₂ ∧ s b₁ b₂ on α × β is 2-BQO.

theorem TwoBQO.pi (n : ℕ) (α : Fin n → Type u_1) (r : (i : Fin n) → α i → α i → Prop) : (∀ (i : Fin n), TwoBQO (r i)) → TwoBQO fun (f g : (i : Fin n) → α i) => ∀ (i : Fin n), r i (f i) (g i)

Iterated finite product. For a Fintype index ι, the product ∀ i, α i with pointwise quasi-order is 2-BQO when each component is.

theorem TwoBQO.prodN (n : ℕ) : TwoBQO fun (f g : Fin n → ℕ) => ∀ (i : Fin n), f i ≤ g i

Sum along a 2-BQO (the main closure theorem)

Setup. Given a quasi-order r on ι and quasi-orders s i on α i, the sum Σᵢ αᵢ is ordered by (i, x) ≤ (j, y) iff r i j ∧ i ≠ j (strictly above), or i = j ∧ s i x y (same fibre). This is Pequignot's Proposition 2.4(iii) lifted to 2-BQO.

def TwoBQO.LexSumRelQO {ι : Type u_1} (r : ι → ι → Prop) (s : ι → Type u_2) (t : (i : ι) → s i → s i → Prop) : (i : ι) × s i → (i : ι) × s i → Prop

The lexicographic sum order along a partial order on Σ i, α i: (i,x) ≤ (j,y) iff r i j and i ≠ j (strictly above in r), or i = j and x ≤ y in t i.

Equations

• TwoBQO.LexSumRelQO r s t ⟨i, x_2⟩ ⟨j, y⟩ = (r i j ∧ i ≠ j ∨ ∃ (h : i = j), t i x_2 (⋯ ▸ y))

theorem TwoBQO.LexSumRelQO.refl {ι : Type u_1} (r : ι → ι → Prop) (s : ι → Type u_2) (t : (i : ι) → s i → s i → Prop) (ht_refl : ∀ (i : ι) (x : s i), t i x x) (σ : (i : ι) × s i) : LexSumRelQO r s t σ σ

TwoBQO.LexSumRelQO r s t is reflexive whenever each t i is.

theorem TwoBQO.LexSumRelQO.trans {ι : Type u_1} (r : ι → ι → Prop) (s : ι → Type u_2) (t : (i : ι) → s i → s i → Prop) (hr_refl : ∀ (i : ι), r i i) (hr_antisymm : ∀ (i j : ι), r i j → r j i → i = j) (hr_trans : ∀ (i j k : ι), r i j → r j k → r i k) (ht_trans : ∀ (i : ι) (x y z : s i), t i x y → t i y z → t i x z) {σ₁ σ₂ σ₃ : (i : ι) × s i} (h₁₂ : LexSumRelQO r s t σ₁ σ₂) (h₂₃ : LexSumRelQO r s t σ₂ σ₃) : LexSumRelQO r s t σ₁ σ₃

TwoBQO.LexSumRelQO r s t is transitive whenever r is reflexive, antisymmetric, and transitive, and each t i is transitive.

theorem TwoBQO.lexSigmaQO_reflect {ι : Type u_3} (r : ι → ι → Prop) (s : ι → Type u_4) (t : (i : ι) → s i → s i → Prop) (f : PairSeq ((i : ι) × s i)) (hf_bad : PairSeq.IsBad (LexSumRelQO r s t) f) : ∃ (e : ℕ → ℕ) (he_mono : StrictMono e), (PairSeq.IsBad r fun (m n : ℕ) (hmn : m < n) => (f (e m) (e n) ⋯).fst) ∨ ∃ (i : ι) (hmem : ∀ (m n : ℕ) (hmn : m < n), (f (e m) (e n) ⋯).fst = i), PairSeq.IsBad (t i) fun (m n : ℕ) (hmn : m < n) => ⋯ ▸ (f (e m) (e n) ⋯).snd

Sum theorem for 2-BQO along a quasi-order, restricted to a bad pair-sequence. If f is bad for LexSumRelQO r s t, then some restriction of f either has a bad index projection (for r), or has a constant index i along which the second components form a bad pair-sequence for t i. The constructive content underlying TwoBQO.lexSigmaQO.

theorem TwoBQO.lexSigmaQO {ι : Type u_3} (r : ι → ι → Prop) (hr : TwoBQO r) (s : ι → Type u_4) (t : (i : ι) → s i → s i → Prop) (ht : ∀ (i : ι), TwoBQO (t i)) : TwoBQO (LexSumRelQO r s t)

Sum theorem for 2-BQO along a quasi-order. If r on ι is 2-BQO and each t i on s i is 2-BQO, then Σ i, s i with LexSumRelQO r s t is 2-BQO.

Domination order on subsets

def DomOrder {α : Type u_3} (r : α → α → Prop) (X Y : Set α) : Prop

X dominates into Y: every element of X is r-below some element of Y.

Equations

• DomOrder r X Y = ∀ x ∈ X, ∃ y ∈ Y, r x y

theorem TwoBQO.dom_twoBQO {α : Type u_3} {r : α → α → Prop} (hr : TwoBQO r) : WellQuasiOrdered (DomOrder r)

The domination order on subsets of a 2-BQO is WQO.

Infinite sequences

Infinite sequences ℕ → Q in a 2-BQO Q are WQO under EmbedForAll.

def EmbedForAll {α : Type u_3} (r : α → α → Prop) (s s' : ℕ → α) : Prop

s embeds pointwise into s': there is a strictly monotone reindexing e with r (s n) (s' (e n)) for every n.

Equations

• EmbedForAll r s s' = ∃ (e : ℕ → ℕ), StrictMono e ∧ ∀ (n : ℕ), r (s n) (s' (e n))

instance EmbedForAll.isPreorder {Q : Type u_3} (r : Q → Q → Prop) [IsPreorder Q r] : IsPreorder (ℕ → Q) (EmbedForAll r)

EmbedForAll r is a preorder on ℕ → Q whenever r is (reflexivity via the identity reindexing, transitivity via composition of strictly monotone reindexings).

theorem Preorder.IsRegularSeq.exists_strictMono_dominating {Q : Type u_3} {le : Q → Q → Prop} {f : ℕ → Q} (hf : IsRegularSeq le f) (n : ℕ) : ∃ (e : ℕ → ℕ), StrictMono e ∧ ∀ (i : ℕ), n ≤ e i ∧ le (f i) (f (e i))

Strengthening of regularity. If f is a regular sequence for a relation, then for every threshold n there is a strictly monotone reindexing e : ℕ → ℕ whose values all lie at or above n and which dominates f pointwise: n ≤ e i and f i ≤ f (e i) for every i. Proved greedily via exists_strictMono_of_greedy, picking at each step a later index that is both > the previous one and ≥ n, available by regularity.

theorem TwoBQO.embedForAll_wqo {α : Type u_3} {r : α → α → Prop} [IsPreorder α r] (hr : TwoBQO r) : WellQuasiOrdered (EmbedForAll r)

EmbedForAll r is WQO on ℕ → Q whenever r is 2-BQO on Q.

Proof sketch. Split each sequence F n into a regular tail G n preceded by a finite head w n (WellQuasiOrdered.eventuallyRegular). Apply the product of Higman's lemma on the heads (WellQuasiOrdered.sublistForall₂) and of the domination order on the downsets S n = {x | ∃ i, r x (G n i)} of the tails (TwoBQO.dom_twoBQO) to a pair a < b with both components related. The domination relation on downsets, combined with regularity, produces a pointwise embedding of the tail G a into G b; the Higman relation on the heads produces a pointwise embedding of the head w a into w b; embed_combine splices the two into a single embedding of F a into F b.