Directed networks with finite bounds

This file defines the carrier shared by finite flow and circulation theory. A network records an explicit family of arrow types and a lower and upper bound on every arrow. Keeping the arrow family explicit allows several networks on the same vertex type without competing Quiver instances.

@[reducible, inline]

abbrev TauCeti.Assignment {V : Sort u_1} (Hom : V → V → Type v) (K : Type w) : Sort (max (max (v + 1) (w + 1)) u_1)

An assignment gives a value to every arrow in an explicitly supplied arrow family. The endpoints are strict-implicit so that applying an assignment to an arrow infers them from the arrow.

theorem TauCeti.Assignment.apply_homOfEq {V : Type u_4} {Hom : V → V → Type v} {K : Type u_1} (f : Assignment Hom K) {x y x' y' : V} (a : Hom x y) (hx : x = x') (hy : y = y') : f (Quiver.homOfEq a hx hy) = f a

Assignment evaluation is invariant under transport of the arrow endpoints.

def TauCeti.Assignment.map {V : Sort u_4} {Hom : V → V → Type v} {K : Type u_1} {L : Type u_2} (f : Assignment Hom K) (φ : K → L) : Assignment Hom L

Change the coefficients of an assignment by applying φ to its value on every arrow.

This definition is exposed so that flows whose bounds are mapped in different but definitionally equal ways, such as along ψ ∘ φ or along φ and then ψ, can be compared.

@[simp]

theorem TauCeti.Assignment.map_apply {V : Sort u_4} {Hom : V → V → Type v} {K : Type u_1} {L : Type u_2} (f : Assignment Hom K) (φ : K → L) {x y : V} (e : Hom x y) : f.map φ e = φ (f e)

@[simp]

theorem TauCeti.Assignment.map_id {V : Sort u_4} {Hom : V → V → Type v} {K : Type u_1} (f : Assignment Hom K) : f.map id = f

@[simp]

theorem TauCeti.Assignment.map_map {V : Sort u_4} {Hom : V → V → Type v} {K : Type u_1} {L : Type u_2} {M : Type u_3} (f : Assignment Hom K) (φ : K → L) (ψ : L → M) : (f.map φ).map ψ = f.map (ψ ∘ φ)

structure TauCeti.Network (K : Type w) (V : Type u) [LE K] : Type (max (max u (v + 1)) w)

A directed network with finite lower and upper bounds on every arrow.

The arrow types may contain parallel arrows, arrows in both directions, and loops. Finiteness is imposed by individual theorems rather than by the network carrier.

• Hom : V → V → Type v

  The type of arrows from one vertex to another.

• lower : TauCeti.Assignment self.Hom K

  The lower bound on each arrow.

• upper : TauCeti.Assignment self.Hom K

  The upper bound on each arrow.

• lower_le_upper {x y : V} (e : self.Hom x y) : self.lower e ≤ self.upper e

  Every lower bound is at most the corresponding upper bound.

@[reducible, inline]

abbrev TauCeti.Network.Assignment {K : Type w} {V : Type u} [LE K] (N : Network K V) (R : Type u_1) : Type (max (max u_2 u_1) u)

Assignments on the arrow family of a network.

@[reducible]

def TauCeti.Network.ofCapacity {K : Type w} {V : Type u} [Zero K] [LE K] (Hom : V → V → Type v) (capacity : TauCeti.Assignment Hom K) (hcapacity : ∀ {x y : V} (e : Hom x y), 0 ≤ capacity e) : Network K V

Construct an ordinary network with zero lower bounds from nonnegative capacities.

This is exposed so that its dependent arrow family reduces in the exported projection lemmas.

@[simp]

theorem TauCeti.Network.ofCapacity_Hom {K : Type w} {V : Type u} [Zero K] [LE K] (Hom : V → V → Type v) (capacity : TauCeti.Assignment Hom K) (hcapacity : ∀ {x y : V} (e : Hom x y), 0 ≤ capacity e) : (ofCapacity Hom capacity ⋯).Hom = Hom

The arrow family of an ordinary network is its supplied arrow family.

@[simp]

theorem TauCeti.Network.ofCapacity_lower {K : Type w} {V : Type u} [Zero K] [LE K] (Hom : V → V → Type v) (capacity : TauCeti.Assignment Hom K) (hcapacity : ∀ {x y : V} (e : Hom x y), 0 ≤ capacity e) {x y : V} (e : (ofCapacity Hom capacity ⋯).Hom x y) : (ofCapacity Hom capacity ⋯).lower e = 0

@[simp]

theorem TauCeti.Network.ofCapacity_upper {K : Type w} {V : Type u} [Zero K] [LE K] (Hom : V → V → Type v) (capacity : TauCeti.Assignment Hom K) (hcapacity : ∀ {x y : V} (e : Hom x y), 0 ≤ capacity e) {x y : V} (e : (ofCapacity Hom capacity ⋯).Hom x y) : (ofCapacity Hom capacity ⋯).upper e = capacity e