Acyclic relations: simple cycles and topological numberings

A relation r is acyclic (cslib's Relation.Acyclic r) when its transitive closure is irreflexive, that is, when r has no closed walk. This file gives two equivalent forms of acyclicity:

• Simple cycles. A closed walk is a nonempty list whose consecutive elements, read cyclically (Cycle.Chain), are related. Every closed walk contains a simple one, without repeated elements: cut the walk at a repeated element and keep the closed walk between its two occurrences. So r is acyclic exactly when it has no simple cycle (Relation.acyclic_iff_forall_nodup_not_cycle_chain), the form in which feedback vertex and arc sets are stated.
• Topological numberings. When the related elements lie in a finite set V, r is acyclic exactly when some numbering f : α → ℕ strictly increases along every step of r (Relation.acyclic_iff_exists_rank). The numbering may be taken below the number of elements of V, which makes it a certificate of polynomial size: number each element by how many elements of V reach it.

Main results

• Relation.exists_nodup_of_cycle_chain: a closed walk contains a simple cycle.
• Relation.exists_cycle_chain_of_transGen, Relation.transGen_of_cycle_chain: closed walks are the transitive closure relating an element to itself.
• Relation.acyclic_iff_forall_nodup_not_cycle_chain: acyclicity as the absence of simple cycles.
• Relation.Acyclic.exists_rank, Relation.acyclic_of_rank, Relation.acyclic_iff_exists_rank: acyclicity on a finite set as a topological numbering bounded by the number of elements.
• Relation.not_transGen_of_rank: a strictly increasing numbering excludes closed walks.

Closed walks and simple cycles

theorem Relation.exists_nodup_of_cycle_chain {α : Type u_1} {r : α → α → Prop} {l : List α} (hne : l ≠ []) (hch : Cycle.Chain r ↑l) : ∃ (c : List α), c ≠ [] ∧ c.Nodup ∧ c ⊆ l ∧ Cycle.Chain r ↑c

A closed walk contains a simple cycle: a nonempty closed chain contains a nonempty closed chain without repetitions, all of whose elements are elements of the walk.

theorem Relation.exists_cycle_chain_of_transGen {α : Type u_1} {r : α → α → Prop} {a : α} (h : TransGen r a a) : ∃ (c : List α), a ∈ c ∧ Cycle.Chain r ↑c

A closed walk through a gives a closed chain containing a.

theorem Relation.transGen_of_cycle_chain {α : Type u_1} {r : α → α → Prop} {c : List α} (hch : Cycle.Chain r ↑c) {a : α} (ha : a ∈ c) : TransGen r a a

Every element of a closed chain lies on a closed walk.

theorem Relation.acyclic_iff_forall_nodup_not_cycle_chain {α : Type u_1} {r : α → α → Prop} : Acyclic r ↔ ∀ (c : List α), c ≠ [] → c.Nodup → ¬Cycle.Chain r ↑c

Acyclicity as the absence of simple cycles: no element lies on a closed walk exactly when there is no nonempty closed chain without repetitions.

Topological numberings

theorem Relation.Acyclic.exists_rank {α : Type u_1} {r : α → α → Prop} (hr : Acyclic r) (V : Finset α) (hV : ∀ (a b : α), r a b → a ∈ V ∧ b ∈ V) : ∃ (f : α → ℕ), (∀ a ∈ V, f a < V.card) ∧ ∀ (a b : α), r a b → f a < f b

Topological numbering. If every step of r is between elements of a finite set V and r is acyclic, then numbering each element by the number of elements of V that reach it gives numbers below the number of elements of V that strictly increase along every step.

The hypothesis hV says that V contains the support of r: both ends of every step. Elements outside V are related to nothing, so their numbers are unconstrained.

theorem Relation.not_transGen_of_rank {α : Type u_1} {r : α → α → Prop} {f : α → ℕ} (hf : ∀ (a b : α), r a b → f a < f b) (a : α) : ¬TransGen r a a

A numbering that strictly increases along every step of r excludes closed walks.

theorem Relation.acyclic_of_rank {α : Type u_1} {r : α → α → Prop} {f : α → ℕ} (hf : ∀ (a b : α), r a b → f a < f b) : Acyclic r

A relation with a numbering that strictly increases along every step is acyclic.

theorem Relation.acyclic_iff_exists_rank {α : Type u_1} {r : α → α → Prop} (V : Finset α) (hV : ∀ (a b : α), r a b → a ∈ V ∧ b ∈ V) : Acyclic r ↔ ∃ (f : α → ℕ), (∀ a ∈ V, f a < V.card) ∧ ∀ (a b : α), r a b → f a < f b

Acyclicity on a finite set as a topological numbering: when every step of r is between elements of a finite set V (the hypothesis hV), r is acyclic exactly when some numbering below the number of elements of V strictly increases along every step.