Documentation

TauCeti.Combinatorics.Network.MinimumCut.Poset

The poset of all minimum cuts #

Let f be a maximum bounded s–t assignment between distinct terminals. Keep only the residual arrows of positive capacity, and collapse each strongly connected component of the resulting quiver to a point: these residual components are partially ordered by reachability. The minimum cuts are exactly the terminal-separating vertex sets closed under positive residual reachability. So every minimum cut contains the components reachable from the component of the source, and avoids those from which the component of the sink is reachable; these two families of components are disjoint because f admits no augmenting walk. A minimum cut is then determined by the remaining free components it contains, and these form an arbitrary upper set of the free components.

This identifies the lattice of minimum cuts, ordered by inclusion, with the lattice of upper sets of the finite poset of free components, also ordered by inclusion. Since Mathlib orders UpperSet by reverse inclusion, the target of the order isomorphism is (UpperSet _)ᵒᵈ. Unions and intersections of minimum cuts correspond to unions and intersections of upper sets, the smallest and largest minimum cuts to the empty and the full upper set, and the minimum cut is unique exactly when there is no free component.

The bounds may be negative and the value of f may have either sign; the ordinary-flow statements follow by specialization.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev TauCeti.BoundedFlow.ResidualComponent {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) :
Type u

The residual components of a bounded s–t assignment f: the strongly connected components of the quiver of residual arrows of positive capacity for f. They are partially ordered by reachability along such arrows.

Instances For
    source
    def TauCeti.BoundedFlow.residualComponent {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) (v : V) :
    f.ResidualComponent

    The residual component of f containing a vertex.

    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.BoundedFlow.FreeComponent {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) :
      Type u

      The free residual components of f: those not reachable from the component of the source and from which the component of the sink is not reachable, with the induced partial order.

      Instances For
        source
        @[simp]
        theorem TauCeti.BoundedFlow.residualComponent_le_residualComponent {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} {v w : V} :
        f.residualComponent v ≤ f.residualComponent w ↔ PositiveReachable (residualCapacity lo hi f.toFun) v w

        The residual component of v is below that of w exactly when w is positively reachable from v for the residual capacities.

        source
        @[simp]
        theorem TauCeti.BoundedFlow.residualComponent_eq_residualComponent {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} {v w : V} :
        f.residualComponent v = f.residualComponent w ↔ PositiveReachable (residualCapacity lo hi f.toFun) v w ∧ PositiveReachable (residualCapacity lo hi f.toFun) w v

        Two vertices have the same residual component exactly when each is positively reachable from the other for the residual capacities.

        source
        theorem TauCeti.BoundedFlow.residualComponent_surjective {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} :
        Function.Surjective f.residualComponent

        Every residual component contains a vertex.

        source
        theorem TauCeti.BoundedFlow.IsMaximum.disjoint_Ici_Iic {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) :
        Disjoint (Set.Ici (f.residualComponent s)) (Set.Iic (f.residualComponent t))

        For a maximum bounded s–t assignment between distinct terminals, no residual component is both reachable from the component of the source and reaches the component of the sink.

        source
        theorem TauCeti.BoundedFlow.IsMaximum.mem_of_residualComponent_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) {S : Finset V} (hS : TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S) {v : V} (hv : f.residualComponent s ≤ f.residualComponent v) :
        v ∈ S

        Every minimum cut contains the vertices whose residual component is reachable from the component of the source.

        source
        theorem TauCeti.BoundedFlow.IsMaximum.notMem_of_residualComponent_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) {S : Finset V} (hS : TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S) {v : V} (hv : f.residualComponent v ≤ f.residualComponent t) :
        v ∉ S

        No minimum cut contains a vertex whose residual component reaches the component of the sink.

        source
        noncomputable def TauCeti.BoundedFlow.IsMaximum.minimizersOrderIso {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) :
        ↥(TerminalCut.minimizers ⋯ {s} {t}) ≃o (UpperSet f.FreeComponent)ᵒᵈ

        The poset of minimum cuts. For a maximum bounded s–t assignment f between distinct terminals, the minimum cuts, ordered by inclusion, are order isomorphic to the upper sets of the poset of free residual components, ordered by inclusion. A minimum cut corresponds to the free components contained in it, and an upper set to the vertices of its components together with the vertices forced onto the source side.

        Instances For
          source
          theorem TauCeti.BoundedFlow.IsMaximum.mem_minimizersOrderIso_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {S : ↥(TerminalCut.minimizers ⋯ {s} {t})} {C : f.FreeComponent} :
          C ∈ OrderDual.ofDual ((minimizersOrderIso hst hf) S) ↔ ∀ (v : V), f.residualComponent v = ↑C → v ∈ ↑S

          A free component belongs to the upper set of a minimum cut exactly when all of its vertices lie in the cut.

          source
          @[simp]
          theorem TauCeti.BoundedFlow.IsMaximum.residualComponent_mem_minimizersOrderIso_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {S : ↥(TerminalCut.minimizers ⋯ {s} {t})} {v : V} (h : ¬f.residualComponent s ≤ f.residualComponent v ∧ ¬f.residualComponent v ≤ f.residualComponent t) :
          ⟨f.residualComponent v, h⟩ ∈ OrderDual.ofDual ((minimizersOrderIso hst hf) S) ↔ v ∈ ↑S

          The free residual component of a vertex belongs to the upper set of a minimum cut exactly when the vertex lies in the cut.

          source
          @[simp]
          theorem TauCeti.BoundedFlow.IsMaximum.mem_minimizersOrderIso_symm_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {U : (UpperSet f.FreeComponent)ᵒᵈ} {v : V} :
          v ∈ ↑((minimizersOrderIso hst hf).symm U) ↔ f.residualComponent s ≤ f.residualComponent v ∨ ∃ (h : ¬f.residualComponent s ≤ f.residualComponent v ∧ ¬f.residualComponent v ≤ f.residualComponent t), ⟨f.residualComponent v, h⟩ ∈ OrderDual.ofDual U

          Vertex-membership formula. A vertex lies in the minimum cut of an upper set of free components exactly when its residual component is reachable from the component of the source or is a member of the upper set.

          source
          theorem TauCeti.BoundedFlow.IsMaximum.coe_minimizersOrderIso_sup {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) (S T : ↥(TerminalCut.minimizers ⋯ {s} {t})) :
          ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) (S ⊔ T))) = ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) S)) ∪ ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) T))

          The free components contained in the union of two minimum cuts are the union of those contained in each.

          source
          theorem TauCeti.BoundedFlow.IsMaximum.coe_minimizersOrderIso_inf {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) (S T : ↥(TerminalCut.minimizers ⋯ {s} {t})) :
          ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) (S ⊓ T))) = ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) S)) ∩ ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) T))

          The free components contained in the intersection of two minimum cuts are the intersection of those contained in each.

          source
          theorem TauCeti.BoundedFlow.IsMaximum.minimizersOrderIso_symm_top {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular (cutBound lo hi)) :
          ↑((minimizersOrderIso hst hf).symm (OrderDual.toDual ⊤)) = TerminalCut.smallest hsub ⋯

          The empty upper set of free components gives the smallest minimum cut.

          source
          theorem TauCeti.BoundedFlow.IsMaximum.minimizersOrderIso_symm_bot {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular (cutBound lo hi)) :
          ↑((minimizersOrderIso hst hf).symm (OrderDual.toDual ⊥)) = TerminalCut.largest hsub ⋯

          The full upper set of free components gives the largest minimum cut.

          source
          theorem TauCeti.BoundedFlow.IsMaximum.existsUnique_isMinimum_iff_isEmpty {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) :
          (∃! S : Finset V, TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S) ↔ IsEmpty f.FreeComponent

          The minimum cut is unique exactly when no residual component is free.

          Ordinary flows #

          source
          noncomputable def TauCeti.Flow.IsMaximum.minimizersOrderIso {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) :
          ↥(TerminalCut.minimizers ⋯ {s} {t}) ≃o (UpperSet f.FreeComponent)ᵒᵈ

          The poset of minimum cuts of an ordinary flow. For a maximum ordinary s–t flow f between distinct terminals, the minimum cuts for the capacity of the arrows leaving a set, ordered by inclusion, are order isomorphic to the upper sets of the poset of free residual components, ordered by inclusion.

          Instances For
            source
            @[simp]
            theorem TauCeti.Flow.IsMaximum.residualComponent_mem_minimizersOrderIso_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) {S : ↥(TerminalCut.minimizers ⋯ {s} {t})} {v : V} (h : ¬f.residualComponent s ≤ f.residualComponent v ∧ ¬f.residualComponent v ≤ f.residualComponent t) :
            ⟨f.residualComponent v, h⟩ ∈ OrderDual.ofDual ((minimizersOrderIso hst hf) S) ↔ v ∈ ↑S

            The free residual component of a vertex belongs to the upper set of a minimum cut of a maximum ordinary flow exactly when the vertex lies in the cut.

            source
            @[simp]
            theorem TauCeti.Flow.IsMaximum.mem_minimizersOrderIso_symm_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) {U : (UpperSet f.FreeComponent)ᵒᵈ} {v : V} :
            v ∈ ↑((minimizersOrderIso hst hf).symm U) ↔ f.residualComponent s ≤ f.residualComponent v ∨ ∃ (h : ¬f.residualComponent s ≤ f.residualComponent v ∧ ¬f.residualComponent v ≤ f.residualComponent t), ⟨f.residualComponent v, h⟩ ∈ OrderDual.ofDual U

            A vertex lies in the minimum cut of an upper set of free components exactly when its residual component is reachable from the component of the source or is a member of the upper set.

            source
            theorem TauCeti.Flow.IsMaximum.coe_minimizersOrderIso_sup {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) (S T : ↥(TerminalCut.minimizers ⋯ {s} {t})) :
            ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) (S ⊔ T))) = ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) S)) ∪ ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) T))

            The free components contained in the union of two minimum cuts of a maximum ordinary flow are the union of those contained in each.

            source
            theorem TauCeti.Flow.IsMaximum.coe_minimizersOrderIso_inf {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) (S T : ↥(TerminalCut.minimizers ⋯ {s} {t})) :
            ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) (S ⊓ T))) = ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) S)) ∩ ↑(OrderDual.ofDual ((minimizersOrderIso hst hf) T))

            The free components contained in the intersection of two minimum cuts of a maximum ordinary flow are the intersection of those contained in each.

            source
            theorem TauCeti.Flow.IsMaximum.minimizersOrderIso_symm_top {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular fun (S : Finset V) => arrowSum cap S Sᶜ) :
            ↑((minimizersOrderIso hst hf).symm (OrderDual.toDual ⊤)) = TerminalCut.smallest hsub ⋯

            The empty upper set of free components gives the smallest minimum cut of a maximum ordinary flow.

            source
            theorem TauCeti.Flow.IsMaximum.minimizersOrderIso_symm_bot {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular fun (S : Finset V) => arrowSum cap S Sᶜ) :
            ↑((minimizersOrderIso hst hf).symm (OrderDual.toDual ⊥)) = TerminalCut.largest hsub ⋯

            The full upper set of free components gives the largest minimum cut of a maximum ordinary flow.

            source
            theorem TauCeti.Flow.IsMaximum.existsUnique_isMinimum_iff_isEmpty {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) :
            (∃! S : Finset V, TerminalCut.IsMinimum (fun (S : Finset V) => arrowSum cap S Sᶜ) {s} {t} S) ↔ IsEmpty f.FreeComponent

            The minimum cut is unique exactly when no residual component of a maximum ordinary flow is free.

            Example #

            On the vertices s = 0, a = 1, b = 2 and t = 3, take unit capacities on the arrows s → a, a → t, s → b, b → t and a → b, and capacity zero on one arrow for every other ordered pair, loops included. The flow sending one unit along each of s → a → t and s → b → t and nothing along a → b has value 2, the capacity of {s}, so it is maximum. Its residual arrows of positive capacity are the reverse arrows a → s, b → s, t → a and t → b, and the forward arrow a → b. So the free residual components are those of a and b, with the component of a below that of b. The upper sets of free components are the empty set, the component of b, and both components, and the minimum cuts are {s}, {s, b} and {s, a, b}: choosing a forces choosing b.