Zulip Chat Archive
Stream: maths
Topic: MazurUlam in affine spaces
Yury G. Kudryashov (Jun 01 2020 at 15:11):
Patrick Massot said:
Yury G. Kudryashov do you want to return to MazurUlam now that we have affine spaces? It would be a nice test of the affine API.
I tried to port MazurUlam to affine spaces, and I have a few difficulties:
 Currently
midpoint
is defined for a semimodule over a semiring with invertible2
. Is there any reasonable way to redefine it in anadd_torsor
without loosing the case of a convex cone (a semimodule overnnreal
)? 
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₁
usingadd_torsor.nonempty V₁
;  prove that
λ y : V₁, f (y +ᵥ x) ᵥ f x
is a linear map.
While I would prefer to have a selfcontained definition of an affine map with only one data fieldto_fun
, at least we need an alternative constructor.
 choose a point

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.
Yury G. Kudryashov (Jun 01 2020 at 18:15):
I added a few issues about affine spaces: #2908 #2909 #2910
Yury G. Kudryashov (Jun 01 2020 at 18:19):
@Joseph Myers :up:
Last updated: May 06 2021 at 17:38 UTC