Mazur-Ulam in affine spaces

Stream: maths

[Yury G. Kudryashov]

Patrick Massot said:

Yury G. Kudryashov do you want to return to Mazur-Ulam now that we have affine spaces? It would be a nice test of the affine API.

I tried to port Mazur-Ulam to affine spaces, and I have a few difficulties:

1. Currently midpoint is defined for a semimodule over a semiring with invertible 2. Is there any reasonable way to redefine it in an add_torsor without loosing the case of a convex cone (a semimodule over nnreal)?

2. Current API assumes that any affine map comes with a linear map. So, if I have a map f : P₁ → P₂, then in order to convert it into an affine map I have to:

   • choose a point x : P₁ using add_torsor.nonempty V₁;
   • prove that λ y : V₁, f (y +ᵥ x) -ᵥ f x is a linear map.
     While I would prefer to have a self-contained definition of an affine map with only one data field to_fun, at least we need an alternative constructor.

3. There is no affine_equiv.

[Yury G. Kudryashov]

UPD: about 2., may be it's useful to be able to explicitly provide derivative. So we only need an alternative constructor.

[Yury G. Kudryashov]

I added a few issues about affine spaces: #2908 #2909 #2910

[Yury G. Kudryashov]

@Joseph Myers :up: