Blocks of a contraction

A contraction keeps, for each supervertex a, the block s(a) of original vertices merged into it Karger and Stein, Section 2. When a contraction step merges v into u and moves the last supervertex into slot v (Cslib.WeightedCut.contractMatrix), the block of u absorbs the block of v and every other supervertex keeps its block (Cslib.WeightedCut.contractBlocks). For blocks given as the fibres of a supervertex map part, this is the same as taking the fibres of the contracted map Cslib.WeightedCut.contractPart (Cslib.WeightedCut.contractBlocks_pullbackCut), so a contraction that tracks blocks carries exactly the information of a supervertex map.

Main definitions

• Cslib.WeightedCut.contractBlocks: the blocks after one contraction step.

Main results

• Cslib.WeightedCut.contractBlocks_pullbackCut: contracting the fibres of part gives the fibres of contractPart part u v huv.

References

• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem

def Cslib.WeightedCut.contractBlocks {α : Type u_1} [DecidableEq α] {m : ℕ} (blocks : Fin (m + 1) → Finset α) (u v : Fin (m + 1)) (i : Fin m) : Finset α

The blocks after merging supervertex v into u and moving the last supervertex into slot v (contractMatrix): the block of u absorbs the block of v, and the others keep theirs.

theorem Cslib.WeightedCut.contractBlocks_pullbackCut {n m : ℕ} (part : Fin n → Fin (m + 1)) {u v : Fin (m + 1)} (huv : u ≠ v) : contractBlocks (fun (i : Fin (m + 1)) => pullbackCut part {i}) u v = fun (i : Fin m) => pullbackCut (contractPart part u v huv) {i}

Contracting the fibres of a supervertex map gives the fibres of the contracted map.