Zulip Chat Archive

Stream: general

Topic: geometry docs

Patrick Massot (Aug 05 2020 at 10:30):

@Joseph Myers would you be interested in writing a page like this or this about your work on geometry? You only need to create a markdown in this folder and add an entry to this file (I can easily do the later if the format is obscure).

Joseph Myers (Aug 05 2020 at 23:40):

It seems quite hard to get to those pages starting from the leanprover-community home page (as far as I can see, that linear algebra page is only accessible from the overview, not directly from the API documentation for linear algebra, for example).

I can see the use of such pages in cases such as sets.html where they're describing a collection of related concepts from different parts of mathlib. I don't think my work on geometry is really spread out in a way that needs such a page yet, as opposed to expanding the module doc strings for linear_algebra.affine_space and geometry.euclidean to discuss more about the current contents.

I do wonder if I should be splitting up linear_algebra/affine_space.lean into smaller files, given it's now the 12th largest .lean file in mathlib (and there are still lots of mathematically obvious facts about affine spaces not yet included), but even if split up I think module doc strings should be able to give a sufficient overview of the API at present.

Patrick Massot (Aug 07 2020 at 09:08):

I agree that the most important step would be to improve module docstrings, especially listing what's in there instead of simply saying that there isn't much. And splitting affine_space.lean could be useful as well.

Patrick Massot (Aug 07 2020 at 09:52):

@Joseph Myers another geometry question: the affine space file never mention convex or convex_hull, do you intend to connect things soon here? I guess you'll want to redo most of our convex/basic.lean in the case of affine spaces.

Joseph Myers (Aug 07 2020 at 10:04):

@Yury G. Kudryashov was working on porting convexity to affine spaces, see branch convex-affine (and issue #2910).

Patrick Massot (Aug 07 2020 at 10:15):

Thanks. The history of this branch is hard to read because of master merges, so I'll wait for Yury to describe its status.

Joseph Myers (Aug 07 2020 at 10:50):

#3719 expands the module doc string for affine spaces.

Yury G. Kudryashov (Aug 07 2020 at 12:28):

The main problem with porting convexity to affine_spaces is that without making V an out_param in affine_space k V P we have to define convex V s instead of convex s.

Patrick Massot (Aug 07 2020 at 12:28):

@Yury G. Kudryashov am I right to think that, in order to resume work on porting convexity to affine spaces, we can simply copy convex/basic.lean from the branch to a up to date mathlib?

Patrick Massot (Aug 07 2020 at 12:29):


Patrick Massot (Aug 07 2020 at 12:29):

That's bad indeed.

Patrick Massot (Aug 07 2020 at 12:29):

I saw that even segments on the branch have an explicit type in the notation.

Yury G. Kudryashov (Aug 07 2020 at 12:31):

I tried to make V an out_param but failed, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/out_param.20.26.20add_torsor

Patrick Massot (Aug 07 2020 at 12:32):

This reminds me of when I tried to define affine spaces three years ago.

Patrick Massot (Aug 07 2020 at 12:33):

Joseph avoided all these random failures by putting explicit arguments all over the place, but it's not very satisfying.

Yury G. Kudryashov (Aug 07 2020 at 12:33):

I can quickly port convexity adding explicit arguments but I don't think that you'll like the result.

Patrick Massot (Aug 07 2020 at 12:40):

I think this is a rather serious issue. It's not blocking me because all the convexity part of my project happen in vector spaces (they are tangent spaces), but it's very bad for formalization in general if Lean doesn't allow to do this nicely.

Yury G. Kudryashov (Aug 07 2020 at 12:43):

Unfortunately, I don't understand why it fails and make an #mwe to test with Lean 4.

Patrick Massot (Aug 07 2020 at 12:48):

It would be nice to get input from people who really understand all the subtlety of elaboration here.

Yury G. Kudryashov (Aug 07 2020 at 13:00):

I tried asking Gabriel. Who else should I ask?

Patrick Massot (Aug 07 2020 at 13:20):

Mario, Rob, Floris? Or even Sebastian if you can minimize enough.

Mario Carneiro (Aug 07 2020 at 13:34):

an MWE would help

Joseph Myers (Aug 07 2020 at 17:18):

It would be nice for k as well as V to be implicit everywhere using affine spaces. (That's not such an issue for convexity because that's hardcoding ℝ everywhere.) If anyone ever wants to reinterpret a complex affine space as a real one, using copies of the types should suffice; I certainly think the normal case is that k and V are both implied by P.

Yury G. Kudryashov (Aug 07 2020 at 21:14):

We don't do this for vector spaces, so I'd prefer to avoid this for affine spaces as well.

Mario Carneiro (Aug 07 2020 at 21:15):

we originally had vector spaces set up like this, and rolled it back after it came to light that it's actually not uncommon to have the one vector space over two different fields

Joseph Myers (Aug 08 2020 at 14:56):

#3726 splits up affine_space.lean, so reducing it from 10th largest .lean file in mathlib to 41st largest.

Yury G. Kudryashov (Aug 08 2020 at 16:49):

:( I'm removing V arguments from affine_space.lean

Last updated: Aug 03 2023 at 10:10 UTC