Convex space

Stream: maths

[Yaël Dillies]

@Yury G. Kudryashov, at least the prod instances work perfectly!

import algebra.module.pi
import algebra.module.prod
import linear_algebra.affine_space.basic

open_locale affine

variables {𝕜 V V₁ V₂ E E₁ E₂ ι : Type*} {𝕜i Vi Ei : Π i : ι, Type*}

variables (𝕜 E)

class convex_space :=
(segment_map : 𝕜 → 𝕜 → E → E → E)

section prod
variables [convex_space 𝕜 E₁] [convex_space 𝕜 E₂]

instance : convex_space 𝕜 (E₁ × E₂) :=
{ segment_map := λ a b x y, begin
  exact ⟨convex_space.segment_map a b x.1 y.1, convex_space.segment_map a b x.2 y.2⟩,
end }

end prod

section pi
variables [Π i, convex_space (𝕜i i) (Ei i)]

instance : convex_space (Π i : ι, 𝕜i i) (Π i : ι, Ei i) :=
{ segment_map := λ a b x y i, convex_space.segment_map (a i) (b i) (x i) (y i) }

end pi

variables {𝕜 E}

section affine
variables [ring 𝕜] [add_comm_group V] [module 𝕜 V] [affine_space V E]
  [add_comm_group V₁] [module 𝕜 V₁] [affine_space V₁ E₁]
  [add_comm_group V₂] [module 𝕜 V₂] [affine_space V₂ E₂]
  [Π i, ring (𝕜i i)] [Π i, add_comm_group (Vi i)] [Π i, module (𝕜i i) (Vi i)]
  [Π i, affine_space (Vi i) (Ei i)]

section
include V

instance affine_space.to_convex_space : convex_space 𝕜 E :=
{ segment_map := λ a _ x y, a • (y -ᵥ x) +ᵥ x }
end

include V₁ V₂

example : @affine_space.to_convex_space 𝕜 _ _ _ _ _ (@prod.add_torsor V₁ E₁ V₂ E₂ _ _ _ _) =
  @prod.convex_space 𝕜 E₁ E₂ _ _ :=
rfl

example : @affine_space.to_convex_space (Π i, 𝕜i i) (Π i, Vi i) (Π i, Ei i) _ _
  (@pi.module' ι 𝕜i Vi _ _ _) (@pi.add_torsor ι Vi _ Ei _) = @pi.convex_space ι 𝕜i Ei _ :=
sorry --totally unrelated diamond issue?

end affine

section module
variables [semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid E₁] [module 𝕜 E₁]
  [add_comm_monoid E₂] [module 𝕜 E₂]
  [Π i, semiring (𝕜i i)] [Π i, add_comm_monoid (Ei i)] [Π i, module (𝕜i i) (Ei i)]

instance module.to_convex_space : convex_space 𝕜 E :=
{ segment_map := λ a b x y, a • x + b • y }

example : @module.to_convex_space 𝕜 (E₁ × E₂) _ _ (@prod.module 𝕜 E₁ E₂ _ _ _ _ _) = @prod.convex_space 𝕜 E₁ E₂ _ _
  :=
rfl

example : @module.to_convex_space _ _ _ _ (@pi.module' ι 𝕜i Ei _ _ _) = @pi.convex_space ι 𝕜i Ei _
  :=
rfl

end module

[Yaël Dillies]

This pi instance also works for defeqness with module. I didn't manage to try for affine_space because I seem to be getting another completely unrelated diamond...

[Yaël Dillies]

I've updated the snippet above.

[Yaël Dillies]

And here's the dreaded diamond vector space diamond.

example [ring 𝕜] [add_comm_group E] [module 𝕜 E] :
  @affine_space.to_convex_space 𝕜 E E _ _ _ _ = @module.to_convex_space 𝕜 E _ _ _ :=
rfl --fails

It is actually unprovable because I haven't required the two weights to sum up to 1 in segment_map. Should I add it?

[Yury G. Kudryashov]

Even if you add it, we can't make it rfl.

[Yury G. Kudryashov]

And I don't know what to do.

[Yaël Dillies]

Yeah, I know we can't, because it requires using h : a + b = 1 :worried:

[Yaël Dillies]

My point was that at least we could make the instances propeq, because they currently are not (they differ on the junk values of segment_map).

[Reid Barton]

If 𝕜 is a ring there would be no problem, right? You could define segment_map for a module using the same sort of formula as for an affine_space (and then just drop the redundant second argument of segment_map completely)

[Reid Barton]

Do we really need convex spaces over semirings?

[Yaël Dillies]

EDIT: Ah yes, I see what you mean

[Yaël Dillies]

But then there's no point in defining convex spaces anymore.

[Yaël Dillies]

I am working on branch#convex_space

[Reid Barton]

Yaël Dillies said:

But then there's no point in defining convex spaces anymore.

I think I'm missing some context on why you're interested in convex spaces in the first place

[Yaël Dillies]

I'm defining convex spaces to be able to generalize convexity to both affine spaces and modules. The convexity refactor generalized convexity to modules, and now we want it in affine spaces.

[Reid Barton]

Isn't a module an affine space?

[Yaël Dillies]

Not if it isn't over a ring but just a semiring, that's the point.

[Yaël Dillies]

(mathlib's module, mathematicians' semimodule)

[Reid Barton]

Well then that gets back to my original question, why do we care about convexity over semirings

[Reid Barton]

But also, I think there is more than one notion of affine space

[Yaël Dillies]

Oh? Is there one that doesn't intrinsically require substraction?

[Yaël Dillies]

Reid Barton said:

Well then that gets back to my original question, why do we care about convexity over semirings

And, for that, ask @Yakov Pechersky

[Reid Barton]

There is https://ncatlab.org/nlab/show/affine+space#unbiased_definition. Basically it means you have a "linear combination" operation $A^n \to A$ for each $(c_1, \ldots, c_n) \in k^n$ with $c_1 + \cdots + c_n = 1$, and they have to satisfy the equations expected of general linear combinations.

[Reid Barton]

Note that under this definition, the empty set would also be considered an affine space unless you explicitly rule it out

[Yaël Dillies]

Ah well that's what I'm trying to define here :grinning:

[Yaël Dillies]

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

[Kevin Buzzard]

In my mind the whole point of an affine space is that it is a homogeneous object which looks everywhere locally like the thing it's modelled on. Additive groups look the same everywhere locally because left or right addition by a fixed element is a bijection, so affine spaces over additive groups are reasonable objects. The definition does not use negation explicitly but it's using it implicitly to make the definition capture the concept which mathematicians are trying to model. If one defines affine spaces over modules then I could imagine that the naive definition is not the useful one because monoids like {0,2,3,4,5,...} look different near 0 to how they look near 37 so you can't be a homogeneous space (another word for affine space) over this object because the object itself isn't homogeneous.

This reminds me of group actions. The definition of a group action doesn't mention inverses so it can in theory be made for monoids. However if you make it for monoids then there are two possibilities -- a multiplicative map into End(S) or a multiplicative map into Aut(S). For groups these are equivalent but for monoids they are not and so one has to decide which one is the useful one rather than just choosing one randomly because it's just what happens to be what you get if you write down the standard group definition (which doesn't assume actions are invertible because this follows from the group axioms) and then apply it to monoids.

[Reid Barton]

Part of the confusion is that mathlib (and Kevin) uses "affine space" in the sense of a torsor, but in the context of convexity there's another, more obviously relevant notion: something where you can form affine combinations.

[Yaël Dillies]

Yes, totally agreed! All I want is an affine-combinations space.

[Kevin Buzzard]

You can have torsors for an abelian group (and probably even more general objects but my rant above is suggesting that they might not be useful objects for monoids) but for this notion of affine space I guess you need a 1? And presumably for semirings it's the same situation --the definition we normally use happens to make sense but it's not clear (at least to me) that it's the useful one if there's no subtraction

[Kevin Buzzard]

For example any set would be an affine space (in the sense of linear combinations) over the naturals this way, right?

[Reid Barton]

Any torsor for an abelian group is an affine space (in the sense of linear combinations) over $\mathbb{Z}$

[Reid Barton]

Right, affine spaces over $\mathbb{N}$ is just the trivial theory (maybe plus the assumption that it is nonempty)

[Kevin Buzzard]

Is that actually used though?

[Reid Barton]

But then affine spaces over $\mathbb{R}_{\ge 0}$ are the convex spaces.

[Kevin Buzzard]

I see!

[Yaël Dillies]

Yeah, anything is a convex space over $\N$, and every set is $\N$-convex.

[Reid Barton]

So you could do that, but it doesn't really matter because you could also define "convex space" directly with the nonnegativity assumption built in, and of course $\mathbb{R}_{\ge 0}$ is the positive cone of a ring.

[Kevin Buzzard]

Is there a use for convex spaces which aren't subspaces of something sensible like a torsor for a real vector space?

[Reid Barton]

The nLab page has examples, apparently being embeddable in a torsor for a vector space is a kind of "cancellability" condition.

[Yaël Dillies]

Yeah, precisely because you get negation.

[Reid Barton]

The question I think is whether there is a use where the free convex spaces (i.e. the spaces parameterizing convex linear combinations) are themselves not embeddable in a module over a ring, and this is what I'm skeptical about

[Reid Barton]

so basically, convexity over a noncancellative semiring

[Yaël Dillies]

This I have no idea. But we can definitely come up with examples. What about ennreal-convexity, for example?

[Reid Barton]

it's the same as ordinary convexity, because $\infty$ doesn't lie in $[0, 1]$

[Reid Barton]

So what I said above wasn't a precise characterization, it's more like just $[0, 1] \subset R$ has to be cancellative in some sense, or something.

[Yaël Dillies]

For context, Yakov was interested in tropical geometry, where the usual stuff happens in $\mathbb R_{\ge 0}$.

[Kevin Buzzard]

But this is cancellative so the pathologies (non-homogeneity) I was concerned about don't show up.

[Yaël Dillies]

So I guess this could be converted to $\R$-convexity, but at the price of coercing everywhere.

[Kevin Buzzard]

By $\R$-convexity do you mean the useless notion (must be able to do $av+bw$ if $a+b=1$ with no positivity constraints, so it's just an affine space) or the usual notion?

[Reid Barton]

I meant the usual one

[Reid Barton]

Also when people talk about convexity in tropical geometry, I think they mean convexity in the usual sense (involving the usual multiplication on the reals), right?

[Yaël Dillies]

Apparently not. https://arxiv.org/pdf/math/0308254.pdf

[Yaël Dillies]

And the tropical semiring is most definitely not cancellative.

[Reid Barton]

What are you referencing specifically?

[Yaël Dillies]

Their definition of "tropical convexity"

[Reid Barton]

Really?

[Yaël Dillies]

𝕜-tropical convexity is precisely tropical 𝕜-convexity.

[Reid Barton]

image.png

[Reid Barton]

This one?

[Yaël Dillies]

Yeah

[Yaël Dillies]

I am not quite sure of what happened to a + b = 1.

[Reid Barton]

How so?

[Yaël Dillies]

Theorically, 1 : tropical 𝕜is 0 : 𝕜, so it should translate to min a b = 0, which isn't the case here?

[Reid Barton]

It seems much more like being a tropical 𝕜-module, right?

[Yaël Dillies]

Yeah actually

[David Wärn]

If you're used to thinking about vector spaces, then you might be surprised by the notion of "module over a ring" which allows weird non-free modules, but that doesn't mean it's not a good notion

[David Wärn]

I would assume that this unbiased notion of affine combination space is also the good one for general semirings

[David Wärn]

Is there a reason to believe it's not?

[Yaël Dillies]

That's where I'm coming from, indeed.

[Kevin Buzzard]

But the monoid action is an example where the naive approach ("just copy the axioms for a group action") gives you something which you might not want, because you have to add the extra axiom that m*_ is bijective, which is automatic in the group case.

[Kevin Buzzard]

Put another way, there are two definitions of group action, both of which make sense for monoids and give different structures

[David Wärn]

Right, but why would you require m* to be bijective? It's like saying modules have to be free

[Kevin Buzzard]

I'm saying that I've seen the definition of a group action on a set given as being a multiplicative map from G to Aut(S) and I'm observing that this definition makes sense for monoids, and I'm deducing that just because a random mathlib definition makes sense in some larger generality doesn't mean it's the "correct" definition in some larger generality, and the proof is that there are two definitions of a group action both of which make sense for monoids and become different concepts

[Patrick Massot]

The definition of monoid actions definitely doesn't ask for bijective maps.

[Kevin Buzzard]

Sure

[Kevin Buzzard]

But you can't deduce from this that an arbitrary definition which makes sense in more generality is "correct" in that greater generality

[Kevin Buzzard]

And my argument gives a proof that this can't always be true

[Yury G. Kudryashov]

Another reason to talk about convexity in nnreal-semimodules: the set of invariant measures of a map is convex.

[Yaël Dillies]

Ahah! This example is interesting because one thing we forgot is that having negative elements in the base (semi)ring also affects the space. That's because an add_comm_monoid acted on by a ring through module is promotable to an add_comm_group, negation in the space being -1 • x.

[Yaël Dillies]

So, by forcing the scalars to be a ring , we a fortiori force the space to be an add_comm_group.

[David Wärn]

Kevin Buzzard said:

But you can't deduce from this that an arbitrary definition which makes sense in more generality is "correct" in that greater generality

Sure, you can't deduce that "unbiased affine combination space" is a good notion just because it specializes to give affine spaces over fields. But still, I think it's definitely a good notion. For example, it specializes to give both the usual affine spaces and convex spaces, the category of such spaces is monadic over Type (so it's a nice algebraic notion), it has a forgetful functor from the category of semimodules, and you get the usual restriction-of-scalar functors (which is to say that you'll get lots of examples of these spaces). What's there not to like? In general this kind of space won't be a torsor for some semimodule, but I think this is just like how modules aren't generally free, and rings don't generally have unique factorisation (i.e., it's not necessarily a sign that you have the wrong notion).

[Kevin Buzzard]

If you've put some thought into it and understand that it's the correct definition then that's fine :-) My point is only that this needs to be done. Thanks for doing it :-)

[Yaël Dillies]

Should I understand that I have your blessing for defining them? :grinning_face_with_smiling_eyes: How should they be called?

[David Wärn]

You could say affine_combination_space to distinguish from the torsor affine_space, but it's a mouthful

[Yaël Dillies]

Is convex_space fine?

[David Wärn]

What do you mean by convex_space?

[Yaël Dillies]

The above

[Yaël Dillies]

What's bothering me with this name is that we never have to restrict to positive coefficients.

[David Wärn]

So an affine combination space over a semiring R?

[Yaël Dillies]

Yeah

[David Wärn]

It's a nice name I suppose, but maybe a bit misleading since R can have negative elements

[David Wärn]

To be clear, I'm not at all an expert on this, and agree that it's not clear what the best definition to formalise is. After thinking about this some more, my armchair understanding is that affine combination space isn't a very good notion for every semiring R, although it makes sense when R is a ring, or has enough multiplicative inverse (like nnreal). It was pointed out above that every set is an affine combination space over $\N$ in a unique way. But in fact there is a sensible notion of convex subsets in $\Z$-modules like $\Z^n$, which you can use also to define convex functions (those for which the upper graph is convex); you just won't get it from thinking about $\Z^n$ as an affine combination space over $\N$.

In this situation, you might prefer to use something like the "slice category" definition mention on nlab. Namely, say an affine space over a semiring $R$ is an $R$-semimodule $P$ together with a linear map $w : P \to R$. Think of an element of $P$ as a kind of weighted sum, and $w$ as giving its weight, so really $w^{-1}(1)$ is what you would normally think of as the underlying type of an affine space, but if $R$ doesn't have enough multiplicative inverses then this type doesn't tell you very much about all of $P$. Now you get a "forgetful functor" $M \mapsto M \times R$ from semimodules to affine spaces. Taking $R = \N$, I believe you can understand convex subsets of $\Z^n$ in terms of the "underlying" affine space.

[Yaël Dillies]

With that definition, would {0, 2} be $\Z$-convex in $\Z$?

[Adam Topaz]

I haven't been following this discussion at all, but I do think it's worthwhile to mention that the axioms of a convex space (or whatever you want to call it) can be formalized as an abstract algebraic gadget, without reference to any ring or semirng.
Essentially, consider a commutative monoid with $0$, say $R$, endowed with a function $\sigma : R \to R$ and a function $R^3 \to R$ denoted $(x,a,b) \mapsto C_x(a,b)$. Think of this as a signature (in the sense of first order logic), and consider the axioms appearing in nlab#convex-space which can all be written down without reference to any (semi)ring, given the data above (where $\sigma(t)$ should take the place of $1-t$), together with axioms like $\sigma(1) = 0$ and $\sigma(\sigma(t)) = t$ for all $t$.

[Adam Topaz]

(I don't know if these axioms actually give the same theory that's satisfied by all rings, but it's certainly contained in there.)

[Yury G. Kudryashov]

I see that the focus moved to "what is the right super-general definition?". I think that instead of this we should decide what example do we care about, then write a definition that will work in these cases. Whoever starts caring about a use case not covered by the current definition may refactor.

[Yury G. Kudryashov]

@Adam Topaz How exactly do you suggest to encode this in Lean?

[Adam Topaz]

class cing (A : Type*) extends monoid_with_zero A :=
(sigma : A \to A)
(C : A \to A \to A \to A)
... axioms

[Yaël Dillies]

That's what I started doing on branch#convex_space, right?

[Yury G. Kudryashov]

@Adam Topaz And what is a convex_space?

[Yaël Dillies]

I haven't yet gone through all the axioms, but this is certainly where I was heading.

[Adam Topaz]

Yaël Dillies said:

That's what I started doing on branch#convex_space, right?

It looks like you're working with semirings, rigght?

[Adam Topaz]

Yury G. Kudryashov said:

Adam Topaz And what is a convex_space?

The analogue of a module over a cing

[Yaël Dillies]

Only because they give me a 1. I could relax to add_monoid + has_one.

[Adam Topaz]

Well, I want, e.g. $\{0,1\}$ with $\sigma(0) = 1$ to be such a gadget as well... no addition necessary

[Yaël Dillies]

Wait sorry what's a cing? :astonished:

[Yury G. Kudryashov]

@Adam Topaz Is there any specific example you care about where this generality is important?

[Adam Topaz]

This is the smallest reasonable algebraic theory where one can define the analogue of Milnor K-theory, but I don't know if anything meaningful can be said about such gadgets in the abstract

[Yury G. Kudryashov]

I have these examples in my head:

• real vector spaces;
• vector spaces over rational numbers;
• affine spaces over real or rational numbers;
• nnreal-semimodules, including measures.

[Adam Topaz]

Yury G. Kudryashov said:

Adam Topaz Is there any specific example you care about where this generality is important?

The interval $[0,1]$ would also be an example.

[Yury G. Kudryashov]

I'm talking about convex spaces, not instances of cing.

[Yaël Dillies]

I assume going from my definition of convex space to your abstract gadgets is a rather independent step, right?

[Adam Topaz]

Ah, well I think "modules" over $[0,1]$ in this sense should be the usual convex spaces (well, maybe there would be some weird quotients)

[Yury G. Kudryashov]

I don't think that we should generalize for the sake of generalization.

[Yaël Dillies]

I'm not against it, but clearly refactoring from semimodules to convex/unbiased affine spaces is gonna be some sleepless nights already.

[Yaël Dillies]

Yury G. Kudryashov said:

I don't think that we should generalize for the sake of generalization.

Category-theory-phobic :rofl:

[Yury G. Kudryashov]

@Adam Topaz The main problem I see with any definition is that once we have a theory that covers both modules over nnreals and real affine spaces, we get a diamond for real vector spaces.

[Adam Topaz]

Yes @Yury G. Kudryashov, I agree, this would not solve any diamond issues.

[Adam Topaz]

(Sorry, i have to run! I would be happy to discuss this laterr!)

[Yaël Dillies]

Well, there's no way around that diamond. So why not go for it anyway? Having a theory accessible through a def is better than not having it at all.

[Yaël Dillies]

Wait, once we have convex_space, what would be the point of affine_space? Maybe we can generalize the definition of affine_space rather than defining a new class.

[David Wärn]

Yes, it might be a good idea to change the definition of affine_space to be an affine combination space. You would get a different API, since you wouldn't have an unbundled vector space parameter. Instead you could define "the module associated to an affine space", and prove that any nonempty affine space over a ring is a torsor for this module.

[Yury G. Kudryashov]

BTW, this will solve the diamond. We can have a definition (not an instance) add_torsor.to_affine_space and a type class saying that add torsor and affine space structures agree.

[Yury G. Kudryashov]

BTW, this will solve the diamond. We can have a definition (not an instance) add_torsor.to_affine_space and a type class saying that add torsor and affine space structures agree.

[Yury G. Kudryashov]

But this is a large refactor

[Yury G. Kudryashov]

And you shouldn't add an instance of add torsor with a manually constructed module because the additive group in the definition of add torsor is an out param

[Yury G. Kudryashov]

What do you plan to use as the basic operation in the new affine_space? Something like Π (x y : R), x + y = 1 → P → P → P?

[Yury G. Kudryashov]

Or affine_comb (f : P →₀ R) (hf : f.sum id = 1) : P?

[Reid Barton]

I think the laws are (a lot?) easier to state for the second form

[Yury G. Kudryashov]

In the first form the axioms will be similar to those in https://ncatlab.org/nlab/show/convex+space#definition

[Yury G. Kudryashov]

But building affine_comb from the binary operation is not trivial.

[Joseph Myers]

Note that the vast bulk of lemmas about affine_space are really lemmas about add_torsor for a module (they involve vectors, they don't involve affine combinations), and, similarly, most of the lemmas about affine_subspace are really about a sub-torsor as they also involve vectors (constrained so that the subgroup is a submodule). So if you redefine affine_space, existing lemmas (that currently use the affine_space notation) should probably change to be about add_torsor and something similar should be done for renaming affine_subspace.

[Yaël Dillies]

Yury G. Kudryashov said:

But this is a large refactor

I have time to spare. I'm a Cambridge student :rofl:

[Yaël Dillies]

So are we heading towards changing affine_space from an abbreviation of add_torsor to an unbiased affine space?

[Antoine Chambert-Loir]

The definition of a monoid action will imply that invertible elements map to invertible elements, because it maps the unit element of the monoid to identity. But think of a semigroup action, where semigroups are just associative laws, possibly without unit — then a group action would not be a semigroup action of a group.

Similar question : a monoid action can be defined either as a map $M\times X \to X$ (plus axioms) or as a morphism of monoids from $M$ to the monoid of self-maps of $X$. For mathematicians, both are rapidly equivalent, and we switch from one to another (Bourbaki has a stylistic convention, speaks of action and of operation), but for automatic formalization, how are the two reconciled?

And for actions of topological monoids, the first definition is the good one, namely, the continuity of the map $M\times X\to X$, because for most applications, eg, representations of topological groups on Hilbert spaces, the map $M\to \operatorname{Aut}(X)$ is not continuous.

[Johan Commelin]

(Tip: Zulip needs double $$s around maths.)
We tend to focus on the $M × X → X$ approach. It can be easily combined with nice notation, and works well together with forgetting structure. (E.g. a module is a monoid action. And it is the exact same map $M × X → X$, but for the $M → \text{End}(X)$ you would need to change the version of $\text{End}$ that you are considering.)

[Yaël Dillies]

I lost track of the discussion. Can someone explain me what I should do?

[David Wärn]

I think you should define unbiased affine combination spaces over a semiring R, and call it affine_space R

[Yaël Dillies]

affine_space R P, rather?

[Yaël Dillies]

I mean something like

class affine_space' (𝕜 E : Type*) [semiring 𝕜] :=
(affine_comb (f : E →₀ 𝕜) (hf : f.sum (λ x, id) = 1) : E)
-- more axioms

[Yaël Dillies]

Do you know what axioms I need?

[David Wärn]

You want an "associativity axiom", which says that an affine combination of affine combinations is ... some affine combination. And a "unitality" axiom which says that if you combine just one point with weight one, you get that point

[Yaël Dillies]

Is that it?

[David Wärn]

I think so. This is a general way of stating axioms for algebraic theories (you just have the two axioms for algebras over a monad)

[Yaël Dillies]

Okay. And what about this?
Yury G. Kudryashov said:

BTW, this will solve the diamond. We can have a definition (not an instance) add_torsor.to_affine_space and a type class saying that add torsor and affine space structures agree.

[Scott Morrison]

The associativity axiom is going to be quite painful expressed in terms of finitely supported functions!

[Scott Morrison]

It would be much easier to state in terms of indexing types.

[Yaël Dillies]

Do you mean affine_comb (ι : Type*) (f : ι →₀ 𝕜) (hf : f.sum (λ x, id) = 1) : E or affine_comb (ι : Type*) [fintype ι] (f : ι → 𝕜) (hf : ∑ x : ι, f x = 1) : E?

[Scott Morrison]

I think you need something more complicated: you need an indexing type, and both a function into k and a function into E

[Scott Morrison]

(to tell you the weights, and the points)

[Reid Barton]

It's still going to be a little awkward with indexing types for universe reasons

[Yaël Dillies]

Oh yeah of course. I mean, this is really about putting docs#finset.center_mass (or docs#finset.affine_combination) inside the typeclass.

[Reid Barton]

Maybe, since the type is finite anyways, you should use Type

[Reid Barton]

I guess you can define a universe-polymorphic affine_comb after the fact

[Reid Barton]

By the same logic, you could just use fin n as the indexing type but then it's again a little awkward to state associativity

[David Wärn]

I don't think it's too bad in terms of finsupp. Here's the statement of associativity, modulo two sorries (edit: hopefully it's right this time)

variables (R : Type) [semiring R] (α : Type)

def T : Type := { v : α →₀ R // v.sum (λ _, id) = 1 }

variables {R α}

def map {β} (f : α → β) (v : T R α) : T R β := ⟨v.val.map_domain f, sorry⟩
def μ (v : T R (T R α)) : T R α := ⟨v.val.sum (λ w r, r • w.val), sorry⟩
def associativity (comb : T R α → α) : Prop := ∀ v, comb (μ v) = comb (map comb v)

[Reid Barton]

For the convex version we have docs#pmf, though it's limited to real

[Yaël Dillies]

Given that affine_space is used quite widely, what do you think of first defining affine_space' and slowly refactor? Or do you prefer that I instead first rename all the affine_space to add_torsor?

[Joseph Myers]

You definitely need to define some kind of def for affine combinations (separate from that appearing in the type class) after the fact, even apart from any universe issues with index types, simply to get a version which is a bundled affine map (whatever form of affine maps makes sense with this affine space definition; I suppose that's maps that preserve affine combinations, with the linkage to linear maps then becoming something defined only for the type class that asserts propositional equality between the affine combinations in the definition and the affine combinations derived from the add_torsor structure).