Zulip Chat Archive
Stream: condensed mathematics
Topic: short exact sequences
Johan Commelin (Sep 29 2021 at 12:24):
Currently, the type of short exact sequences in a category C is called short_exact_sequence C.
My intention is that this moves to mathlib at some point.
Would it be "ok" to call this type SES C instead?
Johan Commelin (Sep 29 2021 at 12:24):
I think the brevity is worth the obscurity...
Riccardo Brasca (Sep 29 2021 at 12:29):
I agree that SES C is a nice abbreviation. And we definitely want short exact sequences in mathlib!
Yaël Dillies (Sep 29 2021 at 12:53):
What about short_ex_seq?
Filippo A. E. Nuccio (Sep 29 2021 at 12:53):
I think that SES is more familiar to mathematicians' ears.
Alex J. Best (Sep 29 2021 at 12:54):
SES is a pretty common abbreviation yeah
Yaël Dillies (Sep 29 2021 at 12:54):
Maybe? But it can probably stand for other things
Eric Rodriguez (Sep 29 2021 at 13:25):
what about abbreviation SES := short_exact_sequence?
Johan Commelin (Sep 29 2021 at 14:18):
the question is more what substring we use in other defs. Is it going to be mk_SES_of_foo or mk_short_ex_seq_of_foo, etc...
Adam Topaz (Sep 29 2021 at 14:19):
+1 for SES from me
Last updated: Dec 20 2023 at 11:08 UTC