Dual cones without the inner product space assumption

[trivial1711]

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}$ (the real numbers). 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^* = \text{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}$ (the real numbers) 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 is working on this (#Is there code for X?>Main Theorem of Polytope Theory )..

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

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.) 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.

Postscript

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 = \text{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' = \text{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.

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Dual.20cones.20without.20the.20inner.20product.20space.20assumption