Documentation

Complexity.Foundations.LinearAlgebra.Matrix.RectPermanent

Rectangular permanents and the Binet–Minc identity #

For a matrix b : Matrix m n R with finite row type m and column type n, the rectangular permanent b.rectPerm is the sum over all injections σ : m ↪ n of ∏ r, b r (σ r) Forbes, Def. 11. For a set Z of columns, b.rectPermSurj Z keeps only the injections whose image contains Z Forbes, Def. 20.

The main result is the Binet–Minc identity in permutation form, over any commutative ring:

∑_{σ : m ↪ n} ∏_r b r (σ r) = ∑_{π ∈ Perm m} sgn π ∏_{q ∈ orbits π} ∑_j ∏_{r ∈ q} b r j,

together with its inclusion–exclusion extension to rectPermSurj:

∑_{σ, Z ⊆ im σ} ∏_r b r (σ r) = ∑_π sgn π ∑_{Y ⊆ Z} (-1)^{|Y|} ∏_{q ∈ orbits π} ∑_{j ∉ Y} ∏_{r ∈ q} b r j.

Here orbits π is the quotient of m by Equiv.Perm.SameCycle π, so fixed points of π are orbits of size one.

Main definitions #

Main results #

Implementation notes #

The rows of b : Matrix m n R are indexed by m and the columns by n, following Mathlib. In Forbes's notation the matrix is n × m, with rows [n] and columns [m]. The definitions need no hypothesis card m ≤ card n: without it there are no injections and both sums are 0 (Matrix.rectPerm_eq_zero_of_card_lt). Forbes's Def. 20 requires the image to contain [k]; here any Z : Finset n is allowed.

Forbes, Thm. 13 states the Binet–Minc identity grouped by set partitions of the rows, with coefficient (-1)^{n - |F|} ∏_{S ∈ F} (|S| - 1)!. The permutation form proved here groups the same terms by permutation instead. The grouped form is not proved in this file. The permutation form, its inclusion–exclusion extension and this proof are original. The proof expands the product over orbits into a sum over functions constant on orbits, exchanges the two sums, and evaluates the signed sum over the stabiliser of each function with a sign-reversing involution.

References #

source
theorem Equiv.Perm.sum_sign_filter_apply_eq {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [DecidableEq n] (f : m → n) :
∑ π : Perm m with ∀ (r : m), f (π r) = f r, ↑(sign π) = if Function.Injective f then 1 else 0

The signed count of the permutations that fix every fibre of f is 1 if f is injective and 0 otherwise. A transposition of two rows with the same value pairs off the permutations with opposite signs.

source
theorem Equiv.Perm.apply_eq_of_sameCycle {m : Type u_1} {n : Type u_2} [Finite m] {π : Perm m} {f : m → n} (hf : ∀ (r : m), f (π r) = f r) {x y : m} (h : π.SameCycle x y) :
f x = f y

A function that is invariant under π is constant on the orbits of π.

source
@[instance_reducible]
instance Equiv.Perm.instDecidableRelSameCycleSetoid {m : Type u_1} [Fintype m] [DecidableEq m] (π : Perm m) :
DecidableRel ⇑(SameCycle.setoid π)

The orbit relation of a permutation of a finite type is decidable, so the type of its orbits is a Fintype with decidable equality.

source
noncomputable def Matrix.rectPerm {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] (b : Matrix m n R) :
R

The rectangular permanent: the sum over all injections σ : m ↪ n of ∏ r, b r (σ r) Forbes, Def. 11. It is 0 when card n < card m.

Instances For
    source
    noncomputable def Matrix.rectPermSurj {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq n] (Z : Finset n) (b : Matrix m n R) :
    R

    The rectangular permanent restricted to the injections whose image contains the columns Z. Forbes, Def. 20 is the case where Z is the set of the first k columns.

    Instances For
      source
      theorem Matrix.rectPerm_eq_sum_injective {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq m] [DecidableEq n] (b : Matrix m n R) :
      b.rectPerm = ∑ f : m → n with Function.Injective f, ∏ r : m, b r (f r)

      The rectangular permanent as a sum over injective functions.

      source
      theorem Matrix.rectPermSurj_eq_sum_injective {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq m] [DecidableEq n] (Z : Finset n) (b : Matrix m n R) :
      rectPermSurj Z b = ∑ f : m → n with Function.Injective f ∧ Z ⊆ Finset.image f Finset.univ, ∏ r : m, b r (f r)

      rectPermSurj as a sum over injective functions.

      source
      @[simp]
      theorem Matrix.rectPermSurj_empty {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq n] (b : Matrix m n R) :
      rectPermSurj ∅ b = b.rectPerm
      source
      theorem Matrix.rectPerm_eq_permanent {m : Type u_1} {R : Type u_3} [Fintype m] [CommSemiring R] [DecidableEq m] (M : Matrix m m R) :
      M.rectPerm = M.permanent

      On square matrices the rectangular permanent is Mathlib's Matrix.permanent.

      source
      theorem Matrix.rectPerm_eq_zero_of_card_lt {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] (b : Matrix m n R) (h : Fintype.card n < Fintype.card m) :
      b.rectPerm = 0

      The rectangular permanent vanishes when there are fewer columns than rows.

      source
      theorem Matrix.rectPermSurj_eq_zero_of_card_lt {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq n] (Z : Finset n) (b : Matrix m n R) (h : Fintype.card m < Z.card) :
      rectPermSurj Z b = 0

      rectPermSurj Z vanishes when Z has more columns than there are rows.

      source
      theorem Matrix.prod_quotient_sameCycle_sum_eq {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [CommSemiring R] [DecidableEq m] [DecidableEq n] (π : Equiv.Perm m) (T : Finset n) (b : Matrix m n R) :
      ∏ q : Quotient (Equiv.Perm.SameCycle.setoid π), ∑ j ∈ T, ∏ r : m with ⟦r⟧ = q, b r j = ∑ f ∈ Fintype.piFinset fun (x : m) => T with ∀ (r : m), f (π r) = f r, ∏ r : m, b r (f r)

      Expanding the product over the orbits of π of the column sums over T gives the sum over the functions into T that are constant on the orbits of π.

      source
      theorem Matrix.sum_injective_eq_sum_sign_prod_sameCycle {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [CommRing R] [DecidableEq m] [DecidableEq n] (T : Finset n) (b : Matrix m n R) :
      ∑ f ∈ Fintype.piFinset fun (x : m) => T with Function.Injective f, ∏ r : m, b r (f r) = ∑ π : Equiv.Perm m, Equiv.Perm.sign π • ∏ q : Quotient (Equiv.Perm.SameCycle.setoid π), ∑ j ∈ T, ∏ r : m with ⟦r⟧ = q, b r j

      Binet–Minc identity for injections into T, in permutation form: the sum over the injective functions f : m → n with values in T of ∏ r, b r (f r) is the signed sum over permutations π of m of the product over the orbits q of π of ∑_{j ∈ T} ∏_{r ∈ q} b r j. Original; Forbes, Thm. 13 states the case T = univ grouped by set partitions.

      source
      theorem Matrix.rectPerm_eq_sum_sign_prod_sameCycle {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [DecidableEq m] (b : Matrix m n R) :
      b.rectPerm = ∑ π : Equiv.Perm m, Equiv.Perm.sign π • ∏ q : Quotient (Equiv.Perm.SameCycle.setoid π), ∑ j : n, ∏ r : m with ⟦r⟧ = q, b r j

      Binet–Minc identity, in permutation form: the rectangular permanent is the signed sum over permutations π of the rows of the product over the orbits q of π of ∑_j ∏_{r ∈ q} b r j. Original form; Forbes, Thm. 13 states the identity grouped by set partitions of the rows.

      source
      theorem Matrix.rectPermSurj_eq_sum_sign_prod_sameCycle {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [DecidableEq m] [DecidableEq n] (Z : Finset n) (b : Matrix m n R) :
      rectPermSurj Z b = ∑ π : Equiv.Perm m, Equiv.Perm.sign π • ∑ Y ∈ Z.powerset, (-1) ^ Y.card * ∏ q : Quotient (Equiv.Perm.SameCycle.setoid π), ∑ j ∈ Yᶜ, ∏ r : m with ⟦r⟧ = q, b r j

      Binet–Minc identity with inclusion–exclusion (original): the sum over the injections whose image contains Z is the signed sum over permutations π of the rows of ∑_{Y ⊆ Z} (-1)^{|Y|} ∏_{q ∈ orbits π} ∑_{j ∉ Y} ∏_{r ∈ q} b r j. For Z = ∅ this is Matrix.rectPerm_eq_sum_sign_prod_sameCycle.