Preferring zmod over fin

Stream: new members

[Yakov Pechersky]

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]

but the matrix API doesn't support zmod right

[Patrick Massot]

What part of the API?

[Patrick Massot]

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

[Yakov Pechersky]

matrix/notation does.

[Patrick Massot]

Do you mean the notation to enter explicit matrices?

[Patrick Massot]

That's too concrete for me...

[Alex J. Best]

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]

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]

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]

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

[Kevin Buzzard]

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]

Yes, that is fin.succ_above.

[Kevin Buzzard]

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