geometry docs

Stream: general

[Patrick Massot]

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

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]

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]

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

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

[Patrick Massot]

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]

#3719 expands the module doc string for affine spaces.

[Yury G. Kudryashov]

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]

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

Ah.

[Patrick Massot]

That's bad indeed.

[Patrick Massot]

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

[Yury G. Kudryashov]

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]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

I tried asking Gabriel. Who else should I ask?

[Patrick Massot]

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

[Mario Carneiro]

an MWE would help

[Joseph Myers]

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]

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

[Mario Carneiro]

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]

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

[Yury G. Kudryashov]

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