4
$\begingroup$

When every epi splits a category is said to satisfy the Axiom of Choice.

When every idempotent splits a category is called Cauchy Complete or Idempotent complete.

These look to be well-studied notions, but what about the corresponding question for monos, i.e., the Axiom of Choice for the opposite category? Does it have a name and are there any references on it? Is it trivial in some way I'm not seeing and that's why it's not studied?

As examples, it's true in Vect, and clearly it's true for categores of NonEmpty and Pointed Sets (using at least LEM).

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ "Co-choice." (Axiom thereof --- MO requires a character minimum.) $\endgroup$
    – Theo Johnson-Freyd
    Commented May 17, 2016 at 1:13
  • $\begingroup$ And I know of no useful discussion. Clearly a category satisfies co-choice iff its opposite satisfies choice. But categories in nature do come with a direction, and so in examples these have different flavor. $\endgroup$
    – Theo Johnson-Freyd
    Commented May 17, 2016 at 1:14
  • 1
    $\begingroup$ We give the name Axiom of Choice to a topos in which all epis split because a topos has other structure capable of making this agree with other forms of AC. However, Max doesn't say anything else about the structure of his category or give any hint of applications besides that monos split. $\endgroup$
    – Paul Taylor
    Commented May 17, 2016 at 9:40
  • 1
    $\begingroup$ Sorry about the lack of context, but the problem is that I'm using split monos (i.e. retractions) in my work and not monos and I wanted a clean explanation for why this is a big difference in my setting (Programming Languages) where these will almost always be distinct notions. So unfortunately I have no applications for this idea, only non-applications. $\endgroup$
    – Max New
    Commented May 17, 2016 at 11:31
  • 2
    $\begingroup$ It's an old idea going back to Dana Scott that you can think of types in an "untyped" language as retracts of a universal domain. I believe the idea is first introduced in "Datatypes as Lattices" but a modern, more accessible description is "Universal Types and What They are Good For" by John Longley. $\endgroup$
    – Max New
    Commented Jun 4, 2016 at 17:19

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .