2
$\begingroup$

For a poset $X$ we define an upperbound $w \in X$ of a subset $S \subseteq X$ to be a weak-supremum if

$(\forall a \in S (a \leq b)) \implies w \leq b$.

While a supremum is defined more carefully (in terms of an excess relation $\not\leq$ on $X$). That is, we define and upperbound $s \in X$ of an inhabited subset $S \subseteq X$ to be a supremum if

$\forall x \in X(s \not\leq x \implies \exists a \in S (a \not\leq x))$,

This differentiation between suprema primarily comes up in constructive analysis when the poset $X = \mathbb{R}$. But, I am currently studying lattice theory constructively and the question began to arise. Given a poset $X$ and a subset $S \subseteq X$ how do we define the join of $S$, $\bigvee S$?

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ In any case $\forall a\in S(a\le b)$ precisely means that $b$ is an upper bound of $S$. Hence your definition of weak-supremum is the definition of the least upper bound, which is the same as join. It is also what I would call supremum. To clarify its relation with your definition of supremum one would need to know precise axiomatics for your relation $\not\le$. $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Aug 16, 2021 at 16:33
  • 1
    $\begingroup$ @PaulTaylor I agree that I need to quantify x, but the choice of an excess relation is neccesary to keep things working in general for posets. $\endgroup$
    – ToucanIan
    Commented Aug 18, 2021 at 18:25
  • 1
    $\begingroup$ @მამუკაჯიბლაძე The axiomatics of an excess relation should be shared. I originally thought they were unnecesary and beyond the scope of the question. Your are correct in saying the two formulas describe the same object, classically. My question pertains to the distinction that arises due to the intuitionstic interpretation. $\endgroup$
    – ToucanIan
    Commented Aug 18, 2021 at 18:29
  • 2
    $\begingroup$ Note that since your stronger notion of supremum is a formal De Morgan dual of the ordinary one, it can be obtained from the antithesis translation, which also supplies a list of axioms for $\nleq$ (Theorem 8.3). $\endgroup$
    – Mike Shulman
    Commented Aug 18, 2021 at 20:03
  • 3
    $\begingroup$ @მამუკაჯიბლაძე Yes, I agree -- what Toucanlan calls the "weak supremum" is the same as the join, and I've never heard it called anything but plain "supremum" even constructively. I would call the other something like a "strong supremum"; I'm not sure if there is an additional question being asked about it. $\endgroup$
    – Mike Shulman
    Commented Aug 19, 2021 at 0:23

0

Reset to default

You must log in to answer this question.