Convex join

Stream: maths

[Yaël Dillies]

Has anybody heard of the convex join? I wrote this code a year ago and it's very useful to deal with convex hulls of unions (mostly for finite sets).

import analysis.convex.basic

variables (𝕜 : Type*) {E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]

/-- The join of two sets is the union of the segments joining them. This can be interpreted as the
topological join, but within the original space. -/
def convex_join (s t : set E) : set E := ⋃ (x ∈ s) (y ∈ t), segment 𝕜 x y

I can't remember whether I made up the name or even the object or not. Looking up "convex join" yields this maths stack exchange question and the topological join, which both look very close to what I have above.

[Yaël Dillies]

I will PR it anyway because I need it for Stone's separation theorem, but it would be good to get the terminology right, if there is one.

[Violeta Hernández]

I recall hearing that you could provide a very general axiomatization of convex geometry by just using the convex join, and I believe it referred to this same operation

[Violeta Hernández]

I'm like 95% sure

[Damiano Testa]

In algebraic geometry, the join of two subsets usually denotes the union of all the lines intersecting both sets. In that context, the "sets" usually have some further properties (irreducible, closed,...). There are also some other small subtleties, but the concept is very similar.

[Yaël Dillies]

Here's more of the code if you want to have a look: branch#stone_separation

[Yaël Dillies]

I find it actually hard to work with finite combinations, so if anyone manages to fill the the two sorry in, I would be glad!

[Michelle Olson]

I am very interested in the topic (especially convex geometry) but I just started learning lean so I don't know how quickly I could be of use!

[Yaël Dillies]

@Michelle Olson, just fyi we now have docs#convex_join and docs#exists_convex_convex_compl_subset in mathlib. You're very welcome to contribute other topics!

[Michelle Olson]

thank you for letting me know!