Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Resources on disinclusion / "directed apartness" relations?

James Gilles (Dec 30 2024 at 20:18):

Recently I was thinking about the relation $\not\subseteq$ between sets. There's an analogous relation in any finite poset:

$a\not\leq b \Leftrightarrow \neg (a \leq b)$.

$\not\leq$ is preserved by finite poset monos.

I'm wondering about how to constructively define something analogous for infinite posets. I'm thinking of the distinction between $\not=$ and $\#$ (the apartness relation). Apartness relations are axiomatized as:

• $\neg (a \# a)$
• $a \# b \Leftrightarrow (b \# a)$
• $a \# b \Rightarrow (a \# c \lor b \# c)$

I've heard this is stronger, constructively, than $\not=$. I'm curious if anybody knows of work doing analogous things with $\not\leq$.

I guess this would be related to the relation $Hom(a,b) = \varnothing$ in classical categories, and maybe $Hom(a,b) = 0$ in Ab-enriched categories.

James Gilles (Dec 30 2024 at 20:35):

(If I was to try to define $\not\leq!$, I'd say:
$a \not\leq!\; c \land b \leq c \Rightarrow a \not\leq!\; b$.
But I'm not sure if this suffices.)

Mike Shulman (Dec 30 2024 at 22:26):

Analogues of apartness for order relations are discussed in section 8 of my paper Affine logic for constructive mathematics. You may not want to plow through the preceding 7 sections to understand everything, but Theorem 8.3 states some axioms relating $\le$ to $\not\le$ (there written as $>$).

James Gilles (Dec 31 2024 at 06:08):

Wonderful, thank you. I actually had found that paper earlier today and have been enjoying browsing through it. It is very clear. I think I was reading an older version though, which Google linked me to for whatever reason.

James Gilles (Dec 31 2024 at 06:28):

Ah, the old version of the paper had "linear" in the title rather than "affine", I was searching for "linear logic apartness relations".

Mike Shulman (Dec 31 2024 at 18:22):

Yeah, the referee said I should call it "affine" instead, and I suppose they were probably right. "Linear" sounds sexier, but "affine" is more correct since the logic it uses is actually affine.