dimension 1 matrix

Stream: Is there code for X?

[Edison Xie]

Do we have that Matrix (Fin 1) (Fin 1) A ≃ₐ[K] A for A an K-algebra?

[Kevin Buzzard]

@loogle Matrix ?i ?i ?A, ?A

[loogle]

:search: Matrix.map_smul', Matrix.map_op_smul', and 2086 more

[Kevin Buzzard]

hmm that's quite a lot

@loogle Matrix ?i ?i ?A ≃ₐ[?B] ?A

[loogle]

:shrug: nothing found

[Eric Wieser]

@loogle Matrix ?i ?i, Unique ?i

[loogle]

:search: Matrix.diagonal_unique, Matrix.diag_col_mul_row, and 6 more

[Eric Wieser]

The statement I would expect is

example {n} [Unique n] .... : Matrix n n A ≃ₐ[K] A

[Kevin Buzzard]

Yeah it doesn't look like it (but Eric is right, it should be stated for a type with a Unique typeclass rather than just Fin 1)

[Eric Wieser]

And the ring version, and the "rectangular" version with {m n} [Unique m] [Unique n] for AddEquiv and LinearEquiv, etc

[Ruben Van de Velde]

import Mathlib

example {n A K : Type*} [Unique n] [Field A] [Field K] [Algebra K A] : Matrix n n A ≃ₐ[K] A where
  toFun m := m default default
  invFun a := .of fun _ _ => a
  left_inv m := by ext i j; simp [Subsingleton.elim i default, Subsingleton.elim j default]
  right_inv a := by simp
  map_mul' x y := by simp [Matrix.mul_apply]
  map_add' x y := by simp
  commutes' r := by aesop

[Eric Wieser]

I'm going to deduct marks for Field, but otherwise looks right

[Eric Wieser]

I think a PR should build the whole family of Unique equivalence on top of each other, not just that one at the end

[Edison Xie]

Eric Wieser said:

I think a PR should build the whole family of Unique equivalence on top of each other, not just that one at the end

which file do you think it belongs to and what name do you think it should be named as?

[Eric Wieser]

Maybe Matrix.uniqueEquiv, Matrix.uniqueAlgEquiv, etc

[Eric Wieser]

#find_home should give good suggestions for where to put them

[Ruben Van de Velde]

Yeah, I just wanted to force through to a :tada: asap, and let anyone who felt like it deconstruct it into mathlib-appropriate pieces

[Edison Xie]

pr #22375