mathlib4

mathlib4 copied to clipboard

Adds a widget which displays certain kinds of goals in the language of category theory as commutative diagrams. Currently only squares and triangles are supported, but it should be easy to extend this to arbitrary other kinds of diagrams.

There are lots of questions to figure out. About widgets in general:

• Should we put the JS code in widget/ or elsewhere?
• Server support code in Mathlib/Tactic/Widget or elsewhere?
• Currently to build the UI we need to run lake build widgetCommDiag manually. Should this be a dependency of the default target? It would mean that to build mathlib you now need to have Node.js installed, do we really want that? Perhaps we should distribute widgets in compiled form instead? Use an optional dependency? Maybe Lake's cloud features can support that.

About this one:

• When should it be displayed? Currently you need to write a squares! tactic invocation in your script. Should we just default to always showing it? Maybe a custom algebra tactic mode that always shows it? An annotation on the by keyword?
• Currently to add a new kind of diagram we need to write a Penrose substance program describing the diagram, a server support method to collect its objects/cells, and a bit of React to connect them. I think we could automate the React part, then it'd just be Penrose + Lean. Is that desirable?

I would like to join the team to work on this particular widget. How do I begin to build and include this code?

@enjoysmath, you should be able to checkout this pull request locally. Could you describe where you got up to? It may be better to do this over on leanprover.zulipchat.com, in the mathlib4 stream.

I got this running on my machine, and it looks really cool! Is there any way I could help? I was thinking about how the diagrams could be generalized (to not only triangles/squares). For example, would it be better to:

1. encourage (inside Penrose) the diagrams to layout themselves in a grid and ensure that arrows are either horizontal, vertical, or diagonal.
2. Generate the layout in Lean/React by appending appropriate positioning predicates (IsLeftHorizontal, IsUpVetical, etc.) at runtime.

I think the first option might be more straightforward but not as performant since there would be additional strain on Penrose's constraint solver. What are your thoughts on this?

@jul1u5 thanks for your interest! For generalizing to different kinds of diagrams, there are at least two mostly unrelated tasks.

• One is just about the widget implementation. There is a hardcoded list of 'square' | 'triangle'. I have been meaning to make this more easily extensible from the Lean side (see PR description), so I will make that change soon.
• Two is about how to describe arbitrary diagrams to Penrose. I initially experimented with something like your approach 1 and described the experience here. Since optimization in that case takes quite a while and even if that weren't an issue, the diagrams sometimes come out looking a bit slanted/weird, I concluded that it is easier to state rigid constraints in the Style program. These are the IsLeftHorizontal et al which implicitly generate a grid of the objects. Nevertheless if you are keen to explore this further, I don't want to discourage you! I found the Penrose IDE to be helpful for quick prototyping.
  • Even if we keep the Penrose Style/DSL somewhat optimization-free, there is still a choice between the current approach of simply hardcoding descriptions of each interesting index category/(co)limit and the alternative of autogenerating Substance programs (which I understand is your option 2). I went with the former because after all, in practice people only draw a small, finite subclass of all possible diagrams, and describing them in the DSL is not difficult (although we are currently missing arrow styles such as tails for monos/epis/embeddings). But if you want to try autogeneration, it would be cool if something could be made to work! I must admit I don't have a good idea of how one might do this. You'd probably need code for some of the soft heuristics such as "limit/colimit apexes on top-left/bottom-right, respectively" that people tend to use on paper.