# Zulip Chat Archive

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

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

(it is)`matrix X X R`

might not be known to be a semigroup.

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