## Stream: maths

### Topic: Naming contest: FreeMat?

#### Johan Commelin (Mar 23 2021 at 13:33):

Consider the following category:

• objects: natural numbers
• morphisms between $m$ and $n$: the free abelian group $\Z[\mathrm{Mat}_{m \times n}]$ generated by $m \times n$-matrices.

How do you call this gadget? The best I could come up with is FreeMat. But maybe there is a better name out there?

#### Damiano Testa (Mar 23 2021 at 13:37):

Just to make sure that I understand: this is equivalent to the category of free, Z-modules with a finite basis, right?

#### Johan Commelin (Mar 23 2021 at 13:40):

Then you would only have $\mathrm{Mat}_{m \times n}$ as morphisms, right?

#### Damiano Testa (Mar 23 2021 at 13:43):

Ah, you are right: I read $\mathbb{Z} [..]$ as $\textrm{Mat}_{...} (\mathbb{Z})$!

... whereas, this is some form of group completion on the morphisms.

#### Damiano Testa (Mar 23 2021 at 13:43):

Also, I am not sure that I know of a better name.

#### Johan Commelin (Mar 23 2021 at 13:53):

Ooh yeah, I should have specified that the matrices have $\Z$ coefficients as well

#### Scott Morrison (Mar 23 2021 at 22:47):

You're going to factor this into a general construction, right?

#### Scott Morrison (Mar 23 2021 at 22:47):

the categorical analogue of monoid_algebra.

#### Scott Morrison (Mar 23 2021 at 22:48):

(This is a common pattern, e.g. formal linear combinations of cobordisms or diagrams in quantum topology.)

#### Scott Morrison (Mar 23 2021 at 22:51):

So it should bee something like Free ℤ (Mat ℤ), given appropriate definitions of Free and Mat.

#### Scott Morrison (Mar 23 2021 at 22:53):

(Presumably also you want objects to by fintypes, not nats.)

#### Scott Morrison (Mar 23 2021 at 22:56):

(huh... I could swear we used to have a dmatrix type (dependently typed matrices)... but it seems I'm crazy.)

#### Adam Topaz (Mar 23 2021 at 23:34):

In what level of generality does it make sense to define this? I guess something similar can be done for every category, where this is the case of Mat which is the category with naturals as objects and matrices as morphisms. I guess you can even replace free abelian groups with any functor from types!?

#### Scott Morrison (Mar 24 2021 at 00:03):

I would have said Mat C makes sense for any preadditive C. Its objects are finite tuples of objects of C, and its morphisms are dependently typed matrices.

#### Scott Morrison (Mar 24 2021 at 00:03):

I'm failing to work out where the generalisation free abelian groups to functor from types is happening. :-)

#### Adam Topaz (Mar 24 2021 at 00:18):

Maybe to be more precise, the functor should be a lax monoidal endofunctor on Type*

#### Scott Morrison (Mar 24 2021 at 00:28):

Ah! :-) Now I see.

#### Scott Morrison (Mar 24 2021 at 00:28):

We do have those, ready to go. :-)

#### Scott Morrison (Mar 24 2021 at 00:29):

It's a special case of changing the category you're enriching over, just in this case going from Type to Type you stay in the land of non-enriched categories.

#### Scott Morrison (Mar 24 2021 at 00:29):

(Lax monoidal functors are exactly what you're allowed to apply to the hom-objects of an enriched category.)

#### Scott Morrison (Mar 24 2021 at 02:41):

I made Mat C in #6845.

#### Johan Commelin (Mar 24 2021 at 06:35):

Hmm, I will have to think about whether Fintype instead of nat as object type will work well in my use case

#### Johan Commelin (Mar 24 2021 at 06:35):

But thanks for the responses!

#### Johan Commelin (Mar 24 2021 at 06:37):

@Scott Morrison But your PR doesn't even use any matrix under the hood, right. So it will be hard to use the API for matrix (fin n) (fin m)

#### Scott Morrison (Mar 24 2021 at 06:44):

You're right. It does use dmatrix, which is new.

#### Scott Morrison (Mar 24 2021 at 06:44):

I will think about how to make it smoother in the case where C only has one object to begin with.

#### Scott Morrison (Mar 24 2021 at 06:59):

@Johan Commelin, okay, I fixed this, hopefully to your satisfaction. Now Mat_ C is the full categorical construction for any preadditive category C, and Mat R is the construction for a ring, and it has objects \nat.

#### Scott Morrison (Mar 24 2021 at 07:00):

e.g.

example : matrix (fin 3) (fin 3) ℤ := 𝟙 (Mat.of ℤ 3)


Merci

#### Scott Morrison (Mar 24 2021 at 07:10):

and also

example : Mat.of ℤ 2 ⟶ Mat.of ℤ 3 := ![![(37 : ℤ), 42, 0], ![0, 37, 42]]


#### Scott Morrison (Mar 24 2021 at 07:12):

(It does intrinsically require a ring, not a semiring, however.)

Last updated: May 06 2021 at 18:20 UTC