Zulip Chat Archive

Stream: maths

Topic: categorical product

Kenny Lau (Jul 03 2019 at 07:36):

Is there a category $C$ such that:
1. For every discrete category $D$ and functor $F:D\to C$ , $F$ has a limit (i.e. every sub-multi-set of Obj(C) has limit).
2. $C$ has no product, i.e. there is no functor $F : C \times C \to C$ such that the induced natural transformation Hom(A,B) x Hom(A,C) -> Hom(A,F(B,C)) between two functors $C^{op} \times C \times C \to Set$ is a natural isomorphism

Mario Carneiro (Jul 03 2019 at 07:59):

Using $D={\bf 2}$ , we know that $C$ has a product object $A\times B$ for all $A,B\in Obj(C)$ . Pick one for every pair A,B to obtain a functor $\times:C\times C\to C$ . (The object part of this is obvious, and if $f: A\to A', g:B\to B'$ then $f\times g := [f\circ \pi^1_{A,B}, f\circ \pi^2_{A,B}]_{A',B'}$ .) Then we can define $\phi(f:A\to B, g:A\to C) := [f, g]_{B,C}:A\to B\times C$ and $\phi^{-1}(h:A\to B\times C) :=(\pi^1_{B,C}\circ h, \pi^2_{B,C}\circ h)$ and this is an isomorphism.

In short, the only tricky part is using the axiom of choice to pick a product for every pair of objects. After that it's just equating two ways to say "a category with products".

Kenny Lau (Jul 03 2019 at 08:28):

what if Obj(C) is a class...?

Mario Carneiro (Jul 03 2019 at 08:32):

Then you have to be more careful about what you mean

Kenny Lau (Jul 03 2019 at 08:32):

is there a class that has no choice function?

Mario Carneiro (Jul 03 2019 at 08:32):

What's a category? What's a functor? What's an existential quantification over classes?

Mario Carneiro (Jul 03 2019 at 08:33):

large category theory in ZFC is tricky

Kenny Lau (Jul 03 2019 at 08:33):

I see

Mario Carneiro (Jul 03 2019 at 08:34):

For some choice of definitions, I think it's possible that you can have the existential statement 1 without any concrete functor class term refuting 2

Mario Carneiro (Jul 03 2019 at 08:34):

You can't prove 2 though because it's a higher order statement

Mario Carneiro (Jul 03 2019 at 08:35):

ZFC does not prove the existence or nonexistence of a class with no choice function

Mario Carneiro (Jul 03 2019 at 08:36):

Assuming that all classes have a choice function is usually called "global choice" and is morally equivalent to Lean's choice

Kenny Lau (Jul 03 2019 at 08:36):

does V\{{}} admit a choice function?

Mario Carneiro (Jul 03 2019 at 08:36):

that's also global choice

Kenny Lau (Jul 03 2019 at 08:36):

I don't like this

Kenny Lau (Jul 03 2019 at 08:37):

it's all because of Russell

Mario Carneiro (Jul 03 2019 at 08:37):

You can't prove it in ZFC because it is a higher order statement, it asserts the existence of a class term

Mario Carneiro (Jul 03 2019 at 08:38):

You can axiomatize global choice by saying "here is a class term, I assert it is a choice function on V"

Kenny Lau (Jul 03 2019 at 08:38):

what if we only look at first order sentences?

Mario Carneiro (Jul 03 2019 at 08:38):

That is a first order statement - the "class term" can be replaced by a primitive unary predicate

Mario Carneiro (Jul 03 2019 at 08:39):

It's conservative over ZFC

Kenny Lau (Jul 03 2019 at 08:40):

is there a sentence in two variables $\varphi(x,y)$ such that $\forall x[x \ne \varnothing \implies [\exists! y \varphi] \land [\forall y \varphi \implies y \in x]]$