Zulip Chat Archive

Stream: maths

Topic: convexity


Yury G. Kudryashov (Aug 21 2020 at 22:16):

There are two natural structures that make it possible to speak about convex combinations (hence, convexity, convex functions etc): [semimodule nnreal E] and [vector_space real E] [add_torsor E P].

Yury G. Kudryashov (Aug 21 2020 at 22:18):

Unfortunately, in the most common case [vector_space real E] these two approaches result in non-defeq definitions.

Yury G. Kudryashov (Aug 21 2020 at 22:21):

For a [semimodule nnreal E] we can talk about a • x + (1 - a) • y and for an affine_space we can talk about a • (y -ᵥ x) +ᵥ x.

Yury G. Kudryashov (Aug 21 2020 at 22:25):

So, we either need some clever trick (I failed to come up with one) or stick to one of the approaches. @Patrick Massot @Sebastien Gouezel @Frédéric Dupuis What do think?

Reid Barton (Aug 21 2020 at 22:32):

There's also a separate algebraic structure of convex space which is a place where you can form convex combinations, and which you can obtain from either of these I guess. (Its free algebra on n+1 generators is the n-simplex.)

Adam Topaz (Aug 21 2020 at 22:40):

This abstract version has some examples which don't really come from geometry, like the quotient [0,1][0,1] (as a convex set) by the equivalence relation rrr \sim r' iff r,r[0,1)r,r' \in [0,1).

Kevin Buzzard (Aug 21 2020 at 22:44):

(or r=r'=1 :p)

Adam Topaz (Aug 21 2020 at 22:44):

well yeah :)

Patrick Massot (Aug 22 2020 at 00:04):

I would prioritize the affine space case which seems much more common.

Frédéric Dupuis (Aug 22 2020 at 00:08):

Is there no way to define some sort of "pre-add_torsor" typeclass that wouldn't require an additive group but only a monoid? Even if it's only used for this, it might be worth it if it's possible.

Yury G. Kudryashov (Aug 22 2020 at 02:01):

Reid Barton said:

There's also a separate algebraic structure of convex space which is a place where you can form convex combinations, and which you can obtain from either of these I guess. (Its free algebra on n+1 generators is the n-simplex.)

If we go this way, then a vector_space real E will have two non-defeq instances.

Yury G. Kudryashov (Aug 22 2020 at 02:04):

@Frédéric Dupuis Do you have some definition?

Adam Topaz (Aug 22 2020 at 02:10):

FWIW, I do think that these abstract convex gadgets deserve some attention. They're (positive) Archimedean analogues of Zp\mathbb{Z}_p modules, and the silly example I mentioned above is a "torsion" module, in some sense. The "usual" convex spaces, defined as subsets of real vector spaces, are analogous to lattices in Qp\mathbb{Q}_p-vector spaces.

Yury G. Kudryashov (Aug 22 2020 at 04:11):

We can add a typeclass convex_space but then we'll have a diamond vector_space ℝ E → add_torsor E E → convex_space E vs vector_space ℝ E → semimodule ℝ≥0 E → convex_space E, and the resulting "convex combination" instances are not defeq.

Adam Topaz (Aug 22 2020 at 14:32):

The second path vector_space ℝ E → semimodule ℝ≥0 E → convex_space E is essentially a restriction of scalars. Would it make sense to define something analogous to scalar_tower @Kenny Lau ?

Kenny Lau (Aug 22 2020 at 14:33):

I don't know

Frédéric Dupuis (Aug 22 2020 at 14:56):

@Yury G. Kudryashov No, I don't have a specific definition, it was probably just wishful thinking.

Kenny Lau (Aug 22 2020 at 15:03):

what's the definition of convex_space?

Adam Topaz (Aug 22 2020 at 15:05):

https://ncatlab.org/nlab/show/convex+space


Last updated: Dec 20 2023 at 11:08 UTC