Zulip Chat Archive

Stream: maths

Topic: Naming contest: FreeMat?


view this post on Zulip Johan Commelin (Mar 23 2021 at 13:33):

Consider the following category:

  • objects: natural numbers
  • morphisms between mm and nn: the free abelian group Z[Matm×n]\Z[\mathrm{Mat}_{m \times n}] generated by m×nm \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?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 23 2021 at 13:40):

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

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:43):

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

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

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:43):

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

view this post on Zulip Johan Commelin (Mar 23 2021 at 13:53):

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

view this post on Zulip Scott Morrison (Mar 23 2021 at 22:47):

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

view this post on Zulip Scott Morrison (Mar 23 2021 at 22:47):

the categorical analogue of monoid_algebra.

view this post on Zulip 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.)

view this post on Zulip Scott Morrison (Mar 23 2021 at 22:51):

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

view this post on Zulip Scott Morrison (Mar 23 2021 at 22:53):

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

view this post on Zulip 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.)

view this post on Zulip 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!?

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip Adam Topaz (Mar 24 2021 at 00:18):

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

view this post on Zulip Scott Morrison (Mar 24 2021 at 00:28):

Ah! :-) Now I see.

view this post on Zulip Scott Morrison (Mar 24 2021 at 00:28):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Scott Morrison (Mar 24 2021 at 02:41):

I made Mat C in #6845.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 24 2021 at 06:35):

But thanks for the responses!

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Mar 24 2021 at 06:44):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:00):

e.g.

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

view this post on Zulip Johan Commelin (Mar 24 2021 at 07:01):

Merci

view this post on Zulip Scott Morrison (Mar 24 2021 at 07:10):

and also

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

view this post on Zulip 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