Redefining `AbsConvex` to use a single ring of scalars

Stream: mathlib4

[Christopher Hoskin]

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:

def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s

At the time this definition was formulated, Mathlib's definition of Convex required the scalars to be an OrderedSemiring whereas the definition of Balanced required the scalars to be a SeminormedRing. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as AbsConvex if it is balanced over a SeminormedRing 𝕜 and convex over ℝ.

Recently the requirements for the definition of Convex have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature.

I've opened a PR to make this change (#29342) but @Jireh Loreaux has suggested that it should be discussed here first, in particular the partial order on the complex numbers https://github.com/leanprover-community/mathlib4/pull/29342/files#diff-ba50cd1f8d6dfb5d017128c6e40f79de27adf53ce8c572d22bef36ff7a777795R85

Previous discussion:

• https://github.com/leanprover-community/mathlib4/pull/17029#discussion_r1782249323
• https://github.com/leanprover-community/mathlib4/pull/26345#discussion_r2287535746

Thanks,

Christopher

[Christopher Hoskin]

Are there any opinions on this or alternative suggestions on how to proceed please? @Yaël Dillies @Eric Wieser @Filippo A. E. Nuccio @Moritz Doll @Jon Bannon @Anatole Dedecker @Monica Omar (list of people who have been kind enough to comment on related PRs). Thanks.

[Filippo A. E. Nuccio]

I am sorry, I had completely overseen your first message. I'll try to have a look, but as a start I do not understand why docs#IsOrderedRing is not IsOrderedSemiring.

[Yaël Dillies]

Oh, that's just the same reason as to why docs#Module is not called Semimodule: when a typeclass covers several use cases, we do not necessarily name it after the most general one, but after the most common one.

[Filippo A. E. Nuccio]

Well, but this is highly misleading I find. Since we put some effort in the library to keep Semiring and Ring separated (unlike Semimodule, that appears much less), I would expect a different treatement. Or is it a general agreement to avoid Is+ Semi altogether?

[Yaël Dillies]

Filippo, I am sympathetic to your argument, but this is a different discussion to the one Christopher is trying to have

[Filippo A. E. Nuccio]

Yes, good point. My apologies. I'll try to look at the PR and might resurrect this point elsewhere. Thanks for the alert :slight_smile:

[Yaël Dillies]

I have thought about this a bit a while ago, and I seem to remember that it was important that the two scalar rings could be different. I do not think it matters further than being able to set one of them to \R and the other one to \C (or similarly \Q and \Q(i)), so if you're willing to talk about the order on \C/\Q(i), then I see no downside to your refactor.

[Yaël Dillies]

Do people in fact care about \Q-absolutely convex sets?

[Christopher Hoskin]

Yaël Dillies said:

I have thought about this a bit a while ago, and I seem to remember that it was important that the two scalar rings could be different.

The other possibility would be to make the definition something like this:

variable (𝕜₁ 𝕜₂) [SeminormedRing 𝕜₁] [SMul 𝕜₁ E] [SMul 𝕜₂ E] [Semiring 𝕜₂] [PartialOrder 𝕜₂]
  [AddCommMonoid E]
/-- A set is absolutely convex if it is balanced and convex. -/
def AbsConvex (s : Set E) : Prop := Balanced 𝕜₁ s ∧ Convex 𝕜₂ s

Yaël Dillies said:

I do not think it matters further than being able to set one of them to \R and the other one to \C

I introduced convex_RCLike_iff_convex_real in #29248 to move between the real and complex case.

Yaël Dillies said:

(or similarly \Q and \Q(i))

I occasionally find myself wondering how much of RCLike actually holds for any quadratic alternative real division algebra (i.e. ℝ, ℂ, ℚ and 𝕆) - but I haven't given that any serious thought.

[Yaël Dillies]

Christopher Hoskin said:

The other possibility would be to make the definition something like this:

Yes, but at this point are you saving much over just using Balanced 𝕜₁ s ∧ Convex 𝕜₂ s?

[Christopher Hoskin]

Christopher Hoskin said:

At the time this definition was formulated, Mathlib's definition of Convex required the scalars to be an OrderedSemiring whereas the definition of Balanced required the scalars to be a SeminormedRing. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as AbsConvex if it is balanced over a SeminormedRing 𝕜 and convex over ℝ.

This was just guesswork on my part, so there may have been other reasons for defining it this way.

[Filippo A. E. Nuccio]

For what is worth, there is a crucial user of convexity for vector spaces over nonarchimedean fields, and there quadratic extensions are galore. That being said, the current definition of convex, even with this refactor, does not align with the one used in that context .

[Christopher Hoskin]

Kaup and Upmeier, Jordan algebras and Symmetric Siegel Domains in Banach Spaces, Math. Z. 157, 179-200 (1977) define complex extreme points (and by extension complex convexity) using scalars in the unit ball of ℂ rather than the positive unit ball.

[Kenny Lau]

@Christopher Hoskin do you have a usecase in mind?

[Kenny Lau]

Yaël Dillies said:

one of them to \R and the other one to \C

but isn't the C-unit disc in C the same as the R-unit disc in C?

[Kenny Lau]

oh, never mind, they are different

[Kenny Lau]

do you remember why you needed that?

[Monica Omar]

am i right in thinking that they’re equivalent definitions? a 𝕜-balanced set is 𝕜-convex iff it’s ℝ-convex?

[Kenny Lau]

what does 0<x<1 mean if x is complex?

[Monica Omar]

right, but we’re weakening the definition to a seminormed ring /bbk, not R or C

[Monica Omar]

ignore me. this refactor looks fine to me

[Kevin Buzzard]

Kenny Lau said:

what does 0<x<1 mean if x is complex?

According to mathlib it means terms of this type:

import Mathlib

open scoped ComplexOrder

example : Type := {x : ℂ // 0 < x ∧ x < 1}

[Anatole Dedecker]

They are precisely the real numbers 0 < x < 1, see docs#Complex.lt_def and the aforementionned docs#convex_RCLike_iff_convex_real

[Monica Omar]

lol I thought kenny's question was rhetorical

[Anatole Dedecker]

Ah, maybe it was, but I guess answering it doesn't hurt x)

[Anatole Dedecker]

I think I'm in favor of this refactor. Anything that means that we don't have to work with both a real and a complex structure is good, and mathematically it shouldn't change anything (unless people care about this definition for other rings, but I can't really see that happening)