# Zulip Chat Archive

## 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)
```

#### Johan Commelin (Mar 24 2021 at 07:01):

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