Zulip Chat Archive

Stream: new members

Topic: Preferring zmod over fin


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

view this post on Zulip Kenny Lau (Aug 13 2020 at 21:31):

but the matrix API doesn't support zmod right

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:33):

What part of the API?

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:33):

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

view this post on Zulip Yakov Pechersky (Aug 13 2020 at 21:36):

matrix/notation does.

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:37):

Do you mean the notation to enter explicit matrices?

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:38):

That's too concrete for me...

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

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

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

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

view this post on Zulip 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 δn+1,i\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.

view this post on Zulip Yakov Pechersky (Aug 13 2020 at 23:27):

Yes, that is fin.succ_above.

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