Zulip Chat Archive

Stream: maths

Topic: Mazur-Ulam in affine spaces


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 18:15):

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

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 18:19):

@Joseph Myers :up:


Last updated: May 06 2021 at 17:38 UTC