Coercion of 1x1 matrices

Stream: new members

[Yakov Pechersky]

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]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Yakov Pechersky]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

recover

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

You could just apply mul_comm and be done.

[Kevin Buzzard]

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]

The haveI's were in fact the problem

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Yakov Pechersky]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The time when you care is in the proof

[Kevin Buzzard]

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

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]

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