Arrow assignments and their excess

A directed network on a vertex type V is described by an explicit arrow family Q : V → V → Type*, where Q v w is the type of arrows from v to w; parallel arrows, antiparallel arrows and loops are all allowed. An arrow assignment with values in a type K attaches a value of K to every arrow, with no sign or capacity constraint. Flows, pseudoflows, bounded assignments and residual updates are all arrow assignments subject to further conditions, and they share the additive calculus developed here. Arrow sums only need K to be an additive commutative monoid, while excess needs an additive commutative group.

The excess of an assignment f at a vertex v is the total value on arrows entering v minus the total value on arrows leaving v. With this sign convention a demand vertex has positive excess and a supply vertex negative excess, and the value of an ordinary s–t flow is its excess at the sink t. A loop at v enters and leaves v, so it contributes nothing to the excess.

Main definitions

• TauCeti.Assignment Q K: arrow assignments of the arrow family Q with values in K.
• TauCeti.arrowSum Q f S T: the total value of f on the arrows from S to T.
• TauCeti.excessAt Q f v: the excess of f at v.
• TauCeti.excessHom Q: excess as an additive homomorphism Assignment Q K →+ (V → K).
• TauCeti.Assignment.single e q: the assignment with value q on the arrow e and zero elsewhere.
• TauCeti.IsCirculation f: f has zero excess at every vertex.

Main results

• TauCeti.sum_excessAt_eq_arrowSum_sub: the total excess on a vertex set S is the value entering S minus the value leaving S.
• TauCeti.sum_excessAt: the total excess over all vertices vanishes.
• TauCeti.sum_excessAt_eq_zero_of_forall_mem_iff: the total excess vanishes on a vertex set that no arrow enters or leaves.
• TauCeti.excessAt_single: a single arrow from x to y carrying q has excess q at y and -q at x.
• TauCeti.excessAt_source_eq_neg_sink: an assignment conserved away from s and t has opposite excesses at s and t, and TauCeti.excessAt_sink_eq_arrowSum_sub computes the excess at t as the net value across any vertex set containing s but not t.
• TauCeti.isCirculation_iff_mem_ker: circulations form the kernel of excessHom, and TauCeti.setOf_excessAt_eq_eq_vadd_ker identifies every nonempty prescribed-excess fibre with a translate of that kernel.
• TauCeti.map_excessAt and TauCeti.excessAt_comp_equiv: excess commutes with additive maps of coefficients and with transport along an identification of arrow families.
• TauCeti.IsCirculation.map and TauCeti.Assignment.map_mem_Icc: additive changes of coefficients preserve circulations, and monotone ones preserve feasibility.

Implementation notes

The arrow family is an explicit argument rather than a Quiver instance, so that several arrow families can coexist on one vertex type, and so that instance search finds Fintype (Q v w) directly. An assignment binds its endpoints strict-implicitly, as ∀ ⦃v w⦄, Q v w → K: it is applied to an arrow as f e, while f on its own is not specialised to unknown endpoints.

Single-arrow assignments

noncomputable def TauCeti.Assignment.single {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] {x y : V} (e : Q x y) (q : K) : Assignment Q K

The assignment with value q on the arrow e and zero on every other arrow.

theorem TauCeti.Assignment.single_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] {x y a b : V} (e : Q x y) (q : K) (e' : Q a b) : single e q e' = if ⟨a, ⟨b, e'⟩⟩ = ⟨x, ⟨y, e⟩⟩ then q else 0

@[simp]

theorem TauCeti.Assignment.single_apply_self {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] {x y : V} (e : Q x y) (q : K) : single e q e = q

theorem TauCeti.Assignment.single_apply_of_ne {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] {x y a b : V} (e : Q x y) (q : K) {e' : Q a b} (h : ⟨a, ⟨b, e'⟩⟩ ≠ ⟨x, ⟨y, e⟩⟩) : single e q e' = 0

def TauCeti.arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] (f : Assignment Q K) (S T : Finset V) : K

The total value of the assignment f on the arrows from a vertex of S to a vertex of T. Every arrow is counted once, so parallel arrows add; when S and T meet, loops at their common vertices are counted.

theorem TauCeti.arrowSum_def {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] (f : Assignment Q K) (S T : Finset V) : arrowSum f S T = ∑ v ∈ S, ∑ w ∈ T, ∑ e : Q v w, f e

theorem TauCeti.arrowSum_eq_sum_ite {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] (f : Assignment Q K) (S T : Finset V) : arrowSum f S T = ∑ v : V, ∑ w : V, ∑ e : Q v w, if v ∈ S ∧ w ∈ T then f e else 0

An arrow sum as a sum over every arrow, with an indicator for its endpoints belonging to the specified sets.

theorem TauCeti.arrowSum_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] {M : Type u_1} [SetLike M K] [AddSubmonoidClass M K] {H : M} {f : Assignment Q K} (hf : ∀ ⦃v w : V⦄ (e : Q v w), f e ∈ H) (S T : Finset V) : arrowSum f S T ∈ H

The arrow sums of an assignment with values in an additive submonoid lie in the submonoid.

@[simp]

theorem TauCeti.arrowSum_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] (S T : Finset V) : arrowSum 0 S T = 0

@[simp]

theorem TauCeti.arrowSum_add {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] (f g : Assignment Q K) (S T : Finset V) : arrowSum (f + g) S T = arrowSum f S T + arrowSum g S T

theorem TauCeti.arrowSum_sum {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] {ι : Type u_1} (s : Finset ι) (f : ι → Assignment Q K) (S T : Finset V) : arrowSum (∑ i ∈ s, f i) S T = ∑ i ∈ s, arrowSum (f i) S T

@[simp]

theorem TauCeti.arrowSum_empty_left {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] (f : Assignment Q K) (T : Finset V) : arrowSum f ∅ T = 0

@[simp]

theorem TauCeti.arrowSum_empty_right {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] (f : Assignment Q K) (S : Finset V) : arrowSum f S ∅ = 0

theorem TauCeti.arrowSum_compl_eq_zero_of_forall_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] (f : Assignment Q K) {S : Finset V} (hS : ∀ ⦃x y : V⦄ (a : Q x y), x ∈ S → y ∈ S) : arrowSum f S Sᶜ = 0

If every arrow leaving S ends in S, then the arrow sum from S to its complement vanishes.

theorem TauCeti.arrowSum_union_left {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [DecidableEq V] (f : Assignment Q K) {S S' : Finset V} (h : Disjoint S S') (T : Finset V) : arrowSum f (S ∪ S') T = arrowSum f S T + arrowSum f S' T

theorem TauCeti.arrowSum_union_right {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [DecidableEq V] (f : Assignment Q K) (S : Finset V) {T T' : Finset V} (h : Disjoint T T') : arrowSum f S (T ∪ T') = arrowSum f S T + arrowSum f S T'

theorem TauCeti.map_arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] {L : Type u_1} {F : Type u_2} [AddCommMonoid L] [FunLike F K L] [AddMonoidHomClass F K L] (φ : F) (f : Assignment Q K) (S T : Finset V) : φ (arrowSum f S T) = arrowSum (f.map ⇑φ) S T

Mapping the values of an assignment along an additive monoid homomorphism commutes with summing them over the arrows between two vertex sets.

theorem TauCeti.arrowSum_mono {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [Preorder K] [AddLeftMono K] {f g : Assignment Q K} (h : f ≤ g) (S T : Finset V) : arrowSum f S T ≤ arrowSum g S T

Summing over the arrows between two vertex sets is monotone in the assignment.

theorem TauCeti.arrowSum_eq_zero_iff_of_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) {S T : Finset V} : arrowSum f S T = 0 ↔ ∀ v ∈ S, ∀ w ∈ T, ∀ (e : Q v w), f e = 0

A nonnegative assignment has zero total value on the arrows from S to T exactly when it vanishes on each of these arrows.

theorem TauCeti.arrowSum_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) (S T : Finset V) : 0 ≤ arrowSum f S T

A nonnegative assignment has nonnegative total value on the arrows from S to T.

theorem TauCeti.arrowSum_mono_left {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) {S S' : Finset V} (h : S ⊆ S') (T : Finset V) : arrowSum f S T ≤ arrowSum f S' T

For a nonnegative assignment, the arrow sum is monotone in the set of source vertices.

theorem TauCeti.arrowSum_mono_right {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) (S : Finset V) {T T' : Finset V} (h : T ⊆ T') : arrowSum f S T ≤ arrowSum f S T'

For a nonnegative assignment, the arrow sum is monotone in the set of target vertices.

theorem TauCeti.arrowSum_union_left_le {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} [DecidableEq V] (hf : 0 ≤ f) (S S' T : Finset V) : arrowSum f (S ∪ S') T ≤ arrowSum f S T + arrowSum f S' T

For a nonnegative assignment, the arrow sum is subadditive in the set of source vertices.

theorem TauCeti.arrowSum_union_right_le {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} [DecidableEq V] (hf : 0 ≤ f) (S T T' : Finset V) : arrowSum f S (T ∪ T') ≤ arrowSum f S T + arrowSum f S T'

For a nonnegative assignment, the arrow sum is subadditive in the set of target vertices.

theorem TauCeti.arrowSum_union_compl_le {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} [Fintype V] [DecidableEq V] (hf : 0 ≤ f) (S X : Finset V) : arrowSum f (S ∪ X) (S ∪ X)ᶜ ≤ arrowSum f S Sᶜ + arrowSum f X Finset.univ

Adding the vertices of X to a vertex set S increases the nonnegative value leaving it by at most the total value leaving X.

theorem TauCeti.arrowSum_sdiff_compl_le {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} [Fintype V] [DecidableEq V] (hf : 0 ≤ f) (S Y : Finset V) : arrowSum f (S \ Y) (S \ Y)ᶜ ≤ arrowSum f S Sᶜ + arrowSum f Finset.univ Y

Removing the vertices of Y from a vertex set S increases the nonnegative value leaving it by at most the total value entering Y.

theorem TauCeti.apply_le_arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) {S T : Finset V} {v w : V} (hv : v ∈ S) (hw : w ∈ T) (e : Q v w) : f e ≤ arrowSum f S T

The value of a nonnegative assignment on a single arrow from S to T is at most its total value on the arrows from S to T.

theorem TauCeti.sum_sum_single_in {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] {x y : V} (e : Q x y) (q : K) (v : V) : ∑ w : V, ∑ e' : Q w v, Assignment.single e q e' = if v = y then q else 0

The total value entering v for a single arrow from x to y is q when v = y and zero otherwise.

theorem TauCeti.sum_sum_single_out {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] {x y : V} (e : Q x y) (q : K) (v : V) : ∑ w : V, ∑ e' : Q v w, Assignment.single e q e' = if v = x then q else 0

The total value leaving v for a single arrow from x to y is q when v = x and zero otherwise.

theorem TauCeti.arrowSum_one {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoidWithOne K] [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] (S T : Finset V) : arrowSum 1 S T = ↑{a : (x : V) × (y : V) × Q x y | a.fst ∈ S ∧ a.snd.fst ∈ T}.card

The unit assignment counts arrows: its total value on the arrows from S to T is the number of these arrows, with parallel arrows counted separately.

@[simp]

theorem TauCeti.arrowSum_neg {V : Type u} {Q : V → V → Type v} {K : Type w} [SubtractionCommMonoid K] [(v w : V) → Fintype (Q v w)] (f : Assignment Q K) (S T : Finset V) : arrowSum (-f) S T = -arrowSum f S T

@[simp]

theorem TauCeti.arrowSum_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [SubtractionCommMonoid K] [(v w : V) → Fintype (Q v w)] (f g : Assignment Q K) (S T : Finset V) : arrowSum (f - g) S T = arrowSum f S T - arrowSum g S T

def TauCeti.excessAt {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) (v : V) : K

The excess of the assignment f at the vertex v: the total value on arrows entering v minus the total value on arrows leaving v. Loops at v cancel.

theorem TauCeti.excessAt_def {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) (v : V) : excessAt f v = ∑ w : V, ∑ e : Q w v, f e - ∑ w : V, ∑ e : Q v w, f e

theorem TauCeti.excessAt_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {M : Type u_1} [SetLike M K] [AddSubgroupClass M K] {H : M} {f : Assignment Q K} (hf : ∀ ⦃v w : V⦄ (e : Q v w), f e ∈ H) (v : V) : excessAt f v ∈ H

The excess of an assignment with values in an additive subgroup lies in the subgroup.

theorem TauCeti.excessAt_eq_arrowSum_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) (v : V) : excessAt f v = arrowSum f Finset.univ {v} - arrowSum f {v} Finset.univ

The excess at v is the value entering {v} minus the value leaving {v}.

@[simp]

theorem TauCeti.excessAt_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (v : V) : excessAt 0 v = 0

@[simp]

theorem TauCeti.excessAt_add {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f g : Assignment Q K) (v : V) : excessAt (f + g) v = excessAt f v + excessAt g v

def TauCeti.excessHom {V : Type u} (Q : V → V → Type v) (K : Type w) [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] : Assignment Q K →+ V → K

Excess as an additive homomorphism from arrow assignments to vertex functions.

@[simp]

theorem TauCeti.excessHom_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) (v : V) : (excessHom Q K) f v = excessAt f v

@[simp]

theorem TauCeti.excessAt_neg {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) (v : V) : excessAt (-f) v = -excessAt f v

@[simp]

theorem TauCeti.excessAt_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f g : Assignment Q K) (v : V) : excessAt (f - g) v = excessAt f v - excessAt g v

theorem TauCeti.excessAt_nonpos_of_nonneg_of_forall_in_eq_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) {v : V} (h : ∀ (w : V) (e : Q w v), f e = 0) : excessAt f v ≤ 0

A nonnegative assignment that vanishes on every arrow entering v has nonpositive excess at v.

theorem TauCeti.excessAt_nonneg_of_nonneg_of_forall_out_eq_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [PartialOrder K] [IsOrderedAddMonoid K] {f : Assignment Q K} (hf : 0 ≤ f) {v : V} (h : ∀ (w : V) (e : Q v w), f e = 0) : 0 ≤ excessAt f v

A nonnegative assignment that vanishes on every arrow leaving v has nonnegative excess at v.

theorem TauCeti.excessAt_le_of_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [PartialOrder K] [IsOrderedAddMonoid K] {f cap : Assignment Q K} (hf : f ∈ Set.Icc 0 cap) (v : V) : excessAt f v ≤ ∑ w : V, ∑ e : Q w v, cap e

An assignment between zero and cap has excess at v at most the total capacity of the arrows entering v.

theorem TauCeti.neg_excessAt_le_of_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [PartialOrder K] [IsOrderedAddMonoid K] {f cap : Assignment Q K} (hf : f ∈ Set.Icc 0 cap) (v : V) : -excessAt f v ≤ ∑ w : V, ∑ e : Q v w, cap e

An assignment between zero and cap has minus its excess at v at most the total capacity of the arrows leaving v.

theorem TauCeti.sum_excessAt_eq_arrowSum_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] (f : Assignment Q K) (S : Finset V) : ∑ v ∈ S, excessAt f v = arrowSum f Sᶜ S - arrowSum f S Sᶜ

Excess on a vertex set. The total excess of f on S is the value on arrows entering S from its complement minus the value on arrows leaving S for its complement; arrows with both ends in S cancel.

@[simp]

theorem TauCeti.sum_excessAt {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) : ∑ v : V, excessAt f v = 0

The total excess of an assignment over all vertices is zero: every arrow enters exactly one vertex and leaves exactly one vertex.

theorem TauCeti.sum_excessAt_eq_zero_of_forall_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) {S : Finset V} (hS : ∀ ⦃x y : V⦄ (a : Q x y), x ∈ S ↔ y ∈ S) : ∑ v ∈ S, excessAt f v = 0

A vertex set that no arrow enters or leaves, such as a union of weakly connected components, has total excess zero.

theorem TauCeti.excessAt_source_eq_neg_sink {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) {s t : V} (hconserve : ∀ (v : V), v ≠ s → v ≠ t → excessAt f v = 0) : excessAt f s = -excessAt f t

If an assignment is conserved at every vertex other than s and t, then its excesses at s and t are opposite. In particular a flow loses at its source exactly what it delivers to its sink.

theorem TauCeti.excessAt_sink_eq_arrowSum_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] (f : Assignment Q K) {s t : V} (hconserve : ∀ (v : V), v ≠ s → v ≠ t → excessAt f v = 0) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : excessAt f t = arrowSum f S Sᶜ - arrowSum f Sᶜ S

Value across a cut. If an assignment is conserved at every vertex other than s and t, then for every vertex set S containing s but not t, the excess at t is the value on arrows leaving S minus the value on arrows entering S.

theorem TauCeti.map_excessAt {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {L : Type u_1} {F : Type u_2} [AddCommGroup L] [FunLike F K L] [AddMonoidHomClass F K L] (φ : F) (f : Assignment Q K) (v : V) : φ (excessAt f v) = excessAt (f.map ⇑φ) v

Mapping the values of an assignment along an additive group homomorphism commutes with taking excess.

theorem TauCeti.excessAt_comp_equiv {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {W : Type u'} [Fintype W] {R : W → W → Type v'} [(a b : W) → Fintype (R a b)] (σ : V ≃ W) (τ : (v w : V) → Q v w ≃ R (σ v) (σ w)) (g : Assignment R K) (v : V) : excessAt (fun ⦃a b : V⦄ (e : Q a b) => g ((τ a b) e)) v = excessAt g (σ v)

Excess is invariant under transport along an identification σ of the vertices and identifications τ of the corresponding arrow types: pulling an assignment back along τ and taking excess at v agrees with taking excess at σ v.

@[simp]

theorem TauCeti.excessAt_single {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] {x y : V} (e : Q x y) (q : K) (v : V) : excessAt (Assignment.single e q) v = (if v = y then q else 0) - if v = x then q else 0

Excess of a single arrow. The assignment with value q on an arrow from x to y and zero elsewhere has excess q at y and -q at x; for a loop the two cancel.

Circulations and prescribed excess

def TauCeti.IsCirculation {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) : Prop

A (signed) circulation is an arrow assignment conserved at every vertex: its excess vanishes everywhere. No sign or capacity constraint is imposed.

theorem TauCeti.isCirculation_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) : IsCirculation f ↔ ∀ (v : V), excessAt f v = 0

theorem TauCeti.isCirculation_iff_mem_ker {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] (f : Assignment Q K) : IsCirculation f ↔ f ∈ (excessHom Q K).ker

Circulations are exactly the kernel of the excess homomorphism.

@[simp]

theorem TauCeti.isCirculation_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] : IsCirculation 0

theorem TauCeti.IsCirculation.add {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {f g : Assignment Q K} (hf : IsCirculation f) (hg : IsCirculation g) : IsCirculation (f + g)

theorem TauCeti.IsCirculation.neg {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {f : Assignment Q K} (hf : IsCirculation f) : IsCirculation (-f)

theorem TauCeti.IsCirculation.sub {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {f g : Assignment Q K} (hf : IsCirculation f) (hg : IsCirculation g) : IsCirculation (f - g)

theorem TauCeti.IsCirculation.arrowSum_compl_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] [DecidableEq V] {f : Assignment Q K} (hf : IsCirculation f) (S : Finset V) : arrowSum f Sᶜ S = arrowSum f S Sᶜ

A circulation carries the same total value into any vertex set S as out of it.

theorem TauCeti.excessAt_eq_iff_isCirculation_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {f₀ : Assignment Q K} {b : V → K} (hf₀ : ∀ (v : V), excessAt f₀ v = b v) (f : Assignment Q K) : (∀ (v : V), excessAt f v = b v) ↔ IsCirculation (f - f₀)

Given one assignment f₀ with excess b, an assignment has excess b exactly when it differs from f₀ by a circulation.

theorem TauCeti.setOf_excessAt_eq_eq_vadd_ker {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [(v w : V) → Fintype (Q v w)] [Fintype V] {f₀ : Assignment Q K} {b : V → K} (hf₀ : ∀ (v : V), excessAt f₀ v = b v) : {f : Assignment Q K | ∀ (v : V), excessAt f v = b v} = f₀ +ᵥ ↑(excessHom Q K).ker

Every nonempty prescribed-excess fibre is a translate of the circulations: if f₀ has excess b, the assignments with excess b are exactly f₀ + c for c in the kernel of excessHom.

Change of coefficients

theorem TauCeti.Assignment.sub_apply_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [AddGroup K] {M : Type u_1} [SetLike M K] [AddSubgroupClass M K] {H : M} {f h : Assignment Q K} {x y : V} (e : Q x y) (hh : h e ∈ H) : (f - h) e ∈ H ↔ f e ∈ H

Subtracting a subgroup-valued reference preserves membership on each arrow.

@[simp]

theorem TauCeti.Assignment.map_zero {V : Type u} {Q : V → V → Type v} {K : Type w} {L : Type u_1} {F : Type u_2} [FunLike F K L] [Zero K] [Zero L] [ZeroHomClass F K L] (φ : F) : map 0 ⇑φ = 0

@[simp]

theorem TauCeti.Assignment.map_add {V : Type u} {Q : V → V → Type v} {K : Type w} {L : Type u_1} {F : Type u_2} [FunLike F K L] [Add K] [Add L] [AddHomClass F K L] (φ : F) (f g : Assignment Q K) : (f + g).map ⇑φ = f.map ⇑φ + g.map ⇑φ

@[simp]

theorem TauCeti.Assignment.map_neg {V : Type u} {Q : V → V → Type v} {K : Type w} {L : Type u_1} {F : Type u_2} [FunLike F K L] [AddGroup K] [AddGroup L] [AddMonoidHomClass F K L] (φ : F) (f : Assignment Q K) : (-f).map ⇑φ = -f.map ⇑φ

@[simp]

theorem TauCeti.Assignment.map_sub {V : Type u} {Q : V → V → Type v} {K : Type w} {L : Type u_1} {F : Type u_2} [FunLike F K L] [AddGroup K] [AddGroup L] [AddMonoidHomClass F K L] (φ : F) (f g : Assignment Q K) : (f - g).map ⇑φ = f.map ⇑φ - g.map ⇑φ

theorem TauCeti.Assignment.map_mono {V : Type u} {Q : V → V → Type v} {K : Type w} {L : Type u_1} [Preorder K] [Preorder L] {φ : K → L} (hφ : Monotone φ) {f g : Assignment Q K} (h : f ≤ g) : f.map φ ≤ g.map φ

theorem TauCeti.Assignment.map_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} {L : Type u_1} [Preorder K] [Preorder L] {φ : K → L} (hφ : Monotone φ) {lo hi f : Assignment Q K} (hf : f ∈ Set.Icc lo hi) : f.map φ ∈ Set.Icc (lo.map φ) (hi.map φ)

A monotone coefficient map preserves feasibility, with the bounds mapped as well.

theorem TauCeti.IsCirculation.map {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] {L : Type u_1} {F : Type u_2} [AddCommGroup L] [FunLike F K L] [AddMonoidHomClass F K L] {f : Assignment Q K} (hf : IsCirculation f) (φ : F) : IsCirculation (f.map ⇑φ)

A circulation stays a circulation after an additive change of coefficients.

@[reducible, inline]

abbrev TauCeti.Network.excessAt {V : Type u} {C : Type u_1} [LE C] (N : Network C V) [Fintype V] [(x y : V) → Fintype (N.Hom x y)] {K : Type w} [AddCommGroup K] (f : N.Assignment K) (x : V) : K

Excess of an assignment on a network's arrow family. The network's bounds play no role.

@[reducible, inline]

abbrev TauCeti.Network.excessHom {V : Type u} {C : Type u_1} [LE C] (N : Network C V) [Fintype V] [(x y : V) → Fintype (N.Hom x y)] {K : Type w} [AddCommGroup K] : N.Assignment K →+ V → K

The additive excess map on a network's arrow family.