## 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

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]]$

Not in ZFC

why not?

#### Mario Carneiro (Jul 03 2019 at 08:41):

choice is not definable

#### Kenny Lau (Jul 03 2019 at 08:41):

is that a theorem?

yes

how hard is it?

#### Mario Carneiro (Jul 03 2019 at 08:41):

For instance, there is no definable well order of the reals

#### Mario Carneiro (Jul 03 2019 at 08:42):

Not actually sure who to credit for it

#### Kenny Lau (Jul 03 2019 at 08:42):

so for example this implies V=L?

#### Mario Carneiro (Jul 03 2019 at 08:44):

Here's a proof: https://math.stackexchange.com/a/1315720

#### Mario Carneiro (Jul 03 2019 at 08:44):

It doesn't imply V=L

#### Mario Carneiro (Jul 03 2019 at 08:46):

It certainly "enlarges" L but you still can't prove that all sets are constructible without parameters

#### Kenny Lau (Jul 03 2019 at 08:47):

ok thanks

Last updated: May 11 2021 at 15:12 UTC