Zulip Chat Archive

Stream: new members

Topic: Coercion of 1x1 matrices


view this post on Zulip Yakov Pechersky (Jun 16 2020 at 19:35):

I'm trying to figure out how has_lift and coe_* work. Right now I have the following definitions.

import data.real.basic
import linear_algebra.matrix

open_locale big_operators

universes u v
variables {n : Type u} [fintype n] [decidable_eq n]
variables (R : Type v) [add_comm_monoid R]

noncomputable instance matrix_lift (h : fintype.card n = 1) : has_lift (matrix n n R) R :=
begin
  rw fintype.card at h,
  rw finset.card_eq_one at h,
  rw finset.singleton_iff_unique_mem at h,
  choose b hb using h,
  exact ⟨λ M, M b b
end

noncomputable instance matrix_lift_t (h : fintype.card n = 1) : has_lift_t (matrix n n R) R :=
begin
  rw fintype.card at h,
  rw finset.card_eq_one at h,
  rw finset.singleton_iff_unique_mem at h,
  choose b hb using h,
  exact ⟨λ M, M b b
end

theorem coe_singleton {M : matrix n n R} {h : fintype.card n = 1} {a : n}
                      [has_lift_t (matrix n n R) R]:
                      (M : R) = M a a := sorry

I would think rfl would work, but there is a type mismatch. It also seems weird to me to be supplying a proof in the instance definition. Another issue is that I think using [has_lift_t ...] is non idiomatic, from looking at mathlib source.

view this post on Zulip Jalex Stark (Jun 16 2020 at 19:41):

is the problem that your instances are noncomputable but your theorem is not?

view this post on Zulip Jalex Stark (Jun 16 2020 at 19:42):

(I usually write noncomputable theory at the top of my file to avoid thinking about this)

view this post on Zulip Johan Commelin (Jun 16 2020 at 19:42):

I think that in practice it may be more useful to assume [unique n] instead of fintype.card n = 1.

view this post on Zulip Reid Barton (Jun 16 2020 at 19:42):

Lots of problems here, but ultimately the result can never be true by rfl because it would mean that any two elements of n are definitionally equal.

view this post on Zulip Reid Barton (Jun 16 2020 at 19:43):

You are taking a very mathematician-like attitude here: there's just one element anyways, so let's pick it.

view this post on Zulip Reid Barton (Jun 16 2020 at 19:45):

This works, sort of, but you will have to justify yourself to Lean later.

view this post on Zulip Yakov Pechersky (Jun 16 2020 at 20:37):

Thanks for the insight. Here's what I have currently. Seeing an error I haven't seen before, with "goals accomplished" yet red squiggly.

import data.real.basic
import linear_algebra.matrix

open_locale big_operators

universes u v
variables {n : Type u} [fintype n] [decidable_eq n]
variables (R : Type v)

instance matrix_coe [unique n] : has_coe (matrix n n R) R :=
let a := default n in ⟨λ M, M a a

theorem coe_singleton {M : matrix n n R} [unique n] {a : n} :
                      (M : R) = M a a :=
by { rw unique.uniq _ a, refl }

-- having a theorem that distributes the coe like `↑(A * B) = ↑A * ↑B`
-- is probably useful for what I'm trying to prove
-- which is the commutativity of 1-dim matrices

-- this statement does not work because I don't have ↑ in the statement
-- so I can't use `rw coe_singleton` later
-- example (A : matrix (fin 1) (fin 1) ℝ) (B : matrix (fin 1) (fin 1) ℝ) :
--         A * B = B * A := sorry

-- this errors at the end with
--   tactic failed, result contains meta-variables
--   state:
--   no goals
example (A : matrix (fin 1) (fin 1) ) (B : matrix (fin 1) (fin 1) ) : A * B = B * A :=
begin
  haveI : unique (fin 1) := by apply_instance,
  haveI: has_lift_t (matrix (fin 1) (fin 1) )  := by apply_instance,
  rw coe_singleton,
  rw coe_singleton,
  rw mul_comm,
  exact (default (fin 1)),
  exact (default (fin 1)), -- cursor on comma says "goals accomplished"
end

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:39):

Congratulations, you just got the "unproved invisible metavariable goal" achievement

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:39):

There's some tactic which will make the invisible goal appear, I always forget what it is.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:46):

recover

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:47):

recover, repeat {apply_instance}, finishes things properly. I don't really understand why this happens.

view this post on Zulip Reid Barton (Jun 16 2020 at 20:48):

I don't understand what the two haveIs could accomplish.

view this post on Zulip Reid Barton (Jun 16 2020 at 20:49):

Also, I'm not sure if you are proving what you want to prove.

view this post on Zulip Reid Barton (Jun 16 2020 at 20:50):

You could just apply mul_comm and be done.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:50):

If apply_instance works then the thing you proved was already known to type class inference so you didn't need to add it with haveI (and probably you should have used letI?)

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:50):

The haveI's were in fact the problem

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:51):

matrix X X R might not be known to be a semigroup.(it is)

view this post on Zulip Reid Barton (Jun 16 2020 at 20:51):

actually I guess I'm also not 100% sure what type ↑A is--if you have the has_coe instance anyways, better to write (A : ℝ).

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:53):

example (A : matrix (fin 1) (fin 1) ) (B : matrix (fin 1) (fin 1) ) :
  (A : ) * B = B * A :=
begin
  apply mul_comm,
end

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:54):

example (A : matrix (fin 1) (fin 1) ) (B : matrix (fin 1) (fin 1) ) :
  (A : ) * B = B * A := mul_comm _ _

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:54):

Lean doesn't have a clue where you're coercing to, I think

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 20:54):

If you tell it explicitly, as Reid suggests, it's much happier

view this post on Zulip Reid Barton (Jun 16 2020 at 20:55):

and example is like def in that it uses the body of the definition to elaborate the stated type of the example, so maybe that is where your metavariable(s) came from?

view this post on Zulip Reid Barton (Jun 16 2020 at 20:56):

anyways, all of this is just dancing around the actual work, which is proving that multiplication of 1x1 matrices corresponds to multiplication in R

view this post on Zulip Yakov Pechersky (Jun 16 2020 at 21:06):

Totally clear now:

import data.real.basic
import linear_algebra.matrix

open_locale big_operators

universes u v
variables {n : Type u} [fintype n] [decidable_eq n]
variables (R : Type v)

instance matrix_coe [unique n] : has_coe (matrix n n R) R :=
let a := default n in ⟨λ M, M a a

theorem coe_singleton {M : matrix n n R} [unique n] {a : n} :
                      (M : R) = M a a :=
by { rw unique.uniq _ a, refl }

example (A : matrix (fin 1) (fin 1) ) (B : matrix (fin 1) (fin 1) ) :
                   (A : ) * B = B * A :=
mul_comm _ _

But thinking about how to formalize the proof that n x n matrices commute over the entirety of the space, is valid only for n <= 1, one would need the theory of eigenvectors, which mathlib does not yet have. Correct?

example {n : } (h :  (A : matrix (fin n) (fin n) ) (B : matrix (fin n) (fin n) ), A * B = B * A) :
        n <= 1 := sorry

view this post on Zulip David Wärn (Jun 16 2020 at 21:31):

If you want to show there are non-commuting matrices for n >= 2, why not just look at an explicit example? Say

10 * 01
00   00

view this post on Zulip Yakov Pechersky (Jun 16 2020 at 21:51):

Sure, and show by induction ... . For a proof that did not rely on calculation, I was thinking about the one at https://math.stackexchange.com/a/27832, and then show that all matrices are equal to c * I for some scalar c only for n = 0 \or n = 1.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:10):

You don't need any induction here. David's matrices are n x n

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:11):

It's just some "if first variable is 0 and second is 1 then 1 else 0" matrix

view this post on Zulip Yakov Pechersky (Jun 16 2020 at 22:37):

I think you still need induction to show that fin n for n >= 2 has has_zero and has_one instances, so that those matrices can be defined via an ite call.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:53):

This is not induction. You need to prove 0 < n and 1 < n but both of these follow directly from 2<= n

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:53):

The ite doesn't care if its clause is never satisfied

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:56):

The time when you care is in the proof

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 08:56):

@Yakov Pechersky sorry, I had to sleep :-)

import data.matrix.notation

variables {R : Type*} [ring R] [nonzero R]

example (n : ) :
   (S : matrix (fin (n+2)) (fin (n+2)) R) (T : matrix (fin (n+2)) (fin (n+2)) R),
          S * T  T * S :=
begin
  use (λ a b, if a = 0  b = 1 then 1 else 0),
  use (λ a b, if a = 0  b = 0 then 1 else 0),
  intro h,
  replace h := congr_fun (congr_fun h 0) 1,
  simp [matrix.mul, matrix.dot_product] at h,
  apply @zero_ne_one R,
  convert h,
end

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 08:58):

Poking around in the library a bit for the has_one issue revealed that the trick is to work with fin (n+2).

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 09:06):

I'm a bit unhappy with that nonterminal simp: I'm slightly less unhappy, but still unhappy, with

begin
  use (λ a b, if a = 0  b = 1 then 1 else 0),
  use (λ a b, if a = 0  b = 0 then 1 else 0),
  intro h,
  replace h := congr_fun (congr_fun h 0) 1,
  have h2 : ite ((1 : fin (n + 2)) = 0) (1 : R) 0 = 1,
    simp [matrix.mul, matrix.dot_product] at h, exact h,
  apply @zero_ne_one R,
  convert h2,
end

Last updated: May 16 2021 at 21:11 UTC