Faces of Cones

Stream: maths

[Martin Winter]

Olivia (@ooovi ) and me are implementing faces for PointedCone. Plenty thought went into choosing the right definition. For example, we are now confident that we cannot base our definition on the existing IsExtreme for reasons I can elaborate below. Instead, we will likely go for one of the following: given two pointed cones F and C, F is a face of C if it is contained in C and satisfies either

∀ x ∈ C, ∀ y ∈ C, ∀ a > 0, ∀ b > 0, a • x + b • y ∈ F → x ∈ F

or

∀ x ∈ C, ∀ y ∈ C, x + y ∈ F → x ∈ F

Here we want to ask the community to help decide which of these we should go for.

First, note that we work over a general ordered Ring (and for most part even over Semiring). The first definition is closer to the textbook definition, but the second one is obviously more convenient to work with (it is essentially a reverse add_mem).
Very conveniently, we proved that both definitions are equivalent in many of the usual applications, in particular, if R is a field or an Archimedean ring (such as $\Bbb Z$). The precise statement is that the definitions are equivalent if and only if the ring satisfies ∀ ε > 0, ∃ ω, 1 ≤ ω * ε.

Even over general rings, both definitions yield all basic properties of faces one expects. Most relevant, faces form a complete lattice, with the cone itself as the top face and the lineality space as the bottom face.

There is one main difference we noticed between the definitions that we believe should be the basis for making the decision for one or the other. Consider a non-Archimedean ring R obtain from $\Bbb Z$ by adjoining an infinitesimal element ε. Consider the positive elements of the ring as a PointedCone R R.

• Using the first definition this cone has precisely two faces: top and bot.
• Using the second definition there are infinitely many more faces: the ideals $\epsilon^n R_+$ of positive infinitesimals.

We are not aware of any "right" answer to the question what the faces should be, but perhaps someone cares about this and can give some input.

[Martin Winter]

Regarding why we cannot base faces on IsExtreme. A first conceptual/aesthetic reason is that the existing definition of IsExtreme (and same for IsExposed) is an "affine" notion rather than "linear" one. This means that it uses convex combinations rather than positive combinations (and affine subspaces rather than linear subspaces for IsExposed). I would make the point that these definition should be stated on an affine space rather than on submodules.

But leaving this aside, we found the following concrete problem: A valid use case for pointed cones that we envision is the positive integer lattice which is a $\Bbb Z$-cone. There is a clear understanding of what the faces of that cone should be. However, IsExposed is based on open segments and the open segment $(0,1)$ is empty over $\Bbb Z$. This leads to no subcone of the positive grid being considered a face. The definitions given above do however work correctly.

[Martin Winter]

Lastly, we wonder whether anyone knows what these rings R with the property ∀ ε > 0, ∃ ω, 1 ≤ ω * ε are, whether there is a name for them or a preexisting way to express them as a typeclass. If we are going for the second definition one might want to use the equivalence to the first definition when it holds. Since both fields and Archimedean rings such as $\Bbb Z$ are valid use cases for our theory, we would need to write all lemmas twice (once for field, once for Archimedean ring). Ideally there is a single typeclass that triggers for both cases. And if not, would it be fine to implement one specifically for this reason?

I also asked on MO about these rings, without much success.