Splitting the vertices of a multigraph into directed paths

Fix a set K of kept edges. Every vertex w is replaced by a directed path of slots, one for each end at w of a kept edge: first the ends of the kept edges entering w, then the ends of those leaving w. Each kept edge joins the slot of its tail end to the slot of its head end, and consecutive slots of a path are joined by a path edge.

Every slot meets at most two path edges and one kept edge, and no edge is a loop. A vertex with s > 0 slots contributes s vertices and s - 1 path edges, so the number of edges minus the number of vertices is the number of kept edges minus the number of vertices with a slot. A directed walk entering a vertex along a kept edge arrives at an entering slot, and the path reaches every leaving slot from there, so directed walks lift; a lifted walk stays in the paths of the vertices of the original walk, so vertex-disjoint walks lift to vertex-disjoint walks.

Keeping the edges whose tail lies in the undirected component of a vertex r makes the split graph connected. Applied to a superconcentrator whose terminals lie in that component, the split graph is a superconcentrator, with each input placed at the first slot of its path and each output at the last.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.sigma_fin_eq_iff {V : Type} {f : V → ℕ} {a b : (w : V) × Fin (f w)} : a = b ↔ a.fst = b.fst ∧ ↑a.snd = ↑b.snd

Two elements of a sigma type of Fin fibres are equal when their components are.

Positions in a finite set

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.pos {E : Type} (s : Finset E) (e : E) (h : e ∈ s) : ℕ

The position of e in a fixed enumeration of s.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.pos s e h = ↑(s.equivFin ⟨e, h⟩)

theorem Algebraic.Cutwidth.Superconcentrator.Internal.pos_lt {E : Type} {s : Finset E} {e : E} (h : e ∈ s) : pos s e h < s.card

theorem Algebraic.Cutwidth.Superconcentrator.Internal.eq_of_pos_eq {E : Type} {s t : Finset E} (hst : s = t) {e₁ e₂ : E} {h₁ : e₁ ∈ s} {h₂ : e₂ ∈ t} (h : pos s e₁ h₁ = pos t e₂ h₂) : e₁ = e₂

The split graph

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.inEdges {V E : Type} (G : Multigraph V E) (K : Finset E) (w : V) : Finset E

The kept edges directed into w.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.inEdges G K w = {e ∈ K | G.snd e = w}

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.outEdges {V E : Type} (G : Multigraph V E) (K : Finset E) (w : V) : Finset E

The kept edges directed out of w.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.outEdges G K w = {e ∈ K | G.fst e = w}

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.slots {V E : Type} (G : Multigraph V E) (K : Finset E) (w : V) : ℕ

The number of slots of w: the number of ends at w of kept edges.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Superconcentrator.Internal.SplitVertex {V E : Type} (G : Multigraph V E) (K : Finset E) : Type

The vertices of the split graph: the slots of all vertices.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.SplitVertex G K = ((w : V) × Fin (Algebraic.Cutwidth.Superconcentrator.Internal.slots G K w))

@[reducible, inline]

abbrev Algebraic.Cutwidth.Superconcentrator.Internal.SplitEdge {V E : Type} (G : Multigraph V E) (K : Finset E) : Type

The edges of the split graph: the kept edges and the path edges joining consecutive slots.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.SplitEdge G K = (↥K ⊕ (w : V) × Fin (Algebraic.Cutwidth.Superconcentrator.Internal.slots G K w - 1))

theorem Algebraic.Cutwidth.Superconcentrator.Internal.mem_inEdges_snd {V E : Type} (G : Multigraph V E) (K : Finset E) (e : ↥K) : ↑e ∈ inEdges G K (G.snd ↑e)

theorem Algebraic.Cutwidth.Superconcentrator.Internal.mem_outEdges_fst {V E : Type} (G : Multigraph V E) (K : Finset E) (e : ↥K) : ↑e ∈ outEdges G K (G.fst ↑e)

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.tail {V E : Type} (G : Multigraph V E) (K : Finset E) (e : ↥K) : SplitVertex G K

The slot at which a kept edge leaves its tail.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.head {V E : Type} (G : Multigraph V E) (K : Finset E) (e : ↥K) : SplitVertex G K

The slot at which a kept edge enters its head.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Superconcentrator.Internal.split {V E : Type} (G : Multigraph V E) (K : Finset E) : Multigraph (SplitVertex G K) (SplitEdge G K)

The split graph: kept edges run from tail slots to head slots, and path edges from each slot to the next slot of the same vertex.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.tail_ne_head {V E : Type} {G : Multigraph V E} {K : Finset E} (a b : ↥K) : tail G K a ≠ head G K b

theorem Algebraic.Cutwidth.Superconcentrator.Internal.tail_injective {V E : Type} {G : Multigraph V E} {K : Finset E} : Function.Injective (tail G K)

theorem Algebraic.Cutwidth.Superconcentrator.Internal.head_injective {V E : Type} {G : Multigraph V E} {K : Finset E} : Function.Injective (head G K)

theorem Algebraic.Cutwidth.Superconcentrator.Internal.split_loopless {V E : Type} {G : Multigraph V E} {K : Finset E} : (split G K).Loopless

The split graph has no loops.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.split_maxDegreeLE {V E : Type} {G : Multigraph V E} {K : Finset E} [Fintype V] : (split G K).MaxDegreeLE 3

Every slot meets at most three edges: the kept edge of the slot and two path edges.

Counting

theorem Algebraic.Cutwidth.Superconcentrator.Internal.sum_card_inEdges {V E : Type} {G : Multigraph V E} {K : Finset E} [Fintype V] : ∑ w : V, (inEdges G K w).card = K.card

theorem Algebraic.Cutwidth.Superconcentrator.Internal.sum_card_outEdges {V E : Type} {G : Multigraph V E} {K : Finset E} [Fintype V] : ∑ w : V, (outEdges G K w).card = K.card

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_splitVertex {V E : Type} {G : Multigraph V E} {K : Finset E} [Fintype V] : Fintype.card (SplitVertex G K) = 2 * K.card

The split graph has two slots for every kept edge.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_splitEdge_add {V E : Type} {G : Multigraph V E} {K : Finset E} [Fintype V] : Fintype.card (SplitEdge G K) + {w : V | slots G K w ≠ 0}.card = K.card + Fintype.card (SplitVertex G K)

Edges minus vertices of the split graph: kept edges minus vertices with a slot.

Walks inside one vertex path

def Algebraic.Cutwidth.Superconcentrator.Internal.stepIn {V E : Type} {G : Multigraph V E} {K : Finset E} (P : Set V) (a b : SplitVertex G K) : Prop

Directed steps of the split graph between slots of vertices in P.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.stepIn P a b = ((Algebraic.Cutwidth.Superconcentrator.Internal.split G K).DirAdj a b ∧ a.fst ∈ P ∧ b.fst ∈ P)

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_forward_aux {V E : Type} {G : Multigraph V E} {K : Finset E} (P : Set V) (d : ℕ) (w : V) (i j : Fin (slots G K w)) : w ∈ P → ↑j = ↑i + d → Relation.ReflTransGen (stepIn P) ⟨w, i⟩ ⟨w, j⟩

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_forward {V E : Type} {G : Multigraph V E} {K : Finset E} (P : Set V) {x y : SplitVertex G K} (hxy : x.fst = y.fst) (hx : x.fst ∈ P) (hle : ↑x.snd ≤ ↑y.snd) : Relation.ReflTransGen (stepIn P) x y

Inside the path of a vertex of P, each slot reaches every later slot.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_adj_of_fst_eq {V E : Type} {G : Multigraph V E} {K : Finset E} {x y : SplitVertex G K} (hxy : x.fst = y.fst) : Relation.ReflTransGen (split G K).Adj x y

Any two slots of one vertex are joined in the split graph.