# Zulip Chat Archive

## 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):

Aha, but adding parentheses around the addition 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: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 }
```

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

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 :
by simp_rw [zero_add, mul_one, one_mul, add_zero, neg_one_mul, sub_eq_add_neg]
```

#### 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

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

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 `i`

th 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
)))).add +
((-[1+ 0].mul ( -1 * (_ * 1)
(A.val ⟨1, _⟩ ⟨0, _⟩).mul (
int.of_nat 1
))).add ( +
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