Zulip Chat Archive
Stream: LftCM22
Topic: algebraic hierarchy
Johan Commelin (Jul 13 2022 at 19:03):
In a moment I will talk about the "algebraic hierarchy".
Here is a graphical hyperlinked depiction of the instance graph of algebraic structures in mathlib.
instance_graph.svg
Major thanks to @Eric Wieser for generating this on short notice!
Katja Berčič (Jul 13 2022 at 20:04):
On the Zoom, I mentioned that Michael Kohlhase's group has a theory graph viewer that might be useful to the Lean community. Here's a link to the repository: https://github.com/UniFormal/TGView
Eric Wieser (Jul 14 2022 at 13:03):
For anyone interesting in generating better graphs, that was generated with graphviz and the lean code here:
https://gist.github.com/eric-wieser/479c49a306430d9d8a896f105ef32178
It's not a complete export as I only used everything under file#analysis/normed_space/banach to keep it fast, but you could easily regenerate it for all of mathlib using leanproject mk-all.
Eric Wieser (Jul 14 2022 at 17:01):
I went ahead and updated the above with a mk-all version. The monster graph is
Yakov Pechersky (Jul 14 2022 at 17:17):
The king! image.png
Johan Commelin (Jul 14 2022 at 18:21):
@Eric Wieser Thank you so much for doing this!
Kevin Buzzard (Jul 14 2022 at 19:21):
That typeclass is not my favourite typeclass. [PS sorry.]
Kevin Buzzard (Jul 14 2022 at 19:21):
It shouldn't be at the top
Kevin Buzzard (Jul 14 2022 at 19:22):
There are diamond problems with which has two canonical is_R_or_C structures
Patrick Massot (Jul 14 2022 at 19:29):
Kevin, you shouldn't say that. This type class nicely solves a lot of issues.
Heather Macbeth (Jul 14 2022 at 19:45):
To link to a previous discussion of whether is_R_or_C should even exist, a guess would be that is_R_or_C could be replaced by "simultaneously a a finite-dimensional extension field of ℝ and a star_ring, with the star fixing only ℝ". But I am not even confident that that statement encodes all the needed properties.
Kevin Buzzard (Jul 14 2022 at 19:50):
Of course I'm not serious about is_R_or_C but at some level the typeclass troubles me. Brian Conrad wrote an entire book explaining why if you're doing some kinds of mathematics then you never have to choose a preferred square root of -1. This has led me to believe that you should always think twice before doing so.
Heather Macbeth (Jul 14 2022 at 19:52):
Kevin, my abstract definition doesn't involve a choice of square root of -1 ... I just haven't thought about whether it would truly work in all the use cases.
Eric Wieser (Jul 14 2022 at 19:55):
I think my biggest qualm with is_R_or_C is that it's too appealing a tool to reach for when you might not actually need something that strong. Of course, the reason it's so appealing a tool to reach for is precisely because it solves lots of issues!
Kevin Buzzard (Jul 14 2022 at 20:03):
I think basically I've never thought hard about situations where it's really important to pick an orientation, and I've thought very hard about situations where it's actively a bad idea.
Last updated: Dec 20 2023 at 11:08 UTC