Affine Combination Space

Stream: maths

[Aaron Liu]

I had some thoughts while biking today:

Define an affine combination space over a field 𝕜 to be a type P equipped with a partial operation called affine combination with the signature

affineCombination : (d : P →₀ 𝕜) → d.sum (fun _ c => c) = 1 → P

This affineCombination must satisfy a distributive law

∀ (d : { d : P →₀ 𝕜 // c.sum (fun _ c => c) = 1 } →₀ 𝕜) (hd : d.sum (fun _ c => c) = 1),
  affineCombination (d.mapDomain fun v => affineCombination v.1 ⋯) ⋯ =
    affineCombination (d.sum fun v c => c • v.1) ⋯

and a unit law

∀ (p : P), affineCombination (Finsupp.single p 1) ⋯ = p

Assuming I've got those axioms correct, it's not hard to see that the nonempty affine combination spaces over a field 𝕜 are exactly the affine spaces over vector spaces over 𝕜. But I've done this without ever explicitly mentioning the vector space, so we can generalize this in a different direction. Nothing in the definition requires 𝕜 to have division, or even subtraction, so we can consider these over an arbitrary docs#Semiring. Contrast this to docs#AddTorsor which only makes sense over an AddGroup (with subtraction).
The motivation is the figure out a way to generalize docs#segment and friends to affine spaces without losing their use in semirings, which don't have subtraction.
Some other things I've noticed:

• fixing the semiring gives you a finitary algebraic theory, so abstract nonsense gives you all sorts of results
• a convex set is an affine combination space over the nonnegative part of the scalars
• (semi)modules can be given a similar definition, just without the requirement that the scalars add to one (so with linear combination instead of affine combination), but they also have this nicer presentation with the binary operations of addition and scalar multiplication, however this sort of seems difficult to do with affine combination spaces because of the requirement that the scalars add up to one

Overall, does this sound like a good idea? I would like to hear your thoughts and opinions on this. Also surely someone else has thought of this before? But I don't see it in mathlib so...

[Eric Wieser]

This sounds related to @Yaël Dillies' past plans to refactor convexity to affine spaces

[Yaël Dillies]

Indeed, I have an implementation in LeanCamCombi. It's still on the roadmap, but not my priority

[Jovan Gerbscheid]

I quite like this idea.

This means that we can talk about a Euclidean plane without carrying around this awkward real vector space, right? And instead, given such an affine space, there is a way to construct the corresponding vector space (using some choice of an arbitrary base point), right? So to do oriented angles, we would put an orientation on that vector space? And to make sure it is a plane, we require this vector space to be 2 dimensional. (Or we could define rank of such a space to be the rank of its corresponding vector space).

[Jovan Gerbscheid]

Also, I think Finsupp.degree does what you are doing with Finsupp.sum. There was some recent discussion about what Finsupp.degree should be called.

[Jovan Gerbscheid]

Also I think this should be called AffineSpace

[Aaron Liu]

Jovan Gerbscheid said:

Also I think this should be called AffineSpace

the name is arbitrary and can be whatever you want

[Aaron Liu]

Jovan Gerbscheid said:

Also I think this should be called AffineSpace

the problem is that AffineSubspace is already taken

[Jovan Gerbscheid]

My impression is that if we switch to this new definition of AffineSpace for Euclidean geometry, then we also want to switch AffineSubspace to not depend on a vector space.

[Eric Wieser]

We'll still want some class that is the current AffineSpace, to hold the compatibility between vsub and vadd

[Jovan Gerbscheid]

The current thing used for AffineSpace is AddTorsor, which is a more general concept, so that is certainly not getting removed.

[Aaron Liu]

well it's not more general

[Aaron Liu]

it's just general in a different direction

[Aaron Liu]

they are incomparable elements in the type of abstractions partially ordered by generality

[Eric Wieser]

Oh I see, I forgot that AffineSpace doesn't exist and is only notation

[Aaron Liu]

for example, the set Ico (0 : ℝ) 1 is an affine combination space over ℝ≥0 but isn't an AddTorsor in a compatible way, and any nonabelian AddGroup is an AddTorsor over itself without being an affine combination space in a compatible way

[Jovan Gerbscheid]

I was wondering if your definition of AffineSpace could be made without Finsupp, and instead using some version of lineMap as the fundamental operation. But unfortunately it seems like this doesn't work in the generality of a Semiring R.

Either way, AffineMap.lineMap can be defined in terms of affineCombination. And AffineMap can also be generalized to not have the underlying vector space.

[Joseph Myers]

I don't think having a real vector space for geometrical uses is awkward; it's used extremely frequently and is much more convenient to have simply as V than requiring use of some other definition to produce a space of vectors from a space of points (even apart from the extra awkwardness of needing to insert lots of extra maps to deal with the space of vectors of an affine subspace not being a submodule of the space of vectors of the whole space if you involve such extra definitions in producing a space of vectors). And I certainly expect that for people using concrete coordinates, it's much better for EuclideanSpace to be its own space of vectors (generally: for a module used as an affine space to be its own space of vectors) than needing to use separate types.

I'd expect some kind of typeclass for an abstract affine combination space that's also an AddTorsor for a module that asserts that the two ways of calculating affine combinations agree. (Constructing the data for an abstract affine combination space from a torsor is problematic as an instance, at least if you also want an instance to construct the data for a module over a semiring, because of non-defeq diamonds in the case of a module as a torsor for itself.)

[Joseph Myers]

Removing the existing AffineSpace notation for AddTorsor probably makes sense.

[Aaron Liu]

What about when there are no vectors?

[Joseph Myers]

That's a case when you can use only the typeclass for an affine combination space and not the AddTorsor class or the class saying they agree. (Which isn't relevant for doing Euclidean geometry - in the Euclidean case you can freely use all three classes, because using only a subset of them adds no mathematical generality.)

[Jovan Gerbscheid]

In this new design, to have access to a real vector space at any time, I propose defining a single field structure AffineVectorSpace P (or some other name), which has these instances

instance [AffineSpace R A] : VectorSpace R (AffineVectorSpace A)

abbrev _ [AffineSpace R A] : AddTorsor (AffineVectorSpace A) A

It's very unfortunate that the AddTorsor cannot be an instance because type class synthesis cannot determine R. So yes, this has the disadvantage or having to add this instance explicitly in the local context.

You suggest that AffineSubspace will be more awkward to deal with. I don't know if it will, but if so, we should simply not modify its definition, and it should still work fine.

Indeed we need a type class stating that some AffineSpace instance is compatible with some AddTorsor instance, I hadn't thought of this before. But I'm not sure which instance diamonds you are talking about.

[Adam Topaz]

There have been various past discussions on this zulip about abstractions of the notion of convexity. Such an algebraic structure should fit into such a formalism.

[Jovan Gerbscheid]

@Aaron Liu do you think a definition like this would make sense? Is Semifield too restrictive?

import Mathlib

class AffineSpace (R A : Type*) [Semifield R] where
  semiLineMap : A → A → (r s : R) → r + s = 1 → A
  semiLineMap_zero_one {a b : A} : semiLineMap a b 0 1 (zero_add 1) = b
  semiLineMap_symm {a b : A} {r s : R} (h : r + s = 1) : semiLineMap a b r s h = semiLineMap b a s r (by rw [add_comm, h])
  semiLineMap_distrib (a b c : A) {r s t : R} (h : r + s + t = 1) (hr : r ≠ 0) (hs : s ≠ 0) (ht : t ≠ 0) (hrt : r + t ≠ 0) (hst : s + t ≠ 0) :
    semiLineMap a (semiLineMap b c (s / (s + t)) (t / (s + t)) (by field_simp)) r (s + t) (by rw [← add_assoc, h]) =
    semiLineMap b (semiLineMap a c (r / (r + t)) (t / (r + t)) (by field_simp)) s (r + t) (by rw [← add_assoc, add_comm s, h])

We could also implicitly divide by r + s, so that we only need to require a proof that r + s is nonzero, and then we also don't use division in the definition, which may help to loosed the Semifield. Or we could even have junk values and not take any proof.

[Aaron Liu]

It's less general I guess

[Aaron Liu]

but it's not like I have any concrete use cases in mind

[Aaron Liu]

I don't think ENNReal is a semifield

[Jovan Gerbscheid]

But surely instead of ENNReal, you'd just use NNReal?

[Aaron Liu]

maybe

[Joseph Myers]

Anything using AffineVectorSpace seems strictly worse for all existing affine and Euclidean geometry uses compared to having independently determined V (note that the group is an outParam for an AddTorsor, meaning that (a) it's implicit in most contexts and (b) there are problems if there are ever two different groups with AddTorsor instances for the same space of points).

Given s : AffineSubspace R P, s.direction is a Submodule R V, which is clearly desirable so that all the extensive theory of submodules can be applied readily when working with affine subspaces. And there is the obvious instance AddTorsor s.direction s which is also clearly desirable. But AffineVectorSpace s is not the same as s.direction (coerced to a Sort) and in particular is not a submodule of AffineVectorSpace P.

The diamond for affine combinations is: affine combinations for AddTorsor for a module should be defined something like they are at present, while affine combinations for a module (possibly over a semiring, so no subtraction, so no torsor) look something like docs#Finsupp.linearCombination but it's unlikely these could be made defeq in the case of a module as a torsor over itself, so at least one of these constructions of an affine combination space should not be an instance.

[Aaron Liu]

I don't like AffineVectorSpace anymore

[Eric Wieser]

Aaron Liu said:

but it's not like I have any concrete use cases in mind

Not that concrete, but instantiating with R = Int seems vaguely useful

[Eric Wieser]

Is the AffineVectorSpace you now dislike different from Jovan's AffineSpace above?

[Jovan Gerbscheid]

Jovan Gerbscheid said:

instance [AffineSpace R A] : VectorSpace R (AffineVectorSpace A)

abbrev _ [AffineSpace R A] : AddTorsor (AffineVectorSpace A) A

I think @Aaron Liu is referring to the vector space that we would construct from a given AffineSpace (I couldn't come up with a better name)

[Aaron Liu]

#31984

[Jovan Gerbscheid]

The difference seems to be that in that PR, defining the ConvexSpace, they only allow the weights to be non-negative. So it wouldn't work as an affine combination space we were discussing here.

[Aaron Liu]

yes that's correct

[Aaron Liu]

Maybe I should make a PR generalizing it

[Anatole Dedecker]

I think it should get a different name, but the model should be the same

[Jovan Gerbscheid]

Aaron Liu said:

Maybe I should make a PR generalizing it

How would you do this? I don't think it is straightforward to do so without making it more awkward to use in the convex case.

[Aaron Liu]

I think it should be similar to Ideal and Submodule, where we define all these things for Submodule and then Ideal R is just Submodule R R and we define things for Ideal too

[Joseph Myers]

I'd expect an affine combination space (no restrictions on the signs of weights in combinations) to be fine for convexity in most cases - you simply just use combinations where all weights are nonnegative even if the underlying semiring also includes negative values. The main issue would be that you couldn't then use spans for convex hulls if the semiring includes negative values.

Note incidentally that there's a design question of how spans / convex hulls / subspaces work over the trivial ring in affine combination spaces / convex combination spaces. AffineSubspace for torsors always has ⊥ empty as the closure property is always true for an empty carrier set. But if your closure property is for n-way combinations then the empty combination is a thing when 0=1.

[Aaron Liu]

Joseph Myers said:

Note incidentally that there's a design question of how spans / convex hulls / subspaces work over the trivial ring in affine combination spaces / convex combination spaces. AffineSubspace for torsors always has ⊥ empty as the closure property is always true for an empty carrier set. But if your closure property is for n-way combinations then the empty combination is a thing when 0=1.

Unfolding all the definitions, we get that any affine combination space over the trivial ring is a single point which is equal to the empty combination.

[Aaron Liu]

Joseph Myers said:

I'd expect an affine combination space (no restrictions on the signs of weights in combinations) to be fine for convexity in most cases - you simply just use combinations where all weights are nonnegative even if the underlying semiring also includes negative values. The main issue would be that you couldn't then use spans for convex hulls if the semiring includes negative values.

I'm saying just take the combination over the nonnegative part of your ring, and then you'll only be able to use nonnegative weights