Permanents of rectangular matrices, and their Laplace expansion

The permanent of a matrix is the sum, over the bijections between its rows and its columns, of the products of the entries picked. Stated between two finite types rather than for square matrices (DescriptiveComplexity.bperm), it is the quantity every gadget argument about cycle covers or perfect matchings computes with: the number of perfect matchings of a bipartite graph is the permanent of its 0-1 biadjacency matrix (DescriptiveComplexity.bperm_boole), and the number of cycle covers of a digraph the permanent of its adjacency matrix.

The one tool the gadget arguments need is the Laplace expansion along a set of rows (DescriptiveComplexity.bperm_laplace): the permanent is the sum, over the sets S of columns of the right size, of the permanent of the rows on S times the permanent of the other rows on the other columns. Its consequences here: the vanishing when a row or a column is zero, the restriction of the expansion to the columns the rows are supported on (DescriptiveComplexity.bperm_laplace_of_support), and the factorization when a set of rows is supported on as many columns (DescriptiveComplexity.bperm_block).

noncomputable def DescriptiveComplexity.bperm {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) : R

The permanent of a rectangular matrix: the sum over the bijections between rows and columns of the products of the entries picked. It is 0 when the numbers of rows and columns differ.

Equations

• DescriptiveComplexity.bperm M = ∑ e : α ≃ β, ∏ a : α, M a (e a)

theorem DescriptiveComplexity.bperm_boole {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (P : α → β → Prop) [DecidableRel P] : (bperm fun (a : α) (b : β) => if P a b then 1 else 0) = ↑(Fintype.card { e : α ≃ β // ∀ (a : α), P a (e a) })

The permanent of a 0-1 matrix counts the bijections it contains.

The Laplace expansion along a set of rows

theorem DescriptiveComplexity.bperm_laplace {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (I : Finset α) : bperm M = ∑ S ∈ Finset.powersetCard I.card Finset.univ, (bperm fun (a : ↥I) (b : ↥S) => M ↑a ↑b) * bperm fun (a : { a : α // a ∉ I }) (b : { b : β // b ∉ S }) => M ↑a ↑b

The Laplace expansion of the permanent along the rows in I: the sum, over the sets S of as many columns, of the permanent of the rows I on the columns S times the permanent of the other rows on the other columns.

theorem DescriptiveComplexity.bperm_laplace_of_support {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (I : Finset α) (T : Finset β) (hT : ∀ a ∈ I, ∀ b ∉ T, M a b = 0) : bperm M = ∑ S ∈ Finset.powersetCard I.card T, (bperm fun (a : ↥I) (b : ↥S) => M ↑a ↑b) * bperm fun (a : { a : α // a ∉ I }) (b : { b : β // b ∉ S }) => M ↑a ↑b

The Laplace expansion, restricted to the columns the rows in I are supported on: the other column sets contribute nothing.

theorem DescriptiveComplexity.bperm_block {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (I : Finset α) (J : Finset β) (hJ : J.card = I.card) (hT : ∀ a ∈ I, ∀ b ∉ J, M a b = 0) : bperm M = (bperm fun (a : ↥I) (b : ↥J) => M ↑a ↑b) * bperm fun (a : { a : α // a ∉ I }) (b : { b : β // b ∉ J }) => M ↑a ↑b

Block factorization: when the rows in I are supported on as many columns J, the permanent is the permanent of the block I × J times the one of the complementary block.

Casting