Minors of the permanent

DescriptiveComplexity.pdel M A B is the permanent of the matrix M with the rows in A and the columns in B deleted. Stating the expansions of the permanent on minors indexed by sets of deleted rows and columns, rather than on nested subtypes, is what lets two expansions in different orders meet: deleting the row u then the row u' is deleting {u, u'}.

• DescriptiveComplexity.pdel_laplace_of_support: the Laplace expansion along a set of rows, restricted to the columns they are supported on, on minors.
• DescriptiveComplexity.pdel_row and DescriptiveComplexity.pdel_col: the expansion along one row or column; DescriptiveComplexity.pdel_row_single and DescriptiveComplexity.pdel_col_single when the line has a single nonzero entry; DescriptiveComplexity.pdel_row_zero and DescriptiveComplexity.pdel_col_zero when it has none.
• DescriptiveComplexity.pdel_block: the factorization when a set of rows is supported on as many columns.

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

The permanent of a minor: the matrix with the rows in A and the columns in B deleted.

Equations

• DescriptiveComplexity.pdel M A B = DescriptiveComplexity.bperm fun (a : { a : α // a ∉ A }) (b : { b : β // b ∉ B }) => M ↑a ↑b

theorem DescriptiveComplexity.pdel_laplace_of_support {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) (I : Finset α) (T : Finset β) (hIA : ∀ a ∈ I, a ∉ A) (hTB : ∀ b ∈ T, b ∉ B) (hT : ∀ a ∈ I, ∀ b ∉ B, b ∉ T → M a b = 0) : pdel M A B = ∑ S ∈ Finset.powersetCard I.card T, (bperm fun (x : ↥I) (y : ↥S) => M ↑x ↑y) * pdel M (A ∪ I) (B ∪ S)

The Laplace expansion of a minor along the rows in I, restricted to the columns T those rows are supported on.

theorem DescriptiveComplexity.pdel_block {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) (I : Finset α) (J : Finset β) (hIA : ∀ a ∈ I, a ∉ A) (hJB : ∀ b ∈ J, b ∉ B) (hJ : J.card = I.card) (hT : ∀ a ∈ I, ∀ b ∉ B, b ∉ J → M a b = 0) : pdel M A B = (bperm fun (x : ↥I) (y : ↥J) => M ↑x ↑y) * pdel M (A ∪ I) (B ∪ J)

Block factorization: rows supported on as many columns.

theorem DescriptiveComplexity.pdel_row {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) {a : α} (ha : a ∉ A) : pdel M A B = ∑ b ∈ Bᶜ, M a b * pdel M (insert a A) (insert b B)

Expansion along a row.

theorem DescriptiveComplexity.pdel_col {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) {b : β} (hb : b ∉ B) : pdel M A B = ∑ a ∈ Aᶜ, M a b * pdel M (insert a A) (insert b B)

Expansion along a column.

theorem DescriptiveComplexity.pdel_row_single {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) {a : α} (ha : a ∉ A) {b : β} (hb : b ∉ B) (h : ∀ b' ∉ B, b' ≠ b → M a b' = 0) : pdel M A B = M a b * pdel M (insert a A) (insert b B)

A row with a single nonzero entry.

theorem DescriptiveComplexity.pdel_col_single {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) {b : β} (hb : b ∉ B) {a : α} (ha : a ∉ A) (h : ∀ a' ∉ A, a' ≠ a → M a' b = 0) : pdel M A B = M a b * pdel M (insert a A) (insert b B)

A column with a single nonzero entry.

theorem DescriptiveComplexity.pdel_row_zero {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) {a : α} (ha : a ∉ A) (h : ∀ b ∉ B, M a b = 0) : pdel M A B = 0

A zero row.

theorem DescriptiveComplexity.pdel_col_zero {R : Type} [CommSemiring R] {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : α → β → R) (A : Finset α) (B : Finset β) {b : β} (hb : b ∉ B) (h : ∀ a ∉ A, M a b = 0) : pdel M A B = 0

A zero column.

An isolated node with a self-loop