Zulip Chat Archive

Stream: PR reviews

Topic: 3728: define ordered semimodules and generalize convexity...


view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:06):

@Frédéric Dupuis I'm rewriting convexity for affine spaces, and I have a question about your old PR #3728
Many lemmas assume {β : Type*} [ordered_add_comm_monoid β] [ordered_semimodule ℝ β]. Is there any reason to prefer these assumptions to {γ : Type*} [ordered_cancel_add_comm_monoid γ] [ordered_semimodule ℝ γ]? A (semi)module over can't be just an add_comm_monoid anyway (unless someone forgot to define an instance).

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:07):

It makes sense if you're going to generalize to {β : Type*} [ordered_add_comm_monoid β] [ordered_semimodule nnreal β].

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:08):

Do you need this generalization in some case?

view this post on Zulip Johan Commelin (Aug 20 2020 at 03:08):

@Reid Barton and I were just talking about ordered semimodules yesterday :rofl:

view this post on Zulip Johan Commelin (Aug 20 2020 at 03:08):

Didn't realise there was a PR :see_no_evil:

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:08):

The PR is already merged!

view this post on Zulip Johan Commelin (Aug 20 2020 at 03:09):

/me should learn what is in mathlib!

view this post on Zulip Johan Commelin (Aug 20 2020 at 03:09):

That's what you get for going on holidays

view this post on Zulip Johan Commelin (Aug 20 2020 at 03:12):

@Yury G. Kudryashov What's your reason for preferring the cancellative version?

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:12):

Copy+paste from wrong line

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:12):

Fixed.

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 03:27):

I'm going to wait for an answer before porting convex_on.

view this post on Zulip Frédéric Dupuis (Aug 20 2020 at 11:55):

I didn't have any particularly good reason -- at the beginning I was hoping it would allow us to define convexity for functions into things like nnreal, but as you say it doesn't work anyway. I'd be happy with just ordered_add_comm_group, it would clean things up a bit.

view this post on Zulip Frédéric Dupuis (Aug 20 2020 at 13:36):

Although now that I think about it, [ordered_semimodule nnreal β] might be useful for things like weighting Hermitian matrices by probabilities.


Last updated: May 06 2021 at 12:15 UTC