Minors of matrices (square and non-square)

Stream: Is there code for X?

[Swarnava Chakraborty]

So, I was thinking of proving the Kirchoff's Matrix Tree Theorem in Lean. I would need Minors of the Laplacian and Incidence matrices of SimpleGraphs for the same. I am not sure whether these are defined. Can someone help me?
P.S. I am only dealing with Matrices of type Matrix Finset (Fin n) Finset (Fin m) Int

[Martin Dvořák]

You mean Matrix X Y ℤ where (X : Finset (Fin n)) and (Y : Finset (Fin m)) right?
Perhaps Matrix X Y ℤ where (X : Type) [Fintype X] and (Y : Type) [Fintype Y] could be more convenient, I'm not sure.

[Swarnava Chakraborty]

Either way, is there a function for getting the minor of such a matrix?

[Eric Wieser]

Are you looking for docs#Matrix.submatrix (combined with Matrix.det)?

[Swarnava Chakraborty]

Yes , but a simplified form of this, like if I only want to remove one row and one column, let's say.

[Swarnava Chakraborty]

Nevertheless, this would work for my case with some modifications, I hope, Thanks!

[Eric Wieser]

Are you perhaps looking for docs#Matrix.det_eq_sum_column_mul_submatrix_succAbove_succAbove_det ?

[Swarnava Chakraborty]

What I am exactly looking for is called the Cauchy-Binet Theorem. For making the statement, I would need some specific rows and columns removed (may be none removed) from a rectangular Matrix. i wrote the following code but is getting an error.

def all_subsets_of_size (n m : ℕ) : Finset (Finset (Fin m)) :=
  Finset.powersetCard n (Finset.univ)
noncomputable def submatrix' {n m : ℕ} {α : Type} [Zero α] (A : Matrix (Fin n) (Fin m) α)
  (rows : Finset (Fin n)) (cols : Finset (Fin m)) :
    Matrix (Fin rows.card) (Fin cols.card) α :=
  fun i j => A (rows.toList.get ⟨i.1, by simp [i.2]⟩) (cols.toList.get ⟨j.1, by simp [j.2]⟩)
def zero_to_n_minus_one (n : Nat) : Finset (Fin n) := Finset.univ

#check Finset.card_univ

theorem zero_to_n_minus_one_card_eq_n {n : ℕ} : (zero_to_n_minus_one n).card = n := by
  simp [zero_to_n_minus_one, Finset.card_univ]

noncomputable def Matrix.rowBlocks {n m : ℕ} (N : Matrix (Fin n) (Fin m) Int) (s : Finset (Fin m)) : Matrix (Fin n) (Fin s.card) Int
        := by rw [← @zero_to_n_minus_one_card_eq_n n] ; exact submatrix' N (zero_to_n_minus_one n) s



noncomputable def Matrix.colBlocks {n m : ℕ } (N : Matrix (Fin n) (Fin m) Int) (s : Finset (Fin n)) : Matrix (Fin s.card) (Fin m) Int
  := by rw [← @zero_to_n_minus_one_card_eq_n m] ; exact submatrix' N s (zero_to_n_minus_one m)

/-
typeclass instance problem is stuck, it is often due to metavariables
  Fintype (?m.30343 s)
-/

theorem CauchyBinet {m n : Nat} (M : Matrix (Fin m) (Fin n) Int) (N : Matrix (Fin n) (Fin m) Int) :
  (M * N).det = ∑ s ∈ all_subsets_of_size n m,
  (Matrix.colBlocks M s).det * (Matrix.rowBlocks N s).det :=
  by sorry

I have no idea why this happens.

[Eric Wieser]

I suspect the Finset and Fin stuff is going to make this harder

[Notification Bot]

A message was moved from this topic to #Is there code for X? > Cauchy Binet theorem by Eric Wieser.

[Eric Wieser]

(turns out we had a more aptly-named thread for this, so put my suggestion there instead)

[Swarnava Chakraborty]

Okay Thanks!