## Stream: new members

### Topic: Preferring zmod over fin

#### Yakov Pechersky (Aug 13 2020 at 21:25):

A lot of recent threads have been about some of the missing API in fin. Would zmod be a better choice for some things? For example, if I want to talk about the minor of a matrix (fin (n + 1)) (fin (n + 1)) R, or by dropping a row and column via succ_above, would this be easier if I just chose to use zmod? @Kenny Lau

#### Kenny Lau (Aug 13 2020 at 21:31):

but the matrix API doesn't support zmod right

#### Patrick Massot (Aug 13 2020 at 21:33):

What part of the API?

#### Patrick Massot (Aug 13 2020 at 21:33):

The API certainly don't assume fin n is used.

#### Yakov Pechersky (Aug 13 2020 at 21:36):

matrix/notation does.

#### Patrick Massot (Aug 13 2020 at 21:37):

Do you mean the notation to enter explicit matrices?

#### Patrick Massot (Aug 13 2020 at 21:38):

That's too concrete for me...

#### Alex J. Best (Aug 13 2020 at 21:43):

Do you have maps from zmod n \to zmod (n + 1) (like cast_succ, succ_above, pred_above)? I'm sure you could define them but I doubt they exist as they seem much more natural for fin, of course one could argue that this is just an API issue but: having maps between zmod n and zmod m that aren't group morphisms seems odd.

#### Reid Barton (Aug 13 2020 at 21:44):

I don't see how using zmod could be preferable (unless in a situation where indexing by zmod makes sense for some mathematical reason)

#### Yakov Pechersky (Aug 13 2020 at 21:45):

If people want to formalize more CS, then expressing a matrix with directly indexable types that have the equivalent of pred and succ is very useful for proofs of dynamic programming, for example.

#### Yakov Pechersky (Aug 13 2020 at 21:45):

So it's a preference to making fin have a more filled out API than switching to zmod, in general?

#### Kevin Buzzard (Aug 13 2020 at 23:25):

It seems to me that you are in a worse state, not a better one, if you want to compute the minors of an n+1 x n+1 matrix and you are using zmod. The key thing you need here is the map $\delta^{n+1,i}$ from fin n to fin (n+1) which omits i, and that is surely something which fin n should have. These maps are important for simplicial homology and simplicial sets and simplicial everything.

#### Yakov Pechersky (Aug 13 2020 at 23:27):

Yes, that is fin.succ_above.

#### Kevin Buzzard (Aug 13 2020 at 23:29):

Then given that this exists for fin n but surely doesn't exist for zmod, surely using fin n is better?

Last updated: May 13 2021 at 23:16 UTC