While thinking about constructive mathematics, I stumbled on the following notion, and I would like to know if it has a standard name, a simpler equivalent, or has appeared in the literature:

Say that a set $X$ is mixable (temporary term, for lack of a better one) when it satisfies the following property:

$$\forall S\subseteq X.(\forall u\in S.\forall v\in S.(u=v) \Rightarrow \exists x\in X.\forall y\in S.(y=x))$$

In other words, every subset $S$ of $X$ all of whose elements are equal is a subset of the singleton $\{x\}$ for a certain $x\in X$.

Classically, it is trivial that every (edit:) nonempty set is mixable.

  • Example: Every power set object $\mathscr{P}(Z)$ is mixable. (Indeed, given $S \subseteq \mathscr{P}(Z)$ as assumed, consider $x := \bigcup_{t\in S} t$, that is, $\{z\in Z : \exists t\in S.(z\in t)\}$. Given $y\in S$, since we have $S = \{y\}$, we have $x = \bigcup\{y\} = y$, as announced.) For the same reason, in CZF, we have: $\forall S.(\forall u\in S.\forall v\in S.(u=v) \Rightarrow \exists x.\forall y\in S.(y=x))$.

  • Counterexample: If $\{0,1\}$ is mixable then the Weak Law of Excluded Middle holds. (Indeed, given $p$ a truth value, consider $S := \{0 : p\} \cup \{1 : \neg p\}$. Clearly all elements of $S$ are equal. But if there is $x\in\{0,1\}$ such that $S \subseteq \{x\}$ then either $x=0$ or $x=1$, and in the first case $\neg\neg p$ while in the second $\neg p$ holds, so on the whole, $\neg p \lor \neg\neg p$.)

In sheaf semantics, saying that a sheaf $X$ on a topological space $E$ is mixable means that (†) for every section $s$ of $X$ on an open set $U$ of $E$, there is a covering of $E$ by open sets $V_i$ such that $X$ has a section $x_i$ on each $V_i$ which coincides with $s$ on $V_i \cap U$. This is the case in particular if $X$ is flabby, but I don't know if this property has a name in the sheaf context.

Edit (2019-03-29): As Mike Shulman points out in his answer, the above property of sheaves is actually equivalent to being flabby, so “flabby” is a good name for the property. Since the proof (by a “typical argument”) is not actually written out on nLab, here it is for the completeness of MathOverflow: assume the sheaf $X$ on $E$ has the property (†) described in the previous paragraph, and let $s$ be a section on $U$. Consider sections of $X$ extending $s$, partially ordered by extension: since chains of sections give rise to a single section on the union by the seaf property, Zorn's lemma implies that there is a maximal extension $s' \in X(U')$ of $s$; now apply (†) to $s'$: for any $i$, the sections $s'$ and $x_i$ glue to give a section of $X$ on $U' \cup V_i$, extending $s$, so by maximality of $s'$ we have $V_i\subseteq U'$, and since this holds for every $i$, in fact $U' = E$. Thus, $X$ is flabby.

Question: Does the above “mixable” property have a standard name or a nicer equivalent, and where might I learn more about it?

  • $\begingroup$ So... mixable is sort of like the opposite of a system of representatives for the equality relation? $\endgroup$
    – Asaf Karagila
    Mar 28 '19 at 20:38
  • $\begingroup$ (Or, again, if we talk about forcing, then $X$ is a rather canonical name, and for every name $S$ for a subset of $X$ and every two names which are forcing into $S$, there is some name which is already forced into $X$ which is equal to them. So sort of the construtivist version of the mixing lemma?) $\endgroup$
    – Asaf Karagila
    Mar 28 '19 at 20:40
  • $\begingroup$ (To add on my second comment, let me point out that the mixing lemma is equivalent to AC over ZF.) $\endgroup$
    – Asaf Karagila
    Mar 28 '19 at 20:41
  • 3
    $\begingroup$ I guess you mean that classically it is trivial that every nonempty set is mixable. $\endgroup$
    – Todd Trimble
    Mar 28 '19 at 21:31
  • 1
    $\begingroup$ The argument in your edit is precisely what I had in mind, sorry for not spelling it out on the nLab page. By the way, most applications of Zorn in mathematical practice require a touchup by LEM, that is, they go like this: "By Zorn's lemma, there is a maximal element. Assume that it does not have the desired property. Then by <some-argument>, we can extend it to a larger element. This contradicts maximality." But here no LEM is necessary. This is relevant because if your metatheory satisfies Zorn, then so will any localic topos, while LEM is just false in most localic toposes. $\endgroup$ Mar 29 '19 at 13:30

According to this proposition, the property in question is (by "a typical argument with Zorn's lemma") equivalent to flabbiness for sheaves on topological spaces. Thus, the term "flabby" is sometimes used more generally inside constructive mathematics for sets with this property.

  • $\begingroup$ Do you have examples of texts where the term "flabby" is used inside constructive mathematics, and, hopefully, discussed internally? $\endgroup$
    – Gro-Tsen
    Mar 28 '19 at 21:55
  • 2
    $\begingroup$ Actually, I guess the internal usage is (surprisingly, to me) only fairly recent: arxiv.org/abs/1810.12708, arxiv.org/abs/1903.01211 $\endgroup$ Mar 28 '19 at 23:16
  • 1
    $\begingroup$ Regarding the history of the term: Already in 1990 Anders Kock used the term "flabby" for the property in question (Algebras for the partial map classifier monad in Category Theory. Proceedings of the International Conference held in Como, Italy, July 22–28, 1990). However, he didn't give an explanation for his choice of terminology. It might be that the connection to flabby sheaves has been known for a long time but never written down. $\endgroup$ Mar 29 '19 at 17:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.