Affine spaces

Stream: general

[Kevin Sullivan]

My students and I are developing an affine space library, and an affine coordinate space library based on it. We formalize an affine space as a torsor over a vector space. The formalizations are fully general, e.g., arbitrary field, etc. Our use case is to help in formalizing aspects of classical physics and dynamics.

My question is, what is the current state of development of affine spaces (along with frames, transformations, geometry, etc) in Lean, beyond the work we've been doing? Also, what would be the best way to share our work with the community?

[Patrick Massot]

You can go to https://leanprover-community.github.io/mathlib_docs/ and type affine in the search bar

[Patrick Massot]

Or else use the folder list on the left to browse to `linear_algebra/affine_space and geometry/euclidean.

[Rob Lewis]

As for sharing the code: I've been working on and off on infrastructure for user-contributed libraries. You could add your project to the list here, ideally after setting up CI as described here. (The branch update is important for the contrib tool.) Sooner or later, checked in projects will be displayed somewhere on the community site.

[Joseph Myers]

Although we don't have affine frames yet, the module doc string for linear_algebra/affine_space/basic has a suggestion for how they might be represented in Lean (as an affine_equiv between an affine space and the space of its coordinates; we don't have affine_equiv yet either). Affine spaces are defined in mathlib over arbitrary modules, not just vector spaces (most results so far don't require a field).

[Kevin Sullivan]

Joseph Myers said:

Although we don't have affine frames yet, the module doc string for linear_algebra/affine_space/basic has a suggestion for how they might be represented in Lean (as an affine_equiv between an affine space and the space of its coordinates; we don't have affine_equiv yet either). Affine spaces are defined in mathlib over arbitrary modules, not just vector spaces (most results so far don't require a field).

Thank you. We've implemented affine coordinate spaces as a special case of affine spaces and affine frames as defining isomorphisms between affine coordinate spaces. We're not quite sure yet how to handle equality of points and vectors when represented as different coordinate tuples. We'll study what you've produced and will see if we can integrate what you and what we are doing. We appreciate your work! Thank you, again.