Zulip Chat Archive

Stream: general

Topic: reducing determinate of a matrix


view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 09 2020 at 12:52):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 09 2020 at 12:55):

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

view this post on Zulip 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. :-)

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip Anne Baanen (Jul 09 2020 at 13:02):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Anne Baanen (Jul 09 2020 at 13:10):

QED :-)

view this post on Zulip 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]

view this post on Zulip Kenny Lau (Jul 09 2020 at 13:11):

oh curses I'm slightly slower

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 14:43):

Well done to both of you, very nice

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 14:44):

Now can you do 3*3? ;-)

view this post on Zulip Anne Baanen (Jul 09 2020 at 14:46):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jul 10 2020 at 00:17):

And induction

view this post on Zulip Yakov Pechersky (Jul 10 2020 at 00:48):

I had the wrong definition here.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Jul 25 2020 at 22:26):

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

view this post on Zulip 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}

view this post on Zulip Eloi (Jul 25 2020 at 22:32):

Ouch thanks :sweat_smile:

view this post on Zulip 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}

view this post on Zulip 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