A bunch of Lean files

Stream: maths

[Neil Strickland]

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]

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]

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]

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]

@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]

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]

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]

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]

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

[Scott Morrison]

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]

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.