Documentation

TauCeti.Combinatorics.Network.Acyclic

Acyclic assignments and acyclic flows #

An arrow assignment is acyclic when no directed cycle traverses only arrows of positive value. Cancelling such cycles one at a time, each by its least arrow value, turns every nonnegative assignment on a finite arrow family into an acyclic one that is arrowwise no larger and has the same excess at every vertex. For an ordinary s–t flow this gives an acyclic flow of the same value. A nonnegative acyclic assignment vanishes on every loop and on at least one arrow of every pair of opposite arrows. The path–cycle decomposition of an acyclic assignment has no cycles, so an acyclic ordinary flow carries at most its value on every arrow.

Acyclicity is stronger than having a decomposition without cycles: unit flows along s → a → b → t and s → b → a → t add up to a flow that these two paths decompose, but whose arrows of positive value contain the cycle a → b → a.

Main results #

References #

source
theorem TauCeti.Assignment.IsAcyclic.not_pos_and_pos {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {f : Assignment Q K} (hf : f.IsAcyclic) {x y : V} (e : Q x y) (e' : Q y x) :
¬(0 < f e ∧ 0 < f e')

An acyclic assignment is not positive on two opposite arrows.

source
@[simp]
theorem TauCeti.Assignment.isAcyclic_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [Preorder K] :
IsAcyclic 0
source
theorem TauCeti.Assignment.IsAcyclic.anti {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [Preorder K] {f g : Assignment Q K} (hfg : f ≤ g) (hg : g.IsAcyclic) :
f.IsAcyclic

An assignment below an acyclic one is acyclic.

source
theorem TauCeti.Assignment.IsAcyclic.apply_eq_zero_or_apply_eq_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [PartialOrder K] {f : Assignment Q K} (hf : f.IsAcyclic) (hf₀ : 0 ≤ f) {x y : V} (e : Q x y) (e' : Q y x) :
f e = 0 ∨ f e' = 0

A nonnegative acyclic assignment vanishes on one of any two opposite arrows.

source
theorem TauCeti.Assignment.IsAcyclic.apply_eq_zero_of_loop {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [PartialOrder K] {f : Assignment Q K} (hf : f.IsAcyclic) (hf₀ : 0 ≤ f) {x : V} (e : Q x x) :
f e = 0

A nonnegative acyclic assignment vanishes on every loop.

Cycle cancelling #

source
theorem TauCeti.exists_isAcyclic_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] (H : AddSubgroup K) {f : Assignment Q K} (hf : 0 ≤ f) (hH : ∀ ⦃x y : V⦄ (e : Q x y), f e ∈ H) :
∃ (g : Assignment Q K), g.IsAcyclic ∧ 0 ≤ g ∧ g ≤ f ∧ (∀ (v : V), excessAt g v = excessAt f v) ∧ ∀ ⦃x y : V⦄ (e : Q x y), g e ∈ H

Cycle cancelling. Below every nonnegative arrow assignment f on a finite arrow family lies an acyclic nonnegative assignment with the same excess as f at every vertex. If the values of f lie in an additive subgroup H, then so do those of the acyclic assignment.

source
theorem TauCeti.Flow.exists_isAcyclic_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} (f : Flow cap s t) (H : AddSubgroup K) (hH : ∀ ⦃x y : V⦄ (e : Q x y), f.toFun e ∈ H) :
∃ (g : Flow cap s t), g.toFun.IsAcyclic ∧ g.val = f.val ∧ g.toFun ≤ f.toFun ∧ ∀ ⦃x y : V⦄ (e : Q x y), g.toFun e ∈ H

Acyclic flows. Every ordinary s–t flow f has an acyclic ordinary s–t flow of the same value that is arrowwise at most f. If the values of f lie in an additive subgroup H, then so do those of the acyclic flow.

source
theorem TauCeti.Flow.exists_isAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} (f : Flow cap s t) :
∃ (g : Flow cap s t), g.toFun.IsAcyclic ∧ g.val = f.val ∧ g.toFun ≤ f.toFun

Acyclic flows. Every ordinary s–t flow f has an acyclic ordinary s–t flow of the same value that is arrowwise at most f.

source
theorem TauCeti.SetFlow.exists_isAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) :
∃ (g : SetFlow cap A B), g.toFun.IsAcyclic ∧ g.val = f.val ∧ g.toFun ≤ f.toFun

Acyclic set-to-set flows. Every A–B flow f has an acyclic A–B flow of the same value that is arrowwise at most f.

Decompositions of acyclic assignments #

source
theorem TauCeti.PathCycleDecomposition.cycles_eq_nil_of_isAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) (hf : f.IsAcyclic) :
D.cycles = []

A path–cycle decomposition of an acyclic assignment has no cycles.

source
theorem TauCeti.PathCycleDecomposition.pathAssignment_eq_of_isAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (D : PathCycleDecomposition f) (hf : f.IsAcyclic) :
D.pathAssignment = f

The paths of a path–cycle decomposition of an acyclic assignment add up to the assignment.

source
theorem TauCeti.Flow.toFun_le_val_of_isAcyclic {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} (f : Flow cap s t) (hf : f.toFun.IsAcyclic) {x y : V} (e : Q x y) :
f.toFun e ≤ f.val

An acyclic ordinary s–t flow carries at most its value on every arrow.