Zulip Chat Archive

Stream: maths

Topic: categorical product


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

Is there a category CC such that:
1. For every discrete category DD and functor F:DCF:D\to C, FF has a limit (i.e. every sub-multi-set of Obj(C) has limit).
2. CC has no product, i.e. there is no functor F:C×CCF : 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 Cop×C×CSetC^{op} \times C \times C \to Set is a natural isomorphism

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

Using D=2D={\bf 2}, we know that CC has a product object A×BA\times B for all A,BObj(C)A,B\in Obj(C). Pick one for every pair A,B to obtain a functor ×:C×CC\times:C\times C\to C. (The object part of this is obvious, and if f:AA,g:BBf: A\to A', g:B\to B' then f×g:=[fπA,B1,fπA,B2]A,Bf\times g := [f\circ \pi^1_{A,B}, f\circ \pi^2_{A,B}]_{A',B'}.) Then we can define ϕ(f:AB,g:AC):=[f,g]B,C:AB×C\phi(f:A\to B, g:A\to C) := [f, g]_{B,C}:A\to B\times C and ϕ1(h:AB×C):=(πB,C1h,πB,C2h)\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 φ(x,y)\varphi(x,y) such that x[x[!yφ][yφyx]]\forall x[x \ne \varnothing \implies [\exists! y \varphi] \land [\forall y \varphi \implies y \in x]]

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

Not in ZFC

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

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?

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

yes

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

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: Dec 20 2023 at 11:08 UTC