equivalence relations of matrices

Stream: new members

[Daniel Packer]

Hi,
I'm trying to show the matrix (unitary) similarity is an equivalence relation, but I keep running into the problem that Lean can't infer the size of the matrices I'm declaring the equivalence relation on, and I'm not sure how to tell it to use 'n' and 'F'

import analysis.inner_product_space.pi_L2
import linear_algebra.dimension
import linear_algebra.matrix

open_locale big_operators matrix

variables {F m n: Type*}
  [is_R_or_C F]
  [fintype m] [fintype n]
  [decidable_eq m] [decidable_eq n]
  [has_lt m] [has_lt n]

variables (A B : matrix n n F)

def unitarily_similar :=
  ∃ U : matrix n n F, A = U ⬝ B ⬝ Uᴴ

def equality (a : ℕ) (b : ℕ) := a = b

def matrix_equal := A = B

example : equivalence matrix_equal:=
begin
  sorry
end

[Daniel Packer]

This throws the error: image.png

[Daniel Packer]

(I'm using matrix_equal in case the existential quantifier had something to do with the error)

[Yaël Dillies]

The error message says it all. How could it know what the type of matrix_equal is? You need to type-ascript.

[Yaël Dillies]

One way to do it is

example : @equivalence (matrix n n F) matrix_equal :=

[Daniel Packer]

Ah! Thank you so much. I was trying various versions of that, but I couldn't figure out the right one

[Kyle Miller]

You might also consider making F and n be explicit arguments:

import analysis.inner_product_space.pi_L2
import linear_algebra.dimension
import linear_algebra.matrix

open_locale big_operators matrix

variables {m : Type*} (n : Type*) (F : Type*)
  [is_R_or_C F]
  [fintype m] [fintype n]
  [decidable_eq m] [decidable_eq n]
  [has_lt m] [has_lt n]

variables (A B : matrix n n F)

def unitarily_similar :=
  ∃ U : matrix n n F, A = U ⬝ B ⬝ Uᴴ

def equality (a : ℕ) (b : ℕ) := a = b

def matrix_equal := A = B

example : equivalence (matrix_equal n F) :=
begin
  sorry
end

[Eric Wieser]

Note the proof should be one line, it's docs#eq_equivalence or similar

[Daniel Packer]

I assume you mean for the matrix equality one? For unitarily similar, my proof was longer