Affine space

In this file we introduce the following notation:

• AffineSpace V P is an alternative notation for AddTorsor V P introduced at the end of this file.

We tried to use an abbreviation instead of a notation but this led to hard-to-debug elaboration errors. So, we introduce a localized notation instead. When this notation is enabled with open Affine, Lean will use AffineSpace instead of AddTorsor both in input and in the proof state.

Here is an incomplete list of notions related to affine spaces, all of them are defined in other files:

• AffineMap: a map between affine spaces that preserves the affine structure;
• AffineEquiv: an equivalence between affine spaces that preserves the affine structure;
• AffineSubspace: a subset of an affine space closed w.r.t. affine combinations of points;
• AffineCombination: an affine combination of points;
• AffineIndependent: affine independent set of points;
• AffineBasis.coord: the barycentric coordinate of a point.

TODO

Some key definitions are not yet present.

• Affine frames. An affine frame might perhaps be represented as an AffineEquiv to a Finsupp (in the general case) or function type (in the finite-dimensional case) that gives the coordinates, with appropriate proofs of existence when k is a field.

def Affine.termAffineSpace : Lean.ParserDescr

An AddTorsor G P gives a structure to the nonempty type P, acted on by an AddGroup G with a transitive and free action given by the +ᵥ operation and a corresponding subtraction given by the -ᵥ operation. In the case of a vector space, it is an affine space.

Equations

• Affine.termAffineSpace = Lean.ParserDescr.node `Affine.termAffineSpace 1024 (Lean.ParserDescr.symbol "AffineSpace")