Dual cones without the inner product space assumption

Stream: mathlib4

[Mitchell Lee]

The "inner dual cone" and "dual cone" constructions in mathlib (Set.innerDualCone and PointedCone.dual) require the cone to be a subset of an inner product space over $\mathbb{R}$. However, the construction can be done in much more generality, as follows.

Let $M$ be a module over an arbitrary ordered semiring $R$, and let $C \subseteq M$ be a pointed cone (i.e. an $R_{\geq 0}$-submodule of $M$, where $R_{\geq 0}$ is the subsemiring of $R$ consisting of the nonnegative elements). Then we may define the dual of $C$ to be the set

$$C^* = \{f \in M^* \, | \, \text{$f(v) \geq 0$ for all $v \in C$} \} \subseteq M^*,$$

where $M^* = \operatorname{Hom}_R(M, R)$ is the dual module. It is not hard to see that $C^* \subseteq M^*$ is also a pointed cone.

If $R = \mathbb{R}$ and $M$ is an inner product space, then there is a canonical isomorphism between $M$ and $M^*$, and thus the dual cone of $C$ can be thought of as a subset of $M$ rather than as a subset of $M^*$. This recovers the constructions that are currently in mathlib.

Many important theorems about cones can be stated in this generality. For example, one formulation of the Minkowski–Weyl theorem is that if $M$ is a finite-dimensional vector space over an ordered field $R$ and $C \subseteq M$ is a pointed cone which is finitely generated as an $R_{\geq 0}$-module, then so is $C^*$. I know @Yaël Dillies is working on this (#Is there code for X? > Main Theorem of Polytope Theory ).

Unfortunately, the supporting hyperplane theorem (which, in this formulation, can be stated simply as $C = C^{**}$) seems to require $M$ to be a finite-dimensional vector space over $\mathbb{R}$. But this assumption can be relaxed to $R$ being any ordered field if $C$ is finitely generated as an $R_{\geq 0}$-module (this is Farkas' lemma).

I think that this generality is quite important, because it is common to work with polytopes and cones over $\mathbb{Q}$ and $\mathbb{Z}$. (For one thing, this makes them computable.) I have created a github issue: #19738. However, I am not sure how to proceed with actually refactoring the existing library to work in this generality, or whether this is even a good idea. Does anyone have any thoughts?

[Johan Commelin]

Would it make sense to abstract away from $M^* = \text{Hom}_R(M,R)$ to a pair of modules $M,N$ with a perfect pairing?

[Johan Commelin]

Of course this excludes $M$ of infinite rank. But at the same time it brings back a symmetry, so that $C^{**} = C$ will typecheck again.

[Johan Commelin]

The perfect pairing approach is also the one used in docs#RootPairing

[Mitchell Lee]

Yeah, that would probably be a good idea.

[Mitchell Lee]

The dual can be defined with respect to any pairing (yielding an antitone Galois connection between the pointed cones in $M$ and the pointed cones in $N$), though many of the theorems will only hold for perfect pairings.

[Mitchell Lee]

Also, the concept of dual can be made even more general by replacing the subsemiring $R_{\geq 0}$ with an arbitrary subsemiring, though I am not sure if this has any use.

[Mitchell Lee]

For example, let $L / K$ be a field extension and let $V$ be a vector space over $L$. Then for any subspace $W \subseteq V$ over $K$, one may form the space

$$\{f \in V^* \, | \, \text{$f(v) \in K$ for all $v \in W$}\} \subseteq V^*$$

where $V^{*} = \operatorname{Hom}_L(V, L)$. Is this concept useful?

[Johan Commelin]

I don't see an immediate use for it. So I would stick to $R_{\ge0}$ for now.

[Mitchell Lee]

By the way, here's a coordinate-free and topology-free proof of (one direction of) Minkowski–Weyl for cones by a "deletion-contraction" argument. I can't find this in the literature, but I'm sure I'm not the first person to write this down. It is the result of simply taking the existing proofs using Fourier–Motzkin elimination and removing the coordinates from them. This is similar to how the exchange property in linear algebra can be thought of as removing the coordinates from Gaussian elimination.

Lemma

Let $W$ be a vector space over an ordered field $k$, let $v \in W^*$, and let $B \subseteq W$ be a finite set. Let $H^+ = \{w \in W \, | \, \langle v, w \rangle \geq 0\}$ be the half space corresponding to $v$, let $H = \{w \in W \, | \, \langle v, w \rangle = 0\}$ be the hyperplane corresponding to $v$, and let $C = \operatorname{span}_{k_{\geq 0}} B$ be the pointed cone spanned by $B$. Then $C \cap H^+$ is spanned over $k_{\geq 0}$ by the set $(B \cap H^+) \cup (C \cap H)$.

Proof

We use induction on the size of the set $B \setminus H^+$. In the base case, we have $B \subseteq H^+$; this implies $C \subseteq H^+$ and the lemma follows.

For the inductive step, suppose that the lemma holds for a set $B' \subseteq W$. That is, if we define $C' = \operatorname{span}_{k_{\geq 0}} B'$, then $C' \cap H^+$ is spanned over $k_{\geq 0}$ by the set $(B' \cap H^+) \cup (C' \cap H)$. Choose any $u \in W \setminus H^+$ (so $\langle v, u \rangle < 0$); we will show that the lemma holds for $B = B' \cup \{u\}$ as well.

Let $w \in C \cap H^+$; we will show that $w$ is in the $k_{\geq 0}$-span of $(B \cap H^+) \cup (C \cap H)$. If $w \in H$, this is obvious, so assume that $w \in H^+ \setminus H$; that is, $\langle v, w \rangle > 0$. Since $C$ is spanned by $C' \cup \{u\}$, we may write $w = a w' + b u$ for some $w' \in C'$ and $a, b \geq 0$. We have $\langle v, w \rangle = a \langle v, w' \rangle + b \langle v, u\rangle$. Since $\langle v, w \rangle > 0$ and $\langle v, u\rangle < 0$, we conclude that $\langle v, w' \rangle > 0$. Then

$$w = a w' + b u = \frac{\langle v, w \rangle}{\langle v, w'\rangle} w' + b\left(-\frac{\langle v, u \rangle}{\langle v, w'\rangle} w' + u \right)$$

Consider the vectors $w'$ and $-\frac{\langle v, u \rangle}{\langle v, w'\rangle} w' + u$ appearing in this nonnegative linear combination. The first vector $w'$ is in the $k_{\geq 0}$-span of $(B' \cap H^+) \cup (C' \cap H)$ by the inductive hypothesis. The second vector $-\frac{\langle v, u \rangle}{\langle v, w'\rangle} w' + u$ is an element of $C \cap H$: it is in $C$ because it is a nonnegative linear combination of $w'$ and $u$, and it is in $H$ by a simple computation. Hence, $w$ is in the $k_{\geq 0}$-span of $(B' \cap H^+) \cup (C' \cap H) \cup (C \cap H) = (B \cap H^+) \cup (C \cap H)$, as desired.

Lemma.

Let $W$ be a finite dimensional vector space over an ordered field $k$. Let $v_1, \ldots, v_n \in W^*$ and let $H_1^+, \ldots, H_n^+ \subseteq W$ be the corresponding half spaces (i.e. $H_i = \{w \in W \, | \, \langle v_i, w \rangle \geq 0\}$.) Then $C = H_1^+ \cap \cdots \cap H_n^+$ is a finitely generated pointed cone.

Proof

We use induction on $n$. If $n = 0$, then $C = W$. Since $W$ is finitely generated over $k$ and $k$ is finitely generated over $k_{\geq 0}$ (by $1$ and $-1$), we conclude that $C = W$ is also finitely generated over $k_{\geq 0}$, as desired.

Suppose $n > 0$. Let $\widetilde{C} = H_1^+ \cap \cdots \cap H_{n - 1}^+$. By the inductive hypothesis, $\widetilde{C}$ is a finitely generated pointed cone; let $B \subseteq W$ be a finite generating set of $\widetilde{C}$.

Also, define the hyperplane $H_n = \{w \in W \, | \, \langle v_n, w \rangle = 0\}$. Then $H_n$ is itself a finite dimensional vector space over $k$. By the inductive hypothesis, the set $C \cap H_n = (H_1^+ \cap H_n) \cap \cdots \cap (H_{n - 1}^+ \cap H_n)$ is an intersection of $n - 1$ half spaces in $H_n$, so it is a finitely generated pointed cone; let $B' \subseteq H_n$ be a finite generating set of $C \cap H_n$.

We claim that the finite set $(B \cap H_n^+) \cup B'$ generates the cone $C$. Since $B'$ generates $C \cap H_n$, it suffices to prove that $(B \cap H_n^+) \cup (C \cap H_n)$ generates $C$, which is guaranteed by the previous lemma.

Theorem (Minkowski–Weyl).

Let $V, W$ be finite-dimensional vector spaces over an ordered field $k$ and let $\langle\cdot , \cdot\rangle \colon V \times W \to k$ be a perfect pairing. Let $C \subseteq V$ be a finitely generated pointed cone. Then

$$C^* = \{w \in W \, | \, \text{$\langle v, w \rangle \geq 0$ for all $v \in C$}\} \subseteq W$$

is also a finitely generated pointed cone.

Proof.

Since $C$ is finitely generated, there exist $v_1, \ldots, v_n \in V$ such that $C = \operatorname{span}_{k_{\geq 0}}\{v_1, \ldots, v_n\}$. Then $C^*$ is the intersection of the half spaces $H^+_i = \{w \in W \, | \, \langle v_i, w \rangle \geq 0\}$, so it is a finitely generated pointed cone by the previous lemma.

[Mitchell Lee]

By the way, Wikipedia refers to the construction in mathlib as the "internal dual cone": https://en.m.wikipedia.org/wiki/Dual_cone_and_polar_cone

[Mitchell Lee]

@Yaël Dillies Do you have thoughts on this?