Skip to main content
Clarified
Source Link
Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368

If we take Choice-1 in Lawvere's original form with "has (global) elements" in place of "is not initial", then itChoice-2 follows from Choice-1 in any Boolean category. Factor $f:X\to Y$ as an epi $h : X \twoheadrightarrow Z$ followed by a mono $m:Z\hookrightarrow Y$. Then $h$ is a split epi by Choice-2, while $m$ is complemented by Booleanness, and therefore a split mono since $Z$ has a global element. So we have $s:Z\to X$ with $h s = 1_Z$, and $r:Y\to Z$ with $r m = 1_Z$, and defining $g = s r$ we have $f g f = (m h) (s r) (m h) = m (h s) (r m) h = m h = f$.

In a topos, Booleanness also follows from Choice-21 by the Diaconescu-Goodman-Myhill theorem. So the argumentChoice-2 also works in any topos, again withfollows from Lawvere's original version of Choice-1 in any topos.

If we take Choice-1 in Lawvere's original form with "has (global) elements" in place of "is not initial", then it follows from Choice-1 in any Boolean category. Factor $f:X\to Y$ as an epi $h : X \twoheadrightarrow Z$ followed by a mono $m:Z\hookrightarrow Y$. Then $h$ is a split epi by Choice-2, while $m$ is complemented by Booleanness, and therefore a split mono since $Z$ has a global element. So we have $s:Z\to X$ with $h s = 1_Z$, and $r:Y\to Z$ with $r m = 1_Z$, and defining $g = s r$ we have $f g f = (m h) (s r) (m h) = m (h s) (r m) h = m h = f$.

In a topos, Booleanness also follows from Choice-2 by the Diaconescu-Goodman-Myhill theorem. So the argument also works in any topos, again with Lawvere's original version of Choice-1.

If we take Choice-1 in Lawvere's original form with "has (global) elements" in place of "is not initial", then Choice-2 follows from Choice-1 in any Boolean category. Factor $f:X\to Y$ as an epi $h : X \twoheadrightarrow Z$ followed by a mono $m:Z\hookrightarrow Y$. Then $h$ is a split epi by Choice-2, while $m$ is complemented by Booleanness, and therefore a split mono since $Z$ has a global element. So we have $s:Z\to X$ with $h s = 1_Z$, and $r:Y\to Z$ with $r m = 1_Z$, and defining $g = s r$ we have $f g f = (m h) (s r) (m h) = m (h s) (r m) h = m h = f$.

In a topos, Booleanness also follows from Choice-1 by the Diaconescu-Goodman-Myhill theorem. So Choice-2 also follows from Lawvere's original Choice-1 in any topos.

Source Link
Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368

If we take Choice-1 in Lawvere's original form with "has (global) elements" in place of "is not initial", then it follows from Choice-1 in any Boolean category. Factor $f:X\to Y$ as an epi $h : X \twoheadrightarrow Z$ followed by a mono $m:Z\hookrightarrow Y$. Then $h$ is a split epi by Choice-2, while $m$ is complemented by Booleanness, and therefore a split mono since $Z$ has a global element. So we have $s:Z\to X$ with $h s = 1_Z$, and $r:Y\to Z$ with $r m = 1_Z$, and defining $g = s r$ we have $f g f = (m h) (s r) (m h) = m (h s) (r m) h = m h = f$.

In a topos, Booleanness also follows from Choice-2 by the Diaconescu-Goodman-Myhill theorem. So the argument also works in any topos, again with Lawvere's original version of Choice-1.