Zulip Chat Archive

Stream: maths

Topic: A bunch of Lean files


Neil Strickland (Apr 14 2019 at 20:08):

I have put almost all of my Lean files at https://github.com/NeilStrickland/lean_lib/tree/master. There are about 19000 lines by the crudest metric, although I am sure that someone more skilful could achieve the same results with much less space. There is a README outlining what is there, and many files have substantial header comments. I would be interested in moving some of it to mathlib, although that will probably take a large amount of work with refactoring, complying with coding conventions and so on. I would be interested in comments and suggestions.

Kevin Buzzard (Apr 14 2019 at 20:58):

Which of the homotopy stuff do you think is appropriate for mathlib? Do you know about what Reid Barton has been doing with homotopy theory? (I don't but there's a repo somewhere)

Neil Strickland (Apr 14 2019 at 21:07):

The file itloc.lean is rather specialised, but poset.lean, subdiv.lean and upper.lean could certainly move into mathlib, possibly after some reorganisation. I don't think that anything I have done or am thinking of doing actually overlaps with what Reid has done, although it would be sensible to ensure that there is a smooth interface between them.

Kevin Buzzard (Apr 14 2019 at 21:42):

rw[mul_assoc (r0 ^ i) r0 s0,mul_assoc (r0 ^ i)] -- I think mathlib convention is a space between rw and [, and also space after the comma.

Scott Morrison (Apr 14 2019 at 22:57):

@Neil Strickland, you should definitely start PRing stuff, so that others can use it, it doesn't get lost, and it can all be polished up!

Scott Morrison (Apr 14 2019 at 22:59):

Regardling poset.lean: you should look at category_theory/concrete_category.lean, or some of the examples in the category_theory/instances/ directory, where you'll see an existing general framework for this kind of thing, which should save some repetition. By the time you're define comp, comp_id, id_comp, and assoc, you really should provide the category instance. (After which, as I keep telling Kevin, you get a lot of things for free :-)

Scott Morrison (Apr 14 2019 at 23:01):

There's tonnes of things in there that can be stand alone PRs. (e.g.) I think it's best to make "minimal" PRs, as big ones tend to get stuck in the throat of the reviewing process, unless they are done really well. :-)

Neil Strickland (Apr 15 2019 at 00:11):

Do you have examples yet of categories that are self-enriched? I really need to use the fact that poset.hom P Q has a poset structure such that composition and (co)evaluation are poset morphisms. I don't know if that will cause any problems with your general framework.

Scott Morrison (Apr 15 2019 at 02:10):

No, we haven't done (self-) enrichment yet. It really needs to happen.

Scott Morrison (Apr 15 2019 at 02:12):

I waited a long time on doing this because I wanted to do something overly general. :-) I've seen the error of my ways.

Scott Morrison (Apr 15 2019 at 02:13):

The long-standing issue of how to handle products in categories (are they just special cases of limits, or do you provide a separate API for them?) has also been a hold up on this.


Last updated: Dec 20 2023 at 11:08 UTC