Matrices of matrices

Stream: Is there code for X?

[Kevin Buzzard]

Do we have these? Do we want them? A student here needs them and can't find them.

import Mathlib.Data.Matrix.Basic

namespace Matrix

variable (I J K L R : Type*)

def comp_equiv : Matrix I J (Matrix K L R) ≃ Matrix (I × K) (J × L) R where
  toFun m ik jl := m ik.1 jl.1 ik.2 jl.2
  invFun n i j k l := n (i, k) (j, l)
  left_inv _ := rfl
  right_inv _ := rfl

section AddCommMonoid_stuff

variable [AddCommMonoid R]

def comp_equiv_AddMonoidHom : Matrix I J (Matrix K L R) ≃+ Matrix (I × K) (J × L) R :=
{ Matrix.comp_equiv I J K L R with
  map_add' := fun _ _ ↦ rfl
}

end AddCommMonoid_stuff

section Semiring_stuff

variable [Semiring R] [Fintype I] [Fintype J]

def comp_equiv_RingHom : Matrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R :=
{ Matrix.comp_equiv_AddMonoidHom I I J J R with
  map_mul' := fun m n ↦ by
    ext _ _
    exact (Matrix.sum_apply _ _ _ _).trans <| Eq.symm Fintype.sum_prod_type
}

end Semiring_stuff

[Riccardo Brasca]

I've never seen anything like that in mathlib, but I am not 100% sure. Anyway it can surely be useful (and you probably have something in mind...)

[Kevin Buzzard]

It apparently comes up in the theory of central simple algebras and Morita equivalence.

[Bhavik Mehta]

Note that if they do get added, docs#Matrix.of should be used to construct the matrices, to give you better automation when using these matrices

[Martin Dvořák]

Please please please add them to Mathlib!

[Junyan Xu]

When I used these in #19978 I didn't realize they are recent additions (#14512) :)