Linear Logic and Algebraic Geometry

I noticed a couple of suspicious similarities between, on the one hand, some basic definitions in algebraic geometry (or maybe arguably just commutative algebra) and, on the other hand, the constructive semantics of linear logic. I don't know if these amount to much of anything interesting, but I thought I'd note them down just in case there is any value.

The tl;dr is that "algebraic geometry is like unrestricted logic" (as opposed to linear logic).

It has "weakening" and "contraction" principles
The the "variety-of" $V$ and "ideal-of" $I$ functions from Hilbert's Nullstellensatz correspond to the shift operators $\ups$ and $\dns$ from focusing.
The additive conjunction $\amp$ and the multiplicative conjunction $\otimes$ coincide when appropriately interpreted in rings and spectra, in the sense that $\ups ( P_1 \otimes P_2)$ has the same interpretation as $(\ups P_1) \amp (\ups P_2)$. These normally coincide in unrestricted logic, and crucially do not coincide in linear logic.

This makes me wonder:

Question

Is there some kind of "substructural algebraic geometry" where \[ \ups ( P_1 \otimes P_2) \equiv (\ups P_1) \amp (\ups P_2) \] fails to hold?

1. Prime Ideals and Weakening and Contraction

Fix a commutative ring $R$. A subset $J \subseteq R$ is an ideal if

$0 \in J$.
$a\in J$ implies $-a \in J$.
$a,b \in J$ imply $a+b \in J$.
$a \in J, f \in R$ imply $af \in J$.

An ideal $\pp$ is a prime ideal if for all $a,b\in R$ we have that $ab \in \pp$ implies $a\in \pp$ or $b\in \pp$.

Now we make a suggestive definition, which makes elementhood in a prime ideal resemble logical entailment. Define $f_1, \ldots, f_n \tri \pp$ to mean $f_1\cdots f_n \in \pp$, using the multiplication operation of the ring $R$. Let $\Gamma$ stand for an arbitrary list of elements in $R$.

Lemma: The relation $\tri$ satisfies weakening and contraction laws as follows:
\[{\Gamma \tri \pp \over \Gamma, f \tri \pp }\mathsf{weak} \qquad {\Gamma, f, f \tri \pp \over \Gamma, f\tri \pp}\mathsf{contr}\] Proof: Weakening follows merely because $\pp$ is an ideal. If $\prod \Gamma \in \pp$, then by axiom 4 of being an ideal, we have $\left(\prod\Gamma\right) \cdot f \in \pp$ as well. $\cqed$

Contraction follows because $\pp$ is prime. For suppose $(\prod \Gamma)\cdot f \cdot f \in \pp$. Since $\pp$ is prime, either $\prod \Gamma \in \pp$, or $f \in \pp$, or (redundantly!) $f \in \pp$. In any of those cases, we can apply axiom 4 of the definition of being an ideal to find that $(\prod \Gamma)\cdot f \in \pp$.

2. The Variety-Ideal Adjunction and Focusing Polarity Shifts

In classical algebraic geometry, we pick a field $k$, and consider the polynomial ring $k[x_1, \ldots, x_n]$, and talk about the order-reversing functions $V$ ("variety of") and $I$ ("ideal of") which pass between subsets $S$ of the polynomial ring $k[x_1, \ldots, x_n]$, and subsets $X$ of the affine space $\A_k^n$. These form a Galois connection. \[I(X) = \{ f \in R \st \forall p \in X . f(p) = 0\}\] \[V(S) = \{ p \in \A_k^n \st \forall f \in S . f(p) = 0 \}\] The ideal of a set of points is the set of all polynomials that are zero on all of those points. The variety of a set of polynomials is the set of points that makes all of the polynomials zero.

More generally, if we have a ring $R$, we can consider its spectrum $\spec(R)$, a topological space whose underlying set is the set of all prime ideals $\pp \subseteq R$. The functions $V$ and $I$ generalize to:

They can be defined as follows, assuming $S \subseteq R$ and $X\subseteq \spec(R)$: \[I(X) = \{ f \in R \st \forall \pp \in X . f \in \pp \}\] \[V(S) = \{ \pp \in \spec(R) \st \forall f \in S . f \in \pp \}\] The condition that $f$ is zero at a point $p$ is replaced by the condition that the $f$ belongs to the ideal $\pp$.

Let us change notation slightly to resemble the logical construction immediately below. Instead of thinking in terms of subsets of $R$ and $\spec(R)$, let us treat $S$ (and $IX$) as predicates on $R$, and $X$ (and $VS$) as predicates on $\spec(R)$. We continue to use the notation $f \tri \pp$ for $f \in \pp$. Now observe the resemblance of \[(IX)(f) = \forall (\pp : \spec(R)) . X(\pp) \imp (f \tri \pp) \] \[(VS)(\pp) = \forall (f : R) . S(f) \imp (f \tri \pp) \] to the clauses for the shift operators in the constructive semantics of a polarized logic: \[\sem{\dns N}(\alpha) = \forall \phi . \sem N(\phi) \imp (\alpha \tri \phi)\] \[\sem{\ups P}(\phi) = \forall \alpha . \sem P(\alpha) \imp (\alpha \tri \phi)\]

3. Additive/Multiplicative Conjunctions Coincide

We can expand this observation into a fragment of a "semantics" of polarized propositional logic in rings and spectra. In this semantics it holds that \[ \ups ( P_1 \otimes P_2) \equiv (\ups P_1) \amp (\ups P_2) \] which is further corroboration that we are somehow observing a resource-unrestricted logic rather than linear logic. Recall that the usual semantic clauses for additive and multiplicative conjunction are: \[\sem{N_1 \amp N_2}(\phi) = \sem{N_1}(\phi) \lor \sem{N_2}(\phi) \] \[\sem{P_1 \otimes P_2}(\alpha) = \exists \alpha_1, \alpha_2. (\alpha = \alpha_1 \otimes \alpha_2) \land \sem{P_1}(\alpha_1) \land \sem{P_2}(\alpha_2) \]

We interpret

positive propositions as predicates on $R$
negative propositions as predicates on $\spec(R)$
positive worlds $\alpha$ as ring elements $f \in R$
negative worlds $\phi$ as prime ideals $\pp \in \spec(R)$
$\ups$ as $V$
$\dns$ as $I$
the binary operation $\otimes$ on positive worlds as ring multiplication

So lets suppose we have an interpretation $\sem {P_1} = S_1$ and $\sem{P_2} = S_2$ of two positive propositions as subsets $S_1, S_2 \subseteq R$.

Observe that the standard lifting of ring multiplication to subsets is the definition \[ S_1S_2 = \{f \in R \st \exists f_1, f_2. (f = f_1 f_2) \land (S_1)(f_1) \land (S_2)(f_2) \}\]

Let's compute the interpretation of $\ups ( P_1 \otimes P_2)$. \[\sem{\ups ( P_1 \otimes P_2)}(\pp) \iff \forall (f:R) . \sem{ ( P_1 \otimes P_2)}(f) \imp (f \in \pp) \] \[\iff \forall (f:R) . ( \exists (f_1,f_2:R).(f = f_1f_2) \land \sem{P_1}(f_1) \land \sem{P_2}(f_2)) \imp (f \in \pp) \] \[\iff \forall (f_1,f_2:R). \sem{P_1}(f_1) \imp \sem{P_2}(f_2) \imp (f_1f_2 \in \pp) \] \[\iff \forall (f_1,f_2:R). f_1 \in S_1 \imp f_2 \in S_2 \imp (f_1f_2 \in \pp) \] \[\iff S_1 S_2 \subseteq \pp \] And now let's compute the interpretation of $(\ups P_1) \amp (\ups P_2)$: \[\sem{(\ups P_1) \amp (\ups P_2)}(\pp) \iff \sem{\ups P_1}(\pp) \lor \sem{\ups P_2}(\pp) \] \[\iff (\forall (f_1:R). \sem{ P_1}(f_1) \imp f_1 \in \pp) \lor (\forall (f_2:R). \sem{ P_2}(f_2) \imp f_2 \in \pp) \] \[\iff (\forall (f_1:R). f_1 \in S_1 \imp f_1 \in \pp) \lor (\forall (f_2:R). f_2 \in S_2 \imp f_2 \in \pp) \] \[\iff (S_1 \subseteq \pp) \lor (S_2 \subseteq \pp)\] But we can in fact show

Lemma: \[ S_1 S_2 \subseteq \pp \iff (S_1 \subseteq \pp) \lor (S_2 \subseteq \pp)\]
Proof:
$\Leftarrow$: Suppose wlog that $S_1 \subseteq\pp$. Then since $\pp$ is an ideal, $S_1 S_2 \subseteq \pp$.
$\imp$: Suppose towards a contradiction that not $(S_1 \subseteq \pp) \lor (S_2 \subseteq \pp)$. This means we have $s_1\in S_1 \setminus\pp , s_2\in S_2\setminus \pp$. But then $s_1 s_2 \in S_1S_2$, and since $\pp$ is a prime ideal, we also know $s_1 s_2 \not\in \pp$. This contradicts the assumption $S_1S_2\subseteq \pp$. $\cqed$

Therefore $\otimes$ and $\amp$ coincide in the semantics, at least up to appropriately inserted $\ups$-shifts.