Design for positive cones

Stream: mathlib4

[Artie Khovanov]

Let $G$ be a group. A submonoid $M\leq G$ induces a preorder on $G$ via $a\leq b\iff a-b\in M$. Consider the support $\operatorname{supp}M\coloneqq M\cap-M$. This is exactly the equivalence class of $0$, so the quotient poset forms an ordered group $G/\operatorname{supp}M$. This order is total if and only if $M\cup-M=G$. Conversely, the positive cone $\{g\geq0\}$ of an ordered group is a submonoid with zero support.

The story repeats for convex cones and modules over an ordered ring, and (with one slight variation) for semirings and rings. The story for modules is partially formalised in Mathlib at docs#PointedCone, and the one for groups and rings at docs#GroupCone and docs#RingCone. I would like to refactor Mathlib to unify these definitions and results.

I can think of two main ways to design the formalisation in a uniform way:

1. Have generic classes IsSalient s := ∀ x, x ∈ s → -x ∈ s → x = 0 and IsGenerating s := ∀ x, x ∈ s ∨ -x ∈ s on any SetLike type over a type with negation.
2. Define classes IsSalient and IsGenerating on the type AddSubmonoid _, making use of dot notation for convex cones and subsemirings.

The advantage of (1) is that it makes automation (simp, aesop) easier. The advantage of (2) is that it makes typeclass search easier. I don't have a good reference point for designing predicates on generic substructures. Does anybody have thoughts on how to proceed?

[Yaël Dillies]

When you say "generic classes", do you mean that IsSalient and IsGenerating would be predicates on sets?

[Artie Khovanov]

Yaël Dillies said:

When you say "generic classes", do you mean that IsSalient and IsGenerating would be predicates on sets?

No, on SetLike types. Like how docs#HasMemOrNegMem ("IsGenerating") is formalised currently.

[Yaël Dillies]

So this will be a definition scheme, right? in the sense that you get one predicate for each SetLike type. As you know, we are moving away from definition schemes when dealing with morphisms. Shouldn't we move away from them when dealing with subobjects too?

[Artie Khovanov]

Yes, it would be. And yes docs#RingHom.ker was on my mind when I asked this.

[Artie Khovanov]

The problem is that set membership on a SetLike type works differently than bundled function application. That is, x ∈ s does not elaborate to x ∈ s.toSet. This means that, if S : Semiring R, then S.IsSalient := ∀ x, x ∈ s.toAddSubmonoid → -x ∈ s.toAddSubmonoid → x = 0. This expression simplifies to what we want, but it is not defeq to what we want, which makes matching on hypotheses of the form x ∈ s difficult. On the other hand, f x for a FunLike type elaborates to f.toFun x via a coercion, avoiding this issue.

[Yaël Dillies]

Artie Khovanov said:

which makes matching on hypotheses of the form x ∈ s difficult

But do you rewrite x ∈ s hypotheses often?

[Artie Khovanov]

Yeah true. But you do sometimes want to partially apply eq_zero_of_mem_of_neg_mem, especially when using automation like aesop. I suppose I can just add an extra lemma for each structure I work with.

[Yaël Dillies]

How many generalisable lemmas are we talking about? 10? 100? 1000?

[Artie Khovanov]

3

[Artie Khovanov]

To be fair the number of extra instances in the other approach is very low too

[Yaël Dillies]

IMO that's way too low a number to justify the overhead cost

[Artie Khovanov]

Alright so something like
docs#HasMemOrNegMem, docs#PositiveCone.IsGenerating -> (Add)Submonoid.IsGenerating
docs#AddGroupCone, docs#RingCone, docs#PositiveCone.IsSalient -> (Add)Submonoid.IsSalient

[Artie Khovanov]

Tagging @Bjørn Solheim because I've seen him do work on the convex cone side. Does my refactor seem reasonable?

[Bjørn Solheim]

Thanks for the tag. I believe you have a good suggestion (focusing on the more fundamental sub-monoid structure). The following might be relevant: the total order inducing criteria you are proposing is stronger than the current IsGenerating for ConvexCones (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Convex/Cone/Basic.html#ConvexCone.IsGenerating). Therefore there might be some issues regarding which terminology to use. Maybe IsTotal can be considered? For IsSalient I think the notions coincide with the current library version (possibly modulo the inclusion of zero).

Note that the ConvexCone definition is over positive scalars and thus is separate and different from the submodule over nonnegative scalars definition for PointedCones. There are transport mechanisms but this could be relevant for what you are envisioning. Both IsGenerating and Salient are defined for convex cones (and then later transported to pointed cones).

[Artie Khovanov]

Thanks for the info!
"Generating cone" is, I believe, the standard name for the thing I want. The exact predicate is in Mathlib as docs#ConvexCone.IsReproducing, and they're equivalent for pointed cones over a ring.

[Artie Khovanov]

The fact positive cones aren't submonoids is a bit annoying - are non-pointed cones used much in Mathlib? I think I will just redefine the predicates for submonoids.

[Artie Khovanov]

Oh wow the design for docs#ConvexCone, docs#ConvexCone, docs#PointedCone is really strange - it's a series of coercions, instead of structure classes or projections. @Yaël Dillies have you seen anything like this before?

[Yaël Dillies]

What's PositiveCone?

[Artie Khovanov]

(fixed)

[Yaël Dillies]

What design did you expect?

[Artie Khovanov]

Either ConvexConeClass or a .toConvexCone non-coercion projection

[Yaël Dillies]

We don't really use PointedCones as subobjects, and ConvexCone is rather odd as it doesn't even really represent subobjects!

[Artie Khovanov]

I don't really get why docs#ConvexCone exists tbh. I know it's the pen-and-paper definition, but it's just an axiomatisation of docs#PointedCone (ie a semimodule over the positive cone of a ring) without the 0 point.

[Artie Khovanov]

The situation with docs#PointedCone and docs#ProperCone seems more reasonable to me, it's just the closed subgroup design.

[Artie Khovanov]

Yeah OK: the only place in Mathlib where docs#ConvexCone is used to prove things not about itself is for the Riesz Extension Theorem.
image.png

[Artie Khovanov]

This theorem is not affected by changing docs#ConvexCone to docs#PointedCone.

[Bjørn Solheim]

I am sure there were reasons for choosing the path of ConvexCone as it exists in mathlib (although I am not familiar with them). But I would agree that PointedCones is more in line with the notion of conic/conical span/hull. And, while terminology choices are always difficult and multifaceted, I think convex cone terminology based on convex cones with nonnegative scalars is more common than the positive scalars only version (although it is mentioned on Wikipedia).

[Artie Khovanov]

I'm not necessarily saying we should make this refactor now - but I am pointing out that doing so would be very easy. In particular, the predicates on docs#ConvexCone.Blunt and docs#ConvexCone.Pointed do not appear to be used at all except to bundle docs#ConvexCone into docs#PointedCone.

[Artie Khovanov]

Basically I'm saying that we shouldn't worry about duplicating work done by docs#ConvexCone for docs#PointedCone, because I don't think there's actually any work being done.

[Artie Khovanov]

From the copyrights: looks like docs#ConvexCone was written in 2020 by Yury, and docs#PointedCone was contributed in 2023 by Apurva Nakade.
@Yury G. Kudryashov do you remember the considerations that went into choosing the "strictly positive" definition of positive cones in vector spaces rather than the "non negative" one?

[Yury G. Kudryashov]

I don't remember

[Yury G. Kudryashov]

I think I've added them because they were needed as a dependency for something. I don't mind if you redefine them (assuming that people who actually care about this part of Mathlib don't mind either).

[Artie Khovanov]

OK thanks, I suspected so (they're apparently needed for integration)

[Artie Khovanov]

@ooovi saw that you are working in this area - do you have thoughts on the definition of convex cone? ^^

[Martin Winter]

The terminology PointedCone is also perceived rather negatively whenever I speak to mathematicians working in optimization/geometry. "pointed" is usually used for what mathlib calls "salient". When we move away from using ConvexCone, does the name become available for PointedCone? Together with Olivia (@ooovi ) we are currently working a lot on faces and duality theory for cones and PointedCone is the more important concept throughout.

[Martin Winter]

In fact, we never used ConvexCone. There is one case where one could consider using it: the relative interior of a PointedCone is a ConvexCone.

[Artie Khovanov]

Yeah I agree: rename docs#PointedCone to ConvexCone. Then IsPointed can be a name for "I don't contain any lines", which I want to be a predicate on AddMonoid as described upthread. I think IsPointed would be a good name for the predicate: we say "positive cone of an ordered group/ring" instead of "pointed monoid/semiring," but "cone" is already used in "convex cone" which is unfortunate for uniform naming.

[Artie Khovanov]

Although from a quick search "pointed monoid" can mean what Mathlib calls "monoid with zero"... ugh

[Artie Khovanov]

Related question: does the notion of "support" of a cone, defined as the union of lines it contains, come up in convex geometry or optimisation? The "support" of a subsemiring (defined as $C \cap -C$) comes up in real algebra / ordered ring theory. So, a submonoid / subsemiring / convex cone is proper iff it has zero "support".

[Martin Winter]

In convex geometry this is called the lineality space of a cone. We just introduced it as PointedCone.lineal in our recent (not yet approved) PR https://github.com/leanprover-community/mathlib4/pull/33664

[Artie Khovanov]

OK thanks! I will make sure to use that.

[Artie Khovanov]

If we are going to make this refactor, I would caution against moving files, in case we have to move them all back. But maybe it's fine since my story will take a while to implement.

[Artie Khovanov]

I guess one more question: I understand that the common term for "contains no lines" is "pointed," with "salient" sometimes used (most notably on Wikipedia). What is the common term in convex geometry for "the set of pointwise differences generates the space," or equivalently "the convex cone is not contained in a proper subspace"? I've seen "generating" and "reproducing".

[Martin Winter]

I usually use "full-dimensional", thought that might be too geometric for your generality. I heard people say "essential" or "spanning". But "generating" sounds not wrong for me either. I don't really like "reproducing".

[Artie Khovanov]

"generating" sounds a bit generic to me
"spanning" could work imo

[Artie Khovanov]

OK well I've added it to my project, it seems to work fine
Will PR eventually

[Artie Khovanov]

pinging @Mario Carneiro as the original author of the group/ring cone files

[Mario Carneiro]

This whole file looks completely different from when I worked on it. Originally, it was not meant to be used as such, it was just a temporary structure used to construct a partial order when you want to define "x is positive" or "x is nonnegative" rather than "x < y" or "x <= y"

[Mario Carneiro]

I guess people tried to give it more of a standalone mathematical meaning but it was really supposed to be a *Core kind of class, that's why I didn't want any infrastructure around it other than docs#IsOrderedRing.mkOfCone and the other versions for ordered groups and so on

[Artie Khovanov]

OK cool (yeah that was me rewriting). I guess I'm rewriting again to unbundle and unify everything.

[Artie Khovanov]

New question: it's been suggested in review (#33942) that IsPointed and IsGenerating should be defs rather than classes. Having to pass around IsPointed and IsGenerating as explicit arguments makes using dot notation for polymorphism more annoying. @Yaël Dillies or anyone else do you have thoughts on this?
(tagging @Eric Wieser and @Johan Commelin from the PR)

[Eric Wieser]

Can you give a short example of what you mean by the dot notation being annoying?

[Artie Khovanov]

Before:

AddSubmonoid.eq_zero_of_mem_of_neg_mem.{u} {G : Type u} [AddGroup G] (M : AddSubmonoid G)
  [M.IsPointed] {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) : x = 0

Subsemiring.IsPointed.eq_zero_of_mem_of_neg_mem.{u} {R : Type u} [Ring R] (S : Subsemiring R)
  [S.toAddSubmonoid.IsPointed] {x : R} (hx₁ : x ∈ S) (hx₂ : -x ∈ S) : x = 0

And then we can say M.eq_zero_of_mem_of_neg_mem, S.eq_zero_of_mem_of_neg_mem, S.toAddSubmonoid.eq_zero_of_mem_of_neg_mem and the x ∈ ? hypotheses are all in the right type.

Now:

AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem.{u} {G : Type u} [AddGroup G] {M : AddSubmonoid G}
  (hM : M.IsPointed) {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) : x = 0

Subsemiring.IsPointed.eq_zero_of_mem_of_neg_mem.{u} {R : Type u} [Ring R] {S : Subsemiring R}
  (hS : S.IsPointed) {x : R} (hx₁ : x ∈ S) (hx₂ : -x ∈ S) : x = 0

Then hS.eq_zero_of_mem_of_neg_mem has hypotheses x ∈ S.toAddSubmonoid etc, because the type of hS is still AddSubmonoid.IsPointed. We could change the namespace to just Subsemiring, but then we have to do S.eq_zero_of_mem_of_neg_mem hS.