Zulip Chat Archive

Stream: general

Topic: subdirs

Yury G. Kudryashov (Aug 10 2019 at 16:16):

Hi, do we have a description of the directory structure? In particular, where is the line between algebra/group* and group_theory/*?

Kevin Buzzard (Aug 10 2019 at 16:22):

They grew organically. I suspect people might be open to suggested rearrangements

Kevin Buzzard (Aug 10 2019 at 16:22):

Things are certainly occasionally rearranged

Floris van Doorn (Aug 10 2019 at 17:37):

Most things in algebra/group/ are lemmas about equational reasoning between elements in a group.
Everything else is in group_theory/, like subgroups, quotient groups and anything more advanced.

I don't know the libraries that well, so this is probably not completely right, but it is a good heuristic.

Scott Morrison (Aug 11 2019 at 00:20):

I feel like this distinction is also pretty close to the dividing line between when it makes sense to unbundle and use typeclasses (equational reasoning about elements), and when it makes sense to bundle (and use category theory...) (when you're interesting in relationships between the containers).

Last updated: Aug 03 2023 at 10:10 UTC