## Stream: general

### Topic: reducing determinate of a matrix

#### Christopher Upshaw (Jul 09 2020 at 12:44):

(Is this how I ask a question?)
How do I get finset.univ.sum (λ (σ : equiv.perm n), ↑↑(⇑equiv.perm.sign σ) * finset.univ.prod (λ (i : n), M (⇑σ i) i)) (i.e the definition of determinant in linear_algebra) to reduce to the formula m.det = (m 0 0) * (m 1 1) - (m 0 1) * (m 1 0) (in the case n = fin 2)?

#### Anne Baanen (Jul 09 2020 at 12:48):

I don't believe there is an easy way to do this, since finset.sum is not really designed for computation. Either you would have to show finset.univ : finset (equiv.perm (fin 2)) is equal to a specific list of permutations, or you need to do some tricks with reducing the expression enough that simp or rw can deal with it.

#### Scott Morrison (Jul 09 2020 at 12:52):

Like we have fin_cases, we need a tactic that "writes out a sum"

#### Anne Baanen (Jul 09 2020 at 12:54):

It might be relevant to my talk on linear algebra next week, so let's see how far I get.

#### Scott Morrison (Jul 09 2020 at 12:55):

(And yes, @Christopher Upshaw, this is how you ask a question! :-)

#### Scott Morrison (Jul 09 2020 at 12:56):

(You might be disappointed by how often questions are answered with "hmm... we should make that work". But then hopefully you'll be pleased by how often someone then makes it work. :-)

#### Anne Baanen (Jul 09 2020 at 12:57):

We could try a proof like this:

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = _ /- fill in something clever -/ : refl
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring }


#### Anne Baanen (Jul 09 2020 at 12:58):

The obvious choice is to ask Lean to reduce M.det as much as it can with the command #reduce M.det, but that gives a timeout.

#### Anne Baanen (Jul 09 2020 at 12:59):

So let's just guess that Lean can reduce finset.sum to a sum of two things, and that works:

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = _ + _ : refl _
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring } -- error: focused goal has not been solved


#### Anne Baanen (Jul 09 2020 at 13:00):

But it's not a sum of three things:

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = _ + _ + _ : refl _ -- error: type mismatch
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring }


#### Anne Baanen (Jul 09 2020 at 13:01):

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = _ + (_ + _) : refl _
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring } -- error: focused goal has not been solved


#### Anne Baanen (Jul 09 2020 at 13:02):

In fact, the last term should be 0: _ + (_ + 0) doesn't give a type error.

#### Anne Baanen (Jul 09 2020 at 13:03):

Let's check out the goal that simp, ring didn't solve:

(∏ (x : fin 2), M (⇑(⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) 1) x) x) *
↑↑(sign (⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) 1)) +
(∏ (x : fin 2),
M (⇑(⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) (swap ⟨0, _⟩ ⟨1, _⟩)) x) x) *
↑↑(sign (⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) (swap ⟨0, _⟩ ⟨1, _⟩))) =
M 1 1 * M 0 0 - M 0 1 * M 1 0


#### Anne Baanen (Jul 09 2020 at 13:03):

Looks like we need to do the same trick with these products as we did for the sum.

#### Anne Baanen (Jul 09 2020 at 13:04):

Yup, this doesn't give a type error:

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = (_ * (_ * (_ * 1))) + ((_ * (_ * (_ * 1))) + 0) : refl _
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring } -- error: focused goal has not been solved


#### Anne Baanen (Jul 09 2020 at 13:06):

Looking at the goal again, we get:

⊢ M (⇑(⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) 1) ⟨1, _⟩) ⟨1, _⟩ *
M (⇑(⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) 1) ⟨0, _⟩) ⟨0, _⟩ *
↑↑(sign (⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) 1)) +
M (⇑(⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) (swap ⟨0, _⟩ ⟨1, _⟩)) ⟨1, _⟩)
⟨1, _⟩ *
M (⇑(⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) (swap ⟨0, _⟩ ⟨1, _⟩)) ⟨0, _⟩)
⟨0, _⟩ *
↑↑(sign (⇑((equiv.refl (fin 2)).equiv_congr (equiv.refl (fin 2))) (swap ⟨0, _⟩ ⟨1, _⟩))) =
M 1 1 * M 0 0 - M 0 1 * M 1 0


So we should just fill in some values and we can finish.

#### Anne Baanen (Jul 09 2020 at 13:09):

And with a bit of fiddling with the coercions, we get:

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = ((1 : units ℤ) * (_ * (_ * 1))) + (((-1 : units ℤ) * (_ * (_ * 1))) + 0) : refl M.det
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring }


QED :-)

#### Kenny Lau (Jul 09 2020 at 13:10):

import linear_algebra.matrix

lemma det_2x2 {R : Type*} [comm_ring R] (M : matrix (fin 2) (fin 2) R) :
M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = ((0 + 1) * (M 0 0 * (M 1 1 * 1)) + (-(0 + 1) * (M 1 0 * (M 0 1 * 1)) + 0) : R) : rfl
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 :


#### Kenny Lau (Jul 09 2020 at 13:11):

oh curses I'm slightly slower

#### Kevin Buzzard (Jul 09 2020 at 14:43):

Well done to both of you, very nice

#### Kevin Buzzard (Jul 09 2020 at 14:44):

Now can you do 3*3? ;-)

#### Anne Baanen (Jul 09 2020 at 14:46):

I can do it, but I won't :upside_down:

#### Scott Morrison (Jul 10 2020 at 00:12):

If we had a tactic that, like fin_cases, used eval_expr to obtain an underlying list, and replaced the finset.prod with an explicit list.prod over that list, how helpful would that be in these cases?

#### Yakov Pechersky (Jul 10 2020 at 00:16):

It's probably easier to show the n x n case via the definition of det that uses minors

And induction

#### Yakov Pechersky (Jul 10 2020 at 00:48):

I had the wrong definition here.

#### Yakov Pechersky (Jul 10 2020 at 00:56):

Something more like this. Still not sure how to generate the ni \neq i on the fly:

def det_via_minors {n : ℕ} {R : Type*} [field R]
(M : matrix (fin (n + 1)) (fin (n + 1)) R) (i : fin (n + 1)) : R :=
let c := λ j : fin (n + 1), (-1 : R) ^ (i.val + j.val) in
∑ j, (M i j • (c j • minor M (λ ni, fin.pred_above i ni _) (λ nj, fin.pred_above j nj _)))
---
still wrong


#### Anne Baanen (Jul 10 2020 at 08:39):

Not suggesting that you need to change your approach, but: when I was working with minors to define the adjugate, I found it easier to define it in terms of Cramer's map. So instead of directly removing a row and column from the matrix, set the ith column to the j'th basis vector. And as the next step, show that going from cramer_map A to minor A doesn't change the determinant.

#### Yakov Pechersky (Jul 10 2020 at 12:36):

I'll try that out. But if the idea is to reduce the det of an explicit 2 x 2 matrix to the ad - bc term, wouldn't relying on a linear map make that difficult?

#### Eloi (Jul 25 2020 at 22:13):

Anne Baanen said:

We could try a proof like this:

lemma det_2x2 (M : matrix (fin 2) (fin 2) R) : M.det = M 0 0 * M 1 1 - M 1 0 * M 0 1 :=
calc M.det = _ /- fill in something clever -/ : refl
... = M 0 0 * M 1 1 - M 1 0 * M 0 1 : by { simp, ring }


Hi, I tried this method but for the inverse, and it worked sometimes:
This works fine:

import tactic
import linear_algebra.special_linear_group
open matrix

lemma inverse₀₀ (M : special_linear_group (fin 2) ℤ): M⁻¹ 0 0 = M 1 1 :=
calc M⁻¹ 0 0 = (1*(1* ( _ * 1))) + ( -1 *( _ * 0) + 0): refl _
... = M 1 1 : by {simp, ring}

lemma inverse₀₁ (M : special_linear_group (fin 2) ℤ): M⁻¹ 0 1 = - M 0 1 :=
calc M⁻¹ 0 1 = (1 * (_ * 0)) + (-1 * (1* (_ * 1)) + 0): refl _
... = - M 0 1 :by {simp, ring}


but I don't know how to make this one work:

lemma inverse₁₀ (M : special_linear_group (fin 2) ℤ): M⁻¹ 1 0 = - M 1 0 :=
calc M⁻¹ 0 1 = (1 * (_ * (_ * 1))) + (-1 * (_ * _) + 0): refl _
... = - M 0 1 :by {simp, ring}


Using #reduce I obtain:

variables A : special_linear_group (fin 2) ℤ
#reduce A⁻¹ 1 0
-- result:
/-
(
(int.of_nat 1).mul(                     This is 1 * ( 0 * (_ * 1))
(int.of_nat 0).mul (
(A.val ⟨1, _⟩ ⟨1, _⟩).mul (
int.of_nat 1
((-[1+ 0].mul (                                -1 * (_ * 1)
(A.val ⟨1, _⟩ ⟨0, _⟩).mul (
int.of_nat 1
int.of_nat 0))                                  0
-/


but writing

lemma inverse₁₀ (M : special_linear_group (fin 2) ℤ): M⁻¹ 1 0 = - M 1 0 :=
calc M⁻¹ 0 1 = (1 * (_ * (_ * 1))) + (-1 * (_ * 1) + 0): refl _
... = - M 0 1 :by {simp, ring}


does not work. However writing the 1 in the "wrong" place works¿?:

lemma inverse₁₀ (M : special_linear_group (fin 2) ℤ): M⁻¹ 1 0 = - M 1 0 :=
calc M⁻¹ 0 1 = (1 * (_ * (_ * 1))) + (-1 * (1 * _) + 0): refl _
... = - M 0 1 :by {simp, ring}


After that I get stuck and I can't make it work.

Thanks, and sorry for the long question :scroll:

#### Mario Carneiro (Jul 25 2020 at 22:26):

you got the indices wrong on  M⁻¹ 1 0 and - M 1 0

#### Mario Carneiro (Jul 25 2020 at 22:27):

lemma inverse₁₀ (M : special_linear_group (fin 2) ℤ): M⁻¹ 1 0 = - M 1 0 :=
calc M⁻¹ 1 0 = (1 * (0 * (_ * 1))) + (-1 * (_ * _) + 0): rfl
... = - M 1 0 : by {simp, ring}


#### Eloi (Jul 25 2020 at 22:32):

Ouch thanks :sweat_smile:

#### Mario Carneiro (Jul 25 2020 at 22:33):

by the way, you can be even more clever with this kind of proof, since rfl lines are always redundant in calc:

lemma inverse₁₀ (M : special_linear_group (fin 2) ℤ): M⁻¹ 1 0 = - M 1 0 :=
show (1 * (0 * (_ * 1)) : ℤ) + (-1 * (_ * _) + 0) = _, by {simp, ring}


#### Yakov Pechersky (Feb 16 2021 at 16:05):

Finally, due to #5593, we have:

import data.matrix.notation
import linear_algebra.determinant
import group_theory.perm.fin
import tactic.norm_swap

example {α : Type*} [comm_ring α] {a b c d : α} :
matrix.det ![![a, b], ![c, d]] = a * d - b * c :=
begin
simp [matrix.det, finset.univ_perm_fin_succ, ←finset.univ_product_univ, finset.sum_product,
fin.sum_univ_succ, fin.prod_univ_succ],
ring
end

example {α : Type*} [comm_ring α] (A : matrix (fin 3) (fin 3) α) {a b c d e f g h i : α} :
matrix.det ![![a, b, c], ![d, e, f], ![g, h, i]] =
a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
begin
-- We utilize the norm_swap plugin for norm_num to reduce swap terms
norm_num [matrix.det, finset.univ_perm_fin_succ, ←finset.univ_product_univ,
finset.sum_product, fin.sum_univ_succ, fin.prod_univ_succ],
ring
end
`

Last updated: May 08 2021 at 02:46 UTC