## Stream: maths

### Topic: Mazur-Ulam in affine spaces

#### Yury G. Kudryashov (Jun 01 2020 at 15:11):

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 (Jun 01 2020 at 15:33):

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