Naming contest: FreeMat?

Stream: maths

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

the categorical analogue of monoid_algebra.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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

[Scott Morrison]

Ah! :-) Now I see.

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

I made Mat C in #6845.

[Johan Commelin]

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

[Johan Commelin]

But thanks for the responses!

[Johan Commelin]

@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]

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

[Scott Morrison]

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

[Scott Morrison]

@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]

e.g.

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

[Johan Commelin]

Merci

[Scott Morrison]

and also

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

[Scott Morrison]

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