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

https://gist.githubusercontent.com/eric-wieser/479c49a306430d9d8a896f105ef32178/raw/32f67356bac21dda2c9a80a99d6cef602b643d96/out-large.svg

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 R,\overline{\R}, 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