reducing determinate of a matrix

Stream: general

[Christopher Upshaw]

(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]

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]

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

[Anne Baanen]

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

[Scott Morrison]

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

[Scott Morrison]

(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]

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]

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]

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]

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]

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]

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

[Anne Baanen]

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]

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

[Anne Baanen]

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]

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]

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]

QED :-)

[Kenny Lau]

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]

oh curses I'm slightly slower

[Kevin Buzzard]

Well done to both of you, very nice

[Kevin Buzzard]

Now can you do 3*3? ;-)

[Anne Baanen]

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

[Scott Morrison]

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]

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

[Yakov Pechersky]

And induction

[Yakov Pechersky]

I had the wrong definition here.

[Yakov Pechersky]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

Ouch thanks :sweat_smile:

[Mario Carneiro]

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]

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