## Stream: new members

### Topic: Coercion of 1x1 matrices

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

#### Jalex Stark (Jun 16 2020 at 19:41):

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

#### Jalex Stark (Jun 16 2020 at 19:42):

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

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

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

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

#### Reid Barton (Jun 16 2020 at 19:45):

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

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


#### Kevin Buzzard (Jun 16 2020 at 20:39):

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

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

#### Kevin Buzzard (Jun 16 2020 at 20:46):

recover

#### Kevin Buzzard (Jun 16 2020 at 20:47):

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

#### Reid Barton (Jun 16 2020 at 20:48):

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

#### Reid Barton (Jun 16 2020 at 20:49):

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

#### Reid Barton (Jun 16 2020 at 20:50):

You could just apply mul_comm and be done.

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

#### Kevin Buzzard (Jun 16 2020 at 20:50):

The haveI's were in fact the problem

#### Kevin Buzzard (Jun 16 2020 at 20:51):

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

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

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


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


#### Kevin Buzzard (Jun 16 2020 at 20:54):

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

#### Kevin Buzzard (Jun 16 2020 at 20:54):

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

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

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

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


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


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

#### Kevin Buzzard (Jun 16 2020 at 22:10):

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

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

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

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

#### Kevin Buzzard (Jun 16 2020 at 22:53):

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

#### Kevin Buzzard (Jun 16 2020 at 22:56):

The time when you care is in the proof

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


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

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