tree of algebraic typeclass hierarchy

Stream: mathlib4

[Kenny Lau]

Has anyone made a tree of algebraic typeclass hierarchy? like field -> commring -> ring -> semiring, might also be helpful to include the ones with topology

[Kevin Buzzard]

Screenshot from 2025-11-03 13-15-31.png

is from https://arxiv.org/abs/1910.09336

[Kevin Buzzard]

(but I have no idea how it was made)

[Floris van Doorn]

I've also seen automatically generated new ones, but if you want all classes, it gets really big.

[Floris van Doorn]

Kevin Buzzard said:

(but I have no idea how it was made)

Some metaprogramming to get the data and a lot of manual tweaking to make the positioning somewhat nice.

[Floris van Doorn]

Here are some slightly newer ones, with code that (after updating it to the latest version) should also allow you to generate it yourself on the current Mathlib: #mathlib4 > instance graphs