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