Cofinality, cofinal reductions, and related notions

We explore various properties related to cofinality, defining the notion of a cofinal set and cofinal reduction, as well as the cofinality property (reduction graph and component versions).

We then prove two standard theorems about these: CP => CR and CR + countable => CP.

In later developments, we will need acyclic cofinal reduction sequences. We therefore show that any cofinal reduction sequence can be made acyclic.

def Thesis.cofinal {α : Type u_1} (r : α → α → Prop) (s : Set α) : Prop

A set s is cofinal in r if every element a: α reduces to some b in the set.

Equations

• Thesis.cofinal r s = ∀ (a : α), ∃ b ∈ s, r∗ a b

def Thesis.cofinal_reduction {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) : Prop

A reduction sequence is cofinal in r if the set of all elements in the sequence is cofinal in r.

Equations

• Thesis.cofinal_reduction hseq = Thesis.cofinal r hseq.elems

def Thesis.cofinality_property {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Prop

An ARS has the cofinality property (CP) if for every a ∈ A, there exists a reduction a = b₀ → b₁ → ⋯ that is cofinal in A|{b| a →∗ b}.

Equations

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

def Thesis.cofinality_property_conv {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Prop

An ARS has the component-wise cofinality property (CP≡) if for every a ∈ A, there exists a reduction a = b₀ → b₁ → ⋯ that is cofinal in A|{b | a ≡ b}.

Equations

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

theorem Thesis.cr_of_cp {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} : Thesis.cofinality_property A → Thesis.confluent A.union_rel

Any ARS with the cofinality property is confluent.

theorem Thesis.cp_iff_cp_conv {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Thesis.cofinality_property A ↔ Thesis.cofinality_property_conv A

The reduction-graph version of the cofinality property and the component version are equivalent.

theorem Thesis.cofinality_property.to_conv {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Thesis.cofinality_property A → Thesis.cofinality_property_conv A

theorem Thesis.cp_of_countable_cr {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) [cnt : Countable α] (cr : Thesis.confluent A.union_rel) : Thesis.cofinality_property A

A countable, confluent ARS has the cofinality property.

def Thesis.reduction_seq.acyclic {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) : Prop

A reduction sequence is acyclic if two elements are equal only if their indices are the same.

Equations

• hseq.acyclic = ∀ ⦃n m : ℕ⦄, ↑n < N → ↑m < N → f n = f m → n = m

theorem Thesis.acyclic_of_succeeds {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) (hcf : Thesis.cofinal_reduction hseq) (a : α) (ha : ∀ (n : ℕ), ↑n < N + 1 → ∃ m ≥ n, ↑m < N + 1 ∧ f m = a) : ∃ (N' : ℕ∞) (f' : ℕ → α) (hseq' : Thesis.reduction_seq r N' f'), Thesis.cofinal_reduction hseq' ∧ hseq'.acyclic

theorem Thesis.acyclic_of_finite {α : Type u_1} (r : α → α → Prop) {N : ℕ} {f : ℕ → α} (hseq : Thesis.reduction_seq r (↑N) f) (hcf : Thesis.cofinal_reduction hseq) : ∃ (N' : ℕ∞) (f' : ℕ → α) (hseq' : Thesis.reduction_seq r N' f'), Thesis.cofinal_reduction hseq' ∧ hseq'.acyclic

The acyclic version of a finite cofinal reduction sequence is simply the last element of that reduction sequence.

def Thesis.appears_infinitely {α : Type u_1} (f : ℕ → α) (n : ℕ) : Prop

If h: appears_infinitely f n, the element f n appears infinitely often.

Equations

• Thesis.appears_infinitely f n = ∀ (N : ℕ), ∃ m > N, f n = f m

def Thesis.appears_finitely {α : Type u_1} (f : ℕ → α) (n : ℕ) : Prop

If h: appears_finitely f n, the element f n appears finitely often.

Equations

• Thesis.appears_finitely f n = ∃ (N : ℕ), ∀ m > N, f n ≠ f m

def Thesis.appears_finitely' {α : Type u_1} (f : ℕ → α) (n : ℕ) : Prop

A stronger version of appears_finitely which gives us the final appearance.

Equations

• Thesis.appears_finitely' f n = ∃ (N : ℕ), f n = f N ∧ ∀ m > N, f n ≠ f m

theorem Thesis.last_finite_appearance {α : Type u_1} (f : ℕ → α) (n : ℕ) : Thesis.appears_finitely f n → Thesis.appears_finitely' f n

theorem Thesis.no_appears_infinitely_imp_appears_finitely {α : Type u_1} (f : ℕ → α) : (¬∃ (n : ℕ), Thesis.appears_infinitely f n) ↔ ∀ (n : ℕ), Thesis.appears_finitely f n

theorem Thesis.acyclic_of_appears_infinitely {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) (hseq : Thesis.reduction_seq r ⊤ f) (hcf : Thesis.cofinal_reduction hseq) (hinf : ∃ (n : ℕ), Thesis.appears_infinitely f n) : ∃ (N' : ℕ∞) (f' : ℕ → α) (hseq' : Thesis.reduction_seq r N' f'), Thesis.cofinal_reduction hseq' ∧ hseq'.acyclic

@[irreducible]

noncomputable def Thesis.f_idxs {α : Type u_1} (f : ℕ → α) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) (n : ℕ) : ℕ

Equations

• Thesis.f_idxs f hf n = Classical.choose ⋯

noncomputable def Thesis.f' {α : Type u_1} (f : ℕ → α) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) (n : ℕ) : α

Equations

• Thesis.f' f hf n = f (Thesis.f_idxs f hf n)

theorem Thesis.hseq' {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) (hseq : Thesis.reduction_seq r ⊤ f) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) : Thesis.reduction_seq r ⊤ (Thesis.f' f hf)

theorem Thesis.arg_le_hf {α : Type u_1} (f : ℕ → α) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) (n : ℕ) : n ≤ Classical.choose ⋯

theorem Thesis.f_idxs.strictMono {α : Type u_1} (f : ℕ → α) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) : StrictMono (Thesis.f_idxs f hf)

theorem Thesis.hseq'.cofinal {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) (hseq : Thesis.reduction_seq r ⊤ f) (hcf : Thesis.cofinal_reduction hseq) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) : Thesis.cofinal_reduction ⋯

theorem Thesis.f_idxs_last {α : Type u_1} (f : ℕ → α) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) {n m : ℕ} (hm : m > Thesis.f_idxs f hf n) : f (Thesis.f_idxs f hf n) ≠ f m

f_idxs f hf n represents the greatest index of an element of f. Hence, if m > f_idxs f hf n, f (f_idxs f hf n) ≠ f m.

theorem Thesis.hseq'.acyclic {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) (hseq : Thesis.reduction_seq r ⊤ f) (hf : ∀ (n : ℕ), Thesis.appears_finitely' f n) : ⋯.acyclic

theorem Thesis.acyclic_of_all_appear_finitely {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) (hseq : Thesis.reduction_seq r ⊤ f) (hcf : Thesis.cofinal_reduction hseq) (hninf : ¬∃ (n : ℕ), Thesis.appears_infinitely f n) : ∃ (f' : ℕ → α) (hseq' : Thesis.reduction_seq r ⊤ f'), Thesis.cofinal_reduction hseq' ∧ hseq'.acyclic

Let hseq be an infinite cofinal reduction sequence which contains every element only finitely often. Then there is an acyclic cofinal reduction sequence, which is constructed by skipping all cycles in hseq.

theorem Thesis.cofinal_reduction_acyclic {α : Type u_1} {r : Rel α α} {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f) (hcf : Thesis.cofinal_reduction hseq) : ∃ (N' : ℕ∞) (f' : ℕ → α) (hseq' : Thesis.reduction_seq r N' f'), Thesis.cofinal_reduction hseq' ∧ hseq'.acyclic

Any (cyclic) cofinal reduction sequence has an acyclic counterpart.